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?
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]