1#! /usr/bin/env python3
2
3import z3
4
5x = z3.Real('x')
6y = z3.Real('y')
7z = z3.Real('z')
8s = z3.Solver()
9
10s.add(3 * x + 2 * y - z == 1)
11s.add(2 * x - 2 * y + 4 * z == -2)
12s.add(-x + y / 2 - z == 0)
13
14check = s.check()
15model = s.model()
16
17print(check)
18print(model)
19
20assert check == z3.sat
21assert model[x] == 1 and model[y] == -2 and model[z] == -2
22