Prove a Boolean formula under some Implies conditions in z3py

Question

I'm new in using Z3py, and my assignment is to generate counter examples for both solutions (sat and unsat).
Is there any function to generate counterexample for unsat solution?

Answer 1

unsat means there is no model that satisfies the assertions given. You can only extract a model when the problem is sat. So, to answer your question as you posed it, you cannot create models from an unsat solution: It just does not exist.

A typical approach is to assert the negation of the formula you are trying to prove; and if that formula is satisfiable then your original formula is falsifiable; i.e., there is a counter-example for it. Perhaps that's what you are trying to do? That is: If the negation of the formula has a satisfying model, then that model is a counter-example for the original formula. This is how most provers built on top of SMT solvers work, by sending the negation of what they are trying to prove and getting back unsat. If the prover returns a model, then it is a counter-example.