This script
from z3 import *
solver = z3.Solver()
x = Int('x')
def f(y):
return y+y
solver.add(x >= 0, x < 10, Exists(x, f(x) == 4) )
print solver.check()
print solver.model()
gives me
sat
[x = 0]
as an answer. This is not what I want or expect. As an answer I would like to see
sat
[x = 2]
I found two other posts going in a similar direction((Z3Py) declaring function and Quantifier in Z3), but something doesn't work out.
How do you use the existantial quantifier in this case to get an adequate answer?
The existential binds a different x whose scope is limited to the body of the formula. Hence, your constraints are effectively (0 ≤ x < 10) ∧ (∃ x' . f(x') == 4). Both conjuncts are satisfied by a model in which x = 0; in particular, the second conjunct is satisfied in this model because x' could be 2.
It seems that you want to constrain x further, not only by the inequality. Try the following (not tested)
solver.add(x >= 0, x < 10, f(x) == 4)
and then print the model.