Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Exception when Z3 is interrupted during Model.evaluate() #406

Open
PhilippWendler opened this issue Oct 29, 2024 · 1 comment · May be fixed by #407 or #408
Open

Exception when Z3 is interrupted during Model.evaluate() #406

PhilippWendler opened this issue Oct 29, 2024 · 1 comment · May be fixed by #407 or #408
Assignees
@kfriedberger
Labels
bug Z3

Comments

@PhilippWendler
Copy link
Member

Same as #291, just for a different entry point:

Exception in thread "main" com.microsoft.z3.Z3Exception: canceled
	at com.microsoft.z3.Native.modelEval(Native.java:3948)
	at org.sosy_lab.java_smt.solvers.z3.Z3Model.evalImpl(Z3Model.java:380)
	at org.sosy_lab.java_smt.solvers.z3.Z3Model.evalImpl(Z3Model.java:27)
	at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:127)
	at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluate(AbstractEvaluator.java:109)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.evaluate(CachingModel.java:57)
	at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluateImpl(ModelView.java:50)
	at org.sosy_lab.cpachecker.util.predicates.smt.ModelView.evaluate(ModelView.java:56)
[...]

Occurs with JavaSMT 5.0 and Z3 4.12.5.0. Full stack trace available here.

JavaSMT should ensure that all calls into Z3 handle interruptions appropriately and translate them into InterruptedExceptions.
@kfriedberger kfriedberger self-assigned this Oct 29, 2024
@baierd baierd mentioned this issue Oct 29, 2024
Open
@baierd baierd linked a pull request Oct 29, 2024 that will close this issue
Add InterruptedExceptions to Model Generation #407
Open
@baierd
Copy link
Collaborator

baierd commented Oct 29, 2024

I added the correct Exception in a new branch . I guess we should discuss this in PR #407.

kfriedberger added a commit that referenced this issue Oct 29, 2024
@kfriedberger
Z3: handle exceptions from Z3 in a few more places.
aaa7717 
If Z3 is interrupted at those places, we throw a InterruptedException.

We remove the solver-specific Z3SolverException.
It does not bring any benefit over a default SolverException.

This fixes #406.
@kfriedberger kfriedberger linked a pull request Oct 29, 2024 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kfriedberger kfriedberger

Labels
bug Z3
Milestone
No milestone
3 participants
@PhilippWendler @baierd @kfriedberger