
When the result is unsat, it is possible to give some counterexamples? And how to do that?


Coordinator
Feb 13, 2013 at 3:58 PM

We say a formula is unsatisfiable when it does not have any model/solution. Similarly, we say a formula is satisfiable when it has a model/solution.
In Z3, to prove that a fomula F is valid (i.e., it is true in any interpretation), we show that its negation is unsatisfiable.
So, a counterexample is a model/solution for the negation of F. Note that, in this case the negation of F is sat.
Models and counterexamples are associated with satisfiable instances.
For unsatisfiable instances, Z3 can produce a proof or extract unsatisfiable cores.

