You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
21 lines
364 B
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())
|