enumerating possibles expression values with z3

poc-enumerate.py

from z3 import *

selector = BitVec('selector', 32)
expr = 107 + 4 * (selector % 16)
codesize = 128

s = Solver()
s.add(expr < codesize)

possible_jump_table_values = set([])

while True:
    print(f"checking assertions [{', '.join([str(c) for c in s.assertions()])}]")
    result = s.check()
    print(f"result: {result}")

    if result != sat:
        break

    model  = s.model()
    jump_table_value = model.evaluate(expr).as_long()
    possible_jump_table_values.add(jump_table_value)

    # make sure we get a different expr value next time
    s.add(expr != jump_table_value)

print(f"possible jump table values: {possible_jump_table_values}")