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
:smtlib2_compliant
unknown
For the attached benchmark, z3 currently produces unknown.
However, if I comment out the first line in it, which is merely:
(set-option :smtlib2_compliant true)
then I get a sat answer.
sat
I'm curious why there's this discrepancy; I thought the compliance only impacted what subset of smtlib2 was accepted, not how the solver behaved.
Furthermore, this seems to be a regression since z3 compiled on August 27 of this year produces sat on this benchmark.
compliant_unknown.txt
The text was updated successfully, but these errors were encountered:
589024a
fix #6969
3726960
Signed-off-by: Nikolaj Bjorner <[email protected]>
fix #6969, again
160971d
No branches or pull requests
For the attached benchmark, z3 currently produces
unknown
.However, if I comment out the first line in it, which is merely:
then I get a
sat
answer.I'm curious why there's this discrepancy; I thought the compliance only impacted what subset of smtlib2 was accepted, not how the solver behaved.
Furthermore, this seems to be a regression since z3 compiled on August 27 of this year produces
sat
on this benchmark.compliant_unknown.txt
The text was updated successfully, but these errors were encountered: