#!/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")