#!/usr/bin/env python3
from z3 import *
x = Real('x')
y = Real('y')
eq1 = x + y == 5
eq2 = x - y == 3
s = Solver()
s.add(eq1, eq2)
if s.check() == sat:
print("Solution:", s.model())
else:
print("No solution found")