Source

z3 / examples / python / example.py

Full commit
1
2
3
4
5
6
7
8
from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print s.check()
print s.model()