Model usage: fix usage of model values and model evaluation after changing the underlying context. #553
Conversation
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
…nging the underlying context. Several solvers referenced a live prover context in the model, allowing the user to insert further queries in the model or remove queries from the context, potentially making the model inconsistent and unreliable for further iteration or evaluation. The solution consists of several steps, for some solvers: - compute the value-assignments upfront when constructing the model. - invalidate the model once the context is changed. Solvers that already provide a persistent model, such as MathSAT, SMTInterpol, and Z3, will not change their behaviour. However, other solvers will throw an exception on invalid usage. While this change is backward-compatible in the API, it is a serious bugfix that changes the behaviour of some solver bindings in JavaSMT, because we need to loosen a basic guarantee for models.
baierd
requested changes
Nov 19, 2025
Contributor
baierd
left a comment
baierd
left a comment
There was a problem hiding this comment.
Nice addition/cleanup! Thank you!
2 requests to extend the cleanup even more, nothing mayor.
| * returned <code>false</code>. | ||
| */ | ||
| @Override | ||
| public List<BooleanFormula> getUnsatCore() { |
Contributor
There was a problem hiding this comment.
UnsatCores can also affect solver states (e.g. in Z3). It might be a good idea to generally assume that they do?
Member
Author
There was a problem hiding this comment.
Can you give an example? Why would Z3 change its state when calling getUnsatCore?
src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java
Outdated
Show resolved
Hide resolved
Contributor
daniel-raffler
left a comment
daniel-raffler
left a comment
There was a problem hiding this comment.
Looks good to me!
…and unsat core. This fixes a invalid return value in Z3OptimizationProver: We wrongly returned "false" instead of throwing "UnsupportedOperationException".
…, even on empty stack.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
Several solvers referenced a live prover context in the model, allowing the user to insert further queries in the model or remove queries from the context, potentially making the model inconsistent and unreliable for further iteration or evaluation.
The solution consists of several steps, for some solvers:
Solvers that already provide a persistent model, such as MathSAT, SMTInterpol, and Z3, will not change their behaviour.
However, other solvers will throw an exception on invalid usage.
While this change is backward-compatible in the API, it is a serious bugfix that changes the behaviour of some solver bindings in JavaSMT, because we need to loosen a basic guarantee for models.