[Python] z3 sort mismatch for different bytes of the same variable

I'm simulating the behaviour of an algorithm using z3 python package, however I'm encountering problems using a bitwise XOR.

At first I define

class State:
def __init__(self):
self.state = [0] * 0x270
self.index = 0

def mag(i):
return z3.If(i == 0, 0x0, 0x9908b0df)

seed = z3.BitVec('seed', 32)
s= State()


And the script goes on, however when I run the Solver I get a z3.z3types.Z3Exception: sort mismatch caused by trying to execute the __xor__ in the line

s.state = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state & 0x80000000) >> 1) ^ mag((s.state[1] & 1) *8)


Here every entry in s.state depends on the symbolic value of the seed.

Continue reading...