# coding: utf-8
import os, sys
from z3 import *

# Create an instance of a z3 solver
solver = Solver()
# Declare z3 variables for the needed BitVectors

min_ite = BitVec(...)

solver.add(min_ite == If(x < y, x, y))



# Check and print the result.
result = solver.check()
print(result)
if result == sat:
    print(solver.model())