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

(rewriter.flat=false) Refutational unsoundness on simple NIA formula #6091

Closed
wintered opened this issue Jun 11, 2022 · 1 comment
Closed

(rewriter.flat=false) Refutational unsoundness on simple NIA formula #6091

wintered opened this issue Jun 11, 2022 · 1 comment

Comments

@wintered
Copy link

9cd3398

$z3release bug.smt2                                                                                
sat
$cvc5 -q bug.smt2 
sat
$z3release rewriter.flat=false bug.smt2 
unsat
$cat bug.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (= 0 (+ b a)))
(assert (= 0 (+ a a (* b a))))
(assert (= (= 0 b) (forall ((a Int)) (= a 1))))
(check-sat)
@wintered wintered changed the title (rewriter.flat) Refutational unsoundness on simple NIA formula (rewriter.flat=false) Refutational unsoundness on simple NIA formula Jun 11, 2022
@NikolajBjorner
Copy link
Contributor

fixed by 33754c252288b590d6d4bacdacfe641cfc099cbb

NikolajBjorner added a commit that referenced this issue Jun 14, 2022
@NikolajBjorner
fix #6091
04f94d8
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
@NikolajBjorner @wintered