I am using z3py for coding. See the following example.
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x+y>3)
if s.check()==sat:
m = s.model()
# how to check whether model m satisfies x+y<5 ?
print(m)
You can evaluate expressions in the model:
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x+y>3)
if s.check()==sat:
m = s.model()
print(m)
print(m.evaluate(x+y<5))
This prints:
[x = 4, y = 0]
True