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

Completeness regression on simple nonlinear formula #5349

Closed

wintered opened this issue Jun 16, 2021 · 1 comment

wintered commented Jun 16, 2021

Commit: dc6a8fd
OS: Ubuntu 18.04

$ z3-4.8.10 unknown.smt2
unsat
$ z3 unknown.smt2
unknown
$ cat unknown.smt2
(declare-const x Int)
(assert (forall ((v Int)) (or (= 0 (mod v 2)) (> x (+ 6869 v)))))
(check-sat)

The text was updated successfully, but these errors were encountered:

NikolajBjorner added a commit that referenced this issue


          #5349 #5338

f95d0b7

NikolajBjorner added a commit that referenced this issue


          #5338 #5349

29a2838

Contributor

NikolajBjorner commented Jun 17, 2021

a butterfly, but otherwise added recognizer for mod-a-constant being part of LIA

NikolajBjorner closed this as completed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment