p = Int('p')
q = Int('q')
s = Solver()
s.add(1<=p<=9, 1<=q<=19, 5<(3*p-4*q)<10)
s.check()
print s.model()
returns sat, and gives the solution
[p = 0, q = 0]
which does not satisfy the constraints. If I remove the final constraint, it returns a sensible pair that satisfies the first two (trivial) constraints. What's going on?
Permalink to try this online: http://rise4fun.com/Z3Py/fk4
EDIT : I'm new to z3, so there's a chance I'm doing something horribly wrong, do let me know.