Baier D.
Baier D.
I'm having a problem with the multithreaded usage of Yices 2. I am using the current release version with the compile option for thread safety. When trying to assert a...
CVC4 was succeeded by CVC5 and as a consequence support for CVC4 stopped. We should also update to CVC5 as a consequence. This issue tracks the status and problems of...
Since we have a working MathSAT5 binary for ARM, we should incorporate the possibility to use this automatically. This means that our build systems either need to detected the architecture...
This PR covers the Windows support for Yices2. The JNI-wrapper was changed to conform to Windows pointer standards. A bash script is provided that explains how to build Yices2 for...
There are currently 2 SigSevs in the [buildbot](https://buildbot.sosy-lab.org/cpachecker/results/nightly-predicate/00178.nightly-predicate.diff.html#/table) table resulting from the use of interpolation with Mathsat5. I checked the queries with Mathsat directly and those result only in an...
Migrating to JUnit 5 would increase the flexibility and introduce the new features of JUnit 5 to our tests while allowing backwards compatibility with JUnit 4.
Several problems with unclear cause (to a user not fimilar with JavaSMT) are encountered on a regular basis when using JavaSMT. An example would be usage of a formula in...
The FormulaManagers for Integers, and possibly Rationals, are incomplete in CVC4. They do not support multiplication for example. However, CVC4 supports these operations. We need to analyze which operations are...
Parsing 2 equal Strings to formulas results in 2 non-equal formulas. It seems like variables are not reused, but created anew with each query. We should ask the Bitwuzla devs...
Bitwuzla (currently available on the branch add_bitwuzla) crashes with a SIGABRT when trying to parse incomplete formulas/queries. We shoud ask the devs to ease this into a non-critical abort that...