Search code examples
mathz3smtz3pytheorem

In Z3Py, prove returns no counterexample

How can Z3 return a valid counterexample? The following code

from z3 import *
set_param(proof=True)
x = Real('x')
f = ForAll(x, x * x > 0)
prove(f)

outputs counterexample [].

I don't have to use prove, but I want to find a valid counterexample to a formula like f in the example. How can I do it?

Solution

  • To get a model, you should really use check, and assert the negation of your formula in a solver context:

    from z3 import *

s = Solver()
x = Real('x')
f = x * x > 0

# Add negation of our formula
# So, if it's not valid, we'll get a model
s.add(Not(f))

print s.check()
print s.model()

    This produces:

    sat
[x = 0]