import z3
x,y,z = z3.Reals('x y z')
s = z3.Solver()
s.add(x + y == z)
print(z3.get_version_string())
print(s.solve_for([x]))
# s.solve_for1(x) This is in the python API but seems to be calling a nonexistant function 
# NameError: name 'Z3_solver_solve_for1' is not defined