from z3 import *

#定义类型
x = Int('x')
y = Int('y')
z = Int('z')

#创建求解器
s = Solver()

#添加约束条件
s.add(y==2*x-7)
s.add(5*x+3*y+2*z==3)
s.add(3*x+z==7)

print s.check()  #检测条件是否OK   
print s.model()  #列出求解结果
sat  #列出求解满足条件值