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()

sat
[x = 0]

sat
[x = 2]