21 lines
364 B

# coding: utf-8
from z3 import *
# Create an instance of a z3 solver
solver = Solver()
min_ite = BitVec("min", 32)
x = BitVec("x", 32)
y = BitVec("y", 32)
# Declare additional z3 variables
solver.add(min_ite == If(x < y, x, y))
# solver.add(...)
# Check and print the result.
result = solver.check()
print(result)
if result == sat:
print(solver.model())