Karlheinz Friedberger
Karlheinz Friedberger
It would be nice to see the `name of the current file`, i.e., log file, property file, or source code when it is opened as an overlay in a generated...
Currently it is only [weakly documented](https://github.com/sosy-lab/java-smt#multithreading-support) which solvers can use which components in a multi-threaded environment. We should check whether some solvers can use several stacks (for the same context)...
There is a new version of OptiMathSAT, which does not bring anything new, except internal improvements. Normally, such an update would not be worth an issue. However, there is a...
The team of Boolector developed a new SMT solver [Bitwuzla](https://bitwuzla.github.io/) that seems to be quite fast for bitvector logic (see [results of SMT-COMP 2020](https://bitwuzla.github.io/smt-comp.html)). Bitwuzla seems to be the successor...
Since a few months, Boolector has new features that might be helpful for us. ### Global Declarations JavaSMT actually only support global declarations, and Boolector [provides now an option for...
The newest (not yet released) version of Yices2 seems to support interpolation: [Interpolation in the Yices2 API](https://github.com/SRI-CSL/yices2/blob/141154bfaa0a46d79b8e602dfad11edefdcfdf8a/src/api/yices_api.c#L9244) Additionally, they seem to provide their own Java bindings, which might be worth...
We should test the performance of basic operations like: - push, pop, addConstraint - creating large amounts of variables - creating large (but cheap) formulas - creating and closing several...
Some SMT solvers provide the feature to define self-build sorts, such as tuple sorts. We might think of a way, perhaps even a new FormulaManager, to support such a feature....
The last column of our [Buildbot table](https://buildbot.sosy-lab.org/cpachecker/results/nightly-predicate/00174.nightly-predicate.diff.html#/table) contains several exceptions from MathSAT5, where PI is already declared (standard symbol in FP theory?) and parsed again from SMTLIB. If this is...
Building JavaSMT with the Eclipse compiler works. However executing the steps `ant clean; ant build-project-ecj; ./runExamples.sh` reports an error: Exception in thread "main" java.lang.Error: Unresolved compilation problem: Type safety: Unchecked...