Karlheinz Friedberger

Thanks for the example and explanation. The NaN problem is known, but is certainly irrelevant for CPAchecker's usage. Can you report to Alberto, that MathSAT writes something like SMTLIB (using...

Have seen it. I will update the library in the ivy repository soon.

Just for clarification: - the exported/dumped name is now `fp.as_ieee_bv`? - the parser does understand `fp.as_ieee_bv`?

One way to go is to directly compile and package SMTInterpol on our own. Then we can (and need to) analyze all dependencies on our own and set the correct...

Blocked by - https://github.com/ultimate-pa/smtinterpol/issues/35 (closed since Oct 2018) - https://github.com/ultimate-pa/smtinterpol/issues/29 (open since April 2017) - https://github.com/ultimate-pa/smtinterpol/issues/48 (closed since May 2020).

Current status: The support in SMTInterpol for solving with assumptions is very weak. There are many exceptions, and most of them are reported (for some time now) without an available...

Some solver provide that feature, some do not. Currently, this is expected behavior and we even have tests for that. See https://github.com/sosy-lab/java-smt/blob/0dc452dbd532e414abd08d42ef9b75d504168f77/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java#L1203 for tests. Internal renaming of variables is avoided...

yes, separate contexts will help here, or using a naming scheme for different types.

We might aim towards using `Ubuntu 18.04` as a basic platform for building and executing our solvers. Some users currently have `Ubuntu 16.04` that has LTS until 2021. This version...

Hi @ThomasHaas. you are giving only few concrete information for a good answer. Could you provide more information, e.g., - Are all queries for MathSAT/Z3/Yices2 exactly identical? - Could you...