Closed
Description
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.
Metadata
Metadata
Assignees
Labels
No labels