Karlheinz Friedberger
Karlheinz Friedberger
Hi. This is quite a long issue, so I will answer in smaller parts. See below. > 1. The conversion between `Rational` and `Integer` sorts in this direction is given...
There are some cases where arity is not sufficient: PLUS, EQ, DISTINCT typically have an arity of 2, however can be used with more operands as well, such as 3...
This PR might provide a solution for a quite old issue: https://github.com/sosy-lab/java-smt/issues/100 :-)
Z3 is the only solver that has its own implementation of tactics like NNF. For other solvers, we apply the tactic in JavaSMT directly. A NNF-result is not unique, i.e.,...
I fully agree with you. Libraries should **not** print directly to stdout/stderr. There have been cases in the past, where we informed the developers and they changed their solver code...
Related issue: https://github.com/uuverifiers/ostrich/issues/95
I find this branch quite interesting and was just playing around with it yesterday. I wished for such a tracing layer some years ago, as it would simplify debugging from...
This should be fixed with upcoming [v5.6.12 of MathSAT](https://mathsat.fbk.eu/download.html).
The PR #544 was merged. We still require feedback from CPAchecker whether the issues with model generation are solved.
MathSAT v5.6.15 is available via Ivy and integrated via #557 . Could someone test the new version?