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

Regression on simple NIA formula #5376

Closed
wintered opened this issue Jun 29, 2021 · 0 comments
Closed

Regression on simple NIA formula #5376

wintered opened this issue Jun 29, 2021 · 0 comments

Comments

@wintered
Copy link

d5c6abe

$z3-4.8.8 bug.smt2
unsat
$z3-4.8.9 bug.smt2
unsat
$z3-4.8.10 bug.smt2
unsat
$z3release bug.smt2 
unknown
$time z3release smt.mbqi.max_iterations=1000000 bug.smt2
unknown
z3release smt.mbqi.max_iterations=1000000 bug.smt2  146.67s user 0.01s system 99% cpu 2:26.72 total
$
$cat bug.smt2 
(declare-const x Int)
(assert (forall ((v Int)) (= v (* x x))))
(check-sat)
NikolajBjorner added a commit that referenced this issue Jul 6, 2021
@NikolajBjorner
#5376
ca05c66
NikolajBjorner added a commit that referenced this issue Jul 6, 2021
@NikolajBjorner
#5376
af5b2a4
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
1 participant
@wintered