z3_solver_integer_constraints_satisfiability_check.py

1from z3 import *
2
3# Create integer variables
4x = Int('x')
5y = Int('y')
6
7# Create a solver instance
8s = Solver()
9
10# Add constraints: x > 2, y < 10, x + 2*y == 7
11s.add(x > 2)
12s.add(y < 10)
13s.add(x + 2*y == 7)
14
15# Check if the constraints are satisfiable
16print(s.check())
17
18# Fetch and print the model (the solution)
19print(s.model())