#!/usr/bin/env python3

# This is a test that checks that the Python 3 module is functional by
# trying out a small example involving integer logic.

from z3 import *

x, y = Ints("x y")

s = Solver()
s.add(x > 0, y > 0, x <= 2, y <= 2, x + 1 <= y)

assert s.check()

m = s.model()

assert m[x] == 1
assert m[y] == 2