CODEWITHSUNDEEP
mathz3smtz3pytheorem
yokke
yokke

Reputation: 99

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?

Upvotes: 0

Views: 338

Answers (1)

alias
alias

Reputation: 30428

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]

Upvotes: 1

Related Questions