Baier D.

Z3 Invalid Dumping of Quantified Formulas

2

CPAchecker found some regressions for Z3 in (more or less) current main [here](https://gitlab.com/sosy-lab/software/cpachecker/-/issues/1402). Essentially, we assume that quantified formulas only contain consts, and not functions. But that is not a...

OpenSMT2 Options Ambiguity

1

The names of options in OpenSMT2 are often ambiguous, as they don't include details about their specific use-case. All options in OpenSMT2 should be looked at and updated to be...

IEEE Floating-point to Bitvector Conversion Not Supported in All Solvers

5

IEEE Floating-point to Bitvector conversion is not supported in Bitwuzla and CVC5, possibly others. The standard says two things about this conversion: ``` :note "There is no function for converting...

Add SolverException for Model and Prover due to MathSAT5/Z3 Model Problem (Including a Sneaky Throw for API not Supporting Changes)

10

MathSAT5s model iterator method may fail and throws an `IllegalArgumentException`. This exception is misleading, as it is a solver error when building the model. This PR catches the `IllegalArgumentException` and...