Why Z3 falling at this?

Question

i'm trying to solve this using z3-solver
but the proplem is that it gives me wrong values
i tried to replace the >> with LShR the values changes but non of them is corrent
however i know the value of w should be 0x41414141 in hex
i also tried to set w to 0x41414141 and it said that it's unsat

from z3 import *
def F(w):
    return ((w * 31337) ^ (w * 1337 >> 16)) % 2**32

s = Solver()
w = BitVec("w",32)
s.add ( F(w) == F(0x41414141))

while s.check() == sat:
     print s.model()
     s.add(Or(w != s.model()[w]))

Possible duplicate of [Why this z3 equation is failing?](https://stackoverflow.com/questions/49281487/why-this-z3-equation-is-failing) — alias, Apr 03 '18 at 00:26

score 1 · Accepted Answer · answered Apr 02 '18 at 19:52

Python uses arbitrary-size integers, whereas z3 clamps all intermediate results to 32 bits, so F gives different results for Python and z3. You'd need something like

def F1(w):
    return ((w * 31337) ^ (((w * 1337) & 0xffffffff) >> 16)) % 2**32
def F1Z(w):
    return ((w * 31337) ^ LShR(((w * 1337) & 0xffffffff), 16)) % 2**32

s.add ( F1Z(w) == F1(0x41414141))

Why Z3 falling at this?

1 Answers1