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.

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 setting makes the benchmark unknown #6969

Closed
LeventErkok opened this issue Oct 30, 2023 · 0 comments
Closed

:smtlib2_compliant setting makes the benchmark unknown #6969

LeventErkok opened this issue Oct 30, 2023 · 0 comments

Comments

@LeventErkok
Copy link

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.

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

NikolajBjorner added a commit that referenced this issue Oct 30, 2023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner added a commit that referenced this issue Oct 30, 2023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant