Throw `SolverException` when interpolation fails - #701

Merged

daniel-raffler merged 15 commits into

solver-exceptions

Aug 10, 2026

Commits on Jul 28, 2026

Bitwuzla: Throw a SolverException when interpolation fails
daniel-raffler
committed
db97082
Yices: Throw a SolverException when interpolation fails
daniel-raffler
committed
0df3002
Yices: Throw an IllegalStateException when trying to interpolate and the solver state is SAT
daniel-raffler
committed
13ef436
OpenSMT: Throw a SolverException when model is not available
daniel-raffler
committed
cda727f
OpenSMT: Throw a SolverException when interpolation is not supported for the selected logic
daniel-raffler
committed
5e1c665
Checkstyle
daniel-raffler
committed
f3c5711
OpenSMT: Extract logic check before interpolation
daniel-raffler
committed
923acbb
Bitwuzla: Inline exception handling
daniel-raffler
committed
a7c3072
Yices: Add a constant to list interpolation error messages
daniel-raffler
committed
4c5c4e0
Bitwuzla: Explicitly list error messages for interpolation errors
daniel-raffler
committed
07e3e87
Make error message lists `static final`
daniel-raffler
committed
03cd053

Commits on Jul 31, 2026

OpenSMT: Print a better error message when model generation fails
daniel-raffler
committed
d498dbc

Commits on Aug 4, 2026

Fix format
daniel-raffler
committed
b0d9682

Commits on Aug 10, 2026