daniel-raffler
daniel-raffler
Hello everyone, this patch set removes all auto generated code and adds a new swig script instead. This will help simplify upgrades to new Bitwuzla versions as changes to the...
Adds a debug mode that helps find common user errors - We check that solver structures are only accessed from the thread that created them - We make sure that...
This patch set is a backport of the floating point parts of https://github.com/sosy-lab/java-smt/pull/353 * It adds a new (JNI) method BitwuzlaJNI.bitwuzla_term_value_get_real() that can be used to read-out floating point values...
Hello everyone, while working on https://github.com/sosy-lab/java-smt/pull/345 I noticed that one of the concurrent tests seems to (occasionally) fail for CVC5. The test case is testBvConcurrencyWithConcurrentContext from SolverConcurrencyTest and you can...
Hello Ostrich seems to struggle with Formulas that don't contain a singleton String. Here is an example: ``` import ap.theories.strings.StringTheory import ap.SimpleAPI import SimpleAPI.ProverStatus import ap.parser._ import ap.theories.strings.SeqStringTheory import ap.util.Debug...
Hello, this is another issue I found while using CPAchecker with Princess. Unfortunately I haven't had much luck trying to pin the problem down. However, maybe the stack trace can...
Hello, we would like to use `yices_term_to_string()` to generate short SMTLIB scripts from yices terms. Unfortunately the function does not seem to escape illegal variable names, which can lead to...
Hello everyone, the goal of this pull request is to add two more theories for strings and rational numbers to the Princess backend. It is a continuation of the work...
Hello everyone, yices2 does not apply correct quotes while dumping SMTLIB formulas. An example for this can be seen in [VariableNamesTest.testBoolVariableDump()](https://github.com/sosy-lab/java-smt/blob/fed0e55e44243a26cc0ca00b90d6835aef6e5d55/src/org/sosy_lab/java_smt/test/VariableNamesTest.java#L557) where the formula for a (boolean) variable named "("...
Hello everyone, in SMTInterpol two Bitvector constants only seem to be equal only when they were created from the same String object: ``` @Test public void testBinary() { Theory theory...