Z3 counter example for UNSAT problem

Mar 28, 2014 at 7:49 AM
In Parsing of file written in smtLib v2 , by z3

If I am writing

(get-model) in file and if it is unsatisfiable then it is showing error like there is no model ,
but for satisfiable it is giving the model..

So , how I can get counter model for unsatisfiable problem.?
Apr 16, 2014 at 5:19 PM
Edited Apr 16, 2014 at 5:19 PM
The (get-model) command only shows a model if there is one that satisfies the problem, as determined by the last (check-sat) command. For unsatisfiable problems, we can produce unsatisfiable cores (the get-unsat-core command) or proofs (the get-proof command). See also the SMTLIB2 tutorial or the following related questions on stackoverflow: (get-unsat-core) returns empty in Z3, Getting a “good” unsat-core with z3 (logic QF_BV), Counterexample output of Z3