Z3: how to encode If-the-else in Z3 python?

python, z3

Solution

You'll need Z3's `If` function:

def z3py.If   (       a,
          b,
          c,
          ctx = None 
  )

Create a Z3 if-then-else expression.

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)

(from here)

Problem

I want to encode If-the-else in Z3 python, but cannot find any docs or sample on how to do that. I have a sample code like below. ``` F = True tmp = BitVec('tmp', 1) tmp1 = BitVec('tmp1', 8) ``` Now how can I encode this condition into F: ``` if tmp == 1, then tmp1 == 100. otherwise, tmp1 == 0 ``` Thanks so much.

Original source