>>> from z3 import Int, solve >>> x = Int('x') >>> solve([x > 2, x < 5, x % 2 == 0]) [x = 4]
If anything, this seems to support the original claim.