from z3 import *

x = Int('x')
y = Int('y')

s = Solver()
s.add(x + y == 6)
s.add(2 * x == 3* y + 2)

print (s.check())
print (s.model())