Throw SolverException when interpolation fails - #701
Merged
Conversation
…the solver state is SAT
OpenSMT doesn't support model generation for arrays and will only return abstract values when evaluting array variables. We therefore can't return a model when arrays were used in the constraints
…for the selected logic OpenSMT only supports interpolation for QF_UF, QF_LIA and QF_LRA and the logic needs to be explicitly set with `solver.opensmt.logic`
baierd
requested changes
Jul 28, 2026
baierd
left a comment
baierd
left a comment
Contributor
There was a problem hiding this comment.
Nice work! Only minor points to work on.
baierd
requested changes
Jul 30, 2026
OpenSMT doesn't support extraction of array values for the model. We abort model generation when the constraints contain formulas over arrays and print this message
Contributor
|
I can approve the PR once Checkstyle is fixed ;D |
Contributor
Author
Sorry about that. The format is fixed now |
…atch block, so that we don't catch exceptions from the vector creation accidentally
baierd
approved these changes
Aug 10, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hello,
this PR changes some runtime exceptions to
SolverExceptionsso that they can be better caught by the user. Specifically, we now throw aSolverExceptionif interpolation fails in Bitwuzla or Yices. This is in line with how interpolation failures are handled in MathSAT, which also only has partial interpolation support for some theories. In addition we throw aSolverExceptionin OpenSMT when model generation or interpolation are not available for the selected logicCloses #643