Baier D.

Applying light quantifier elimination `applyQELightImpl()` is only implemented for Z3. While returning the original formula is valid, we should tell users that this only works for Z3. Otherwise they expect...

MathSAT5 Returns Null for msat_model_create_iterator()

13

I found a problem when asking for a model iterator in Mathsat5 using CPAchecker. It takes about 600s to get to the error and this was executed using [this branch](https://gitlab.com/sosy-lab/software/cpachecker/-/tree/symex-pathbased-solver-context?ref_type=heads)...

Z3 supports interpolation again (using model-based interpolants) by utilizing their CHC backend (Spacer). It has to be compiled with a special flag for that. We can add this back in...

Princess Boolean Quantification Broken

1

Quantification with bound boolean variables is currently not working in Princess. We should investigate and fix this if possible.

Update to SMTInterpol Version 2.5-1388

19

SMTInterpol is available in version 2.5-1388 while we still use the 3 year old version 2.5-1242. I don't know the details of changes, but the new version does include changes...

Extend Solver Independent SMTLib2 Parser/Generator

3

This PR extends JavaSMT with an independent SMTLib2 parser/generator layer. Every solver can use the layer to generate or parse SMTLib2, independent of their own implementation. The parsing directly uses...

SMTLib2 Output Consistency for Quantified Terms

1

I noticed that quantified formulas are dumped in many different ways, some of which are inconsistent with SMTLib2 and can not be parsed by other solvers. We should add I/O...

Update to Java 17 for Next Major Release

1

Java 11 premier support ended in September 2023. We should update to Java 17 as our basis to keep up with the support and new developments. I would suggest to...

MathSAT5 can create quantified formulas, but not solve them. However, they can be dumped with `msat_to_smtlib2_ext()` and `msat_to_smtlib2_term()`. `msat_to_smtlib2_ext()` exports a full SMTLib2 program, while `msat_to_smtlib2_term()` exports only the formula...

Update CVC4 to the Last Release Version 1.8

2

We are currently using prerelease version 1.8 of CVC4. But 1.8 has been release as the last version of CVC4 and is roughly a year younger than our version. We...