Z3 solver - Unsatisfiable model values

0
votes

Z3 can output the model and we can extract the values when the input is satisfiable.

Is there a way to obtain values for our model when we want unsatisfiability? (note: I'm using the c++ API)

Another way to see this question: when z3 proves that the equations return false, can we print a combination that lead to that unsat (false) value?

1
z3solver
What is your goal? If it's unsat, it means all combinations lead to that unsat. Is "unsat core" what you're after? – GManNickG
@GManNickG To my understanding, an unsat core will try to provide which conditions are in conflict but, what I'm trying to see is if I can get a model that contains an example (with actual numbers), so let's say we have s.add( x > 2) and s.add(x < 2) then a possible unsat model would be a model output such as (define-fun x () Int 0) which satisfies x < 2 – Anna K.

1 Answers

2
votes

If your input is unsat, no assignment to inputs will make it true, i.e., all assignments will lead to false. So, you can just pick arbitrary values for your inputs.

From a practical perspective, however, one easy way to achieve what you want is to assert the negation of your original goal and ask for a model of that from the solver. The model that "satisfies" the negation of your goal will make your original goal "false."