#!/usr/bin/env python3

from z3 import *

s=Solver()
x,y,z=Ints('x y z')
s.add(x==2)
s.add(y==3)
s.add(z==x+y)
print (s.check())
print (s.model())