You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Z3 occasionally produces an unsat core that isn't enough to produce unsat. I have the following example, minimised as far as I could from a generated problem:
it's unsat with core (k!10), but if you instead append
(check-sat-assuming (k!10))
it's sat. Note that the actual result Z3 produces is fine, just the unsat core is too small. @CEisenhofer was able to reproduce, and of course I'm happy to help too.
The text was updated successfully, but these errors were encountered:
Z3 occasionally produces an unsat core that isn't enough to produce unsat. I have the following example, minimised as far as I could from a generated problem:
If you append
it's unsat with core
(k!10)
, but if you instead appendit's
sat
. Note that the actual result Z3 produces is fine, just the unsat core is too small. @CEisenhofer was able to reproduce, and of course I'm happy to help too.The text was updated successfully, but these errors were encountered: