Z3 Get Stuck

[raudipra]

Hi everyone,
I am new to z3 and need your help on explaining why my z3 solver got stuck on code below. I generated the function output using "expected seed" and runs z3 solver to reverse-calculate that expected seed, but somehow it got stuck. Any clue?

#!/usr/bin/python3
import z3

solver = z3.Solver()

seed = z3.BitVec("seed", 64)
seed_solution = 123 # z3 should be able to solve this number
multiplier = 25214903917
addend = 11
mask = (1 << 48) - 1
bits = 32 # integer size

len_sequence = 5
sequence = []
for i in range(len_sequence):
    seed_solution = (seed_solution * multiplier + addend) & mask
    sequence.append(seed_solution >> 48 - bits)

for i in range(len(sequence)-1):
    seed = z3.Int2BV(z3.BV2Int(seed) * multiplier + addend, 64) & mask
    value = z3.BV2Int(z3.LShR(seed, (48-bits)))
    solver.add(sequence[i] == value)

print("Before Stuck")
print(solver.check()) # Get stuck here
if solver.check() == z3.sat:
    model = solver.model()

    states = {}
    for state in model.decls():
        states[state.__str__()] = model[state]

    print(states)

    seed0 = states["seed"].as_long()

    seed0 = (seed0 * multiplier + addend) & mask
    next_value = z3.LShR(state0, 48 - bits)
    
    print(next_value)
    print(sequence[-1])

[Notselwyn]

Hi everyone, I am new to z3 and need your help on explaining why my z3 solver got stuck on code below. I generated the function output using "expected seed" and runs z3 solver to reverse-calculate that expected seed, but somehow it got stuck. Any clue?

BV2Int and Int2BV is very expensive (IIRC, it means losing tracking info). try using

for i in range(len(sequence)-1):
-    seed = z3.Int2BV(z3.BV2Int(seed) * multiplier + addend, 64) & mask
+    seed = (seed * multiplier + addend, 64) & mask
-    value = z3.BV2Int(z3.LShR(seed, (48-bits)))
+    value = z3.LShR(seed, (48 - bits))
    solver.add(sequence[i] == value)