We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
Hi, On the latest nightly build z3-seq gives wrong answer on the following file:
qf_s.smt2.zip
All the formulas at every level in the assertion stack are satisfiable.
$ /z3-nightly/bin/z3 qf_s.smt2 sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat
While z3str3 and CVC4 return:
sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat
OS: NAME="Ubuntu" VERSION="16.04.5 LTS (Xenial Xerus)" ID=ubuntu ID_LIKE=debian PRETTY_NAME="Ubuntu 16.04.5 LTS" VERSION_ID="16.04"
The text was updated successfully, but these errors were encountered:
Fixed, seems #2860 was a duplicate of this
Sorry, something went wrong.
No branches or pull requests
Hi,
On the latest nightly build z3-seq gives wrong answer on the following file:
qf_s.smt2.zip
All the formulas at every level in the assertion stack are satisfiable.
$ /z3-nightly/bin/z3 qf_s.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
unsat
While z3str3 and CVC4 return:
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
OS:
NAME="Ubuntu"
VERSION="16.04.5 LTS (Xenial Xerus)"
ID=ubuntu
ID_LIKE=debian
PRETTY_NAME="Ubuntu 16.04.5 LTS"
VERSION_ID="16.04"
The text was updated successfully, but these errors were encountered: