YSITD_TG_Bot says to #ysitd <seadog007>: from z3 import * x = Int('x') s = Solver() s.add(x > 0) s.check() m = s.model() print m[x]