8000 Z3 stops checking for timeout · Issue #7607 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Z3 stops checking for timeout #7607

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
Closed
mikulas-patocka opened this issue Apr 3, 2025 · 3 comments
Closed

Z3 stops checking for timeout #7607

mikulas-patocka opened this issue Apr 3, 2025 · 3 comments

Comments

@mikulas-patocka
Copy link
Contributor

When I run z3 with this input, the solver eventually locks up and stops checking for timeout. When I run it with "z3 timeout=1000", the timeout properly happens and interrupts z3. However, when I run it with "z3 timeout=10000", there is no interruption and the solver locks up indefinitely, consuming 100% CPU.

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const n Int)
(assert (>= a 1))
(assert (>= b 1))
(assert (>= c 1))
(assert (= n 3))
(assert (= (+ (^ a n) (^ b n)) (^ c n)))
(check-sat)
(get-model)
@HuStmpHrrr
Copy link

could you try -T:10?

@mikulas-patocka
Copy link
Contributor Author

With "-T:10", it is properly terminated with the "timeout" message after 10 seconds.

@HuStmpHrrr
Copy link

it's unclear what timeout= is. I suspect that it's a soft timeout, corresponding to -t:, given that both take ms. if you want a hard timeout, -T: is your only choice and you can only control it at the level of seconds.

arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7607
19202af
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@HuStmpHrrr @mikulas-patocka
0