python - なぜZ3はこれで落ちるのですか？

Question

z3-solverを使用してこれを解決しようとし
ていますが、間違った値が返されるという問題があります。値の変更で置き換えようとしましたが、どれも正しいもので
はありませんが、の値は16進数でなければならないこと はわかっています 。に設定すると、それは>>LShR
w0x41414141
w0x41414141unsat

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]))