Z3Py solver from brute force script

I am working on a reverse-engineering challenge, the program takes a 32 bits hex number as input and do a serie of equations using a keyword, if the final result is 0 then the input is valid otherwise the input is wrong.

I wrote a python brute force script that tries every value from 0x11111111 to 0xffffffff :

username = "skander"

i = 286331153

while i < 4294967295 :  
    hash = i
    print("Testing : %s") % (hex(hash))
    for c in username :
        hash = hash >> 27 | (hash ^ ord(c)) << 5
        hash = hash & 0xffffffff        
        hash = hash ^ (hash << 8)
        hash = hash & 0xffffffff 

    if hash == 0 :
        print("****** FOUND ******")
        print(hex(i))
        break
    else :
        i = i + 1

After some attempts, the script gave me the correct value ( 61aebf45 )

I wanted to implement a more elegant way with z3Py and I tried the following script :

from z3 import *


hash = BitVec('hash', 32)


s = Solver()

eq1 = ( hash >> 27 | ((hash ^ ord('s')) << 5))  & 0xffffffff  
eq2 = ( eq1 ^ (eq1 << 8)) & 0xffffffff 

eq3 = ( eq2 >> 27 | ((eq2 ^ ord('k')) << 5))  & 0xffffffff
eq4 = ( eq3 ^ (eq3 << 8)) & 0xffffffff

eq5 = ( eq4 >> 27 | ((eq4 ^ ord('a')) << 5))  & 0xffffffff
eq6 = ( eq5 ^ (eq5 << 8)) & 0xffffffff

eq7 = ( eq6 >> 27 | ((eq6 ^ ord('n')) << 5))  & 0xffffffff
eq8 = ( eq7 ^ (eq7 << 8)) & 0xffffffff

eq9 = ( eq8 >> 27 | ((eq8 ^ ord('d')) << 5))  & 0xffffffff
eq10 = ( eq9 ^ (eq9 << 8)) & 0xffffffff

eq11 = ( eq10 >> 27 | ((eq10 ^ ord('e')) << 5))  & 0xffffffff
eq12 = ( eq11 ^ (eq11 << 8)) & 0xffffffff

eq13 = ( eq12 >> 27 | ((eq12 ^ ord('r')) << 5))  & 0xffffffff
eq14 = ( eq13 ^ (eq13 << 8)) & 0xffffffff


s.add(eq14 == 0)
while s.check() == sat:
    m = s.model()
    print(m[hash])
    s.add(Or(hash != s.model()[hash]))

But no output (unsat problem) and if I modify

hash = BitVec('hash', 32)

to

hash = BitVec('hash', 64)

The script give me a lot of models

Is the problem not solvable or I did a mistake on the code ?

>> translates to arithmetic shift-right; but what you actually meant was logical-shift right. Use LShR instead. That is, replace all instances of:

hash >> 27

with

LShR(hash, 27)

If you do this, it prints 1638842181 which is the value you seem to be looking for.

Note that you don't have to "unroll" the loop yourself; you can just walk over the input string and code this just like you did the original Python; simply keep assigning to the same symbolic value.