Jasper Yu says to YSITD from z3 import * x = Int('x') s = Solver() s.add(x > 0) s.check() m = s.model() print m[x]