Search code examples
z3z3py

Z3 How to check whether a model satisfies a new assertion/constraint


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)

Solution

  • 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