Baier D.
Baier D.
I've added two methods to copy a prover to the solver context with an implementation for Z3 including tests. Note: it seems like Z3 supports this only for the base...
The [getting started](https://github.com/sosy-lab/java-smt/blob/master/doc/Getting-started.md) guide is outdated and should be updated to the most recent version. Also, we might want to include this in our process in the future. Since the...
This issue documents the process and issues of adding Apron as a SMT solver in JavaSMT.
This issue documents the addition of dReal to JavaSMT by @juliusbrehme. Problems are discussed and/or documented here if necassary.
Bitwuzla supports simplification of formulas via the `simplify()` call. We should enable this in our wrapper for the next update of Bitwuzla.
Bitwuzla is very slow for the tests in `FloatingPointFormulaManagerTest` based on the `getListOfFloats()` method. We should extract examples and inform the devs of Bitwuzla about this.
Both OpenSMT2 and Bitwuzla need the removal of certain parts of SMTLIB2 Strings before we can parse them. Examples are comments and `set-logic`. This is currently done lazily and incomplete....
Some operations in SMTLib2, for example Integer `modulo()` and BV `smodulo()` (signed modulo), behave differently. Our documentation does not reflect this properly or fails to explain the differences in a...
Most solvers allow either re-usable shutdown or we use shared environments that are created per prover, making them isolated enough to be shut down without stopping the context. This PR...
Yices2 supports parsing on our currently main branch. But the tests are still disabled for it and it fails many basic tests. This should be investigated and solved before the...