paper_stack.py

from z3 import *

def C03011(Qml5):
	C12d =0
	for Po4M in Qml5:
		C12d = (31 * C12d + (Po4M)) & 0xFFFFFFFF
	return ((C12d + 0x80000000) & 0xFFFFFFFF) - 0X80000000


username = [BitVec('u' + str(i), 32) for i in range(6)]

s = Solver()
s.add(C03011(username) == -1133886720)

for u in username:
    s.add(u >= 0x20)
    s.add(u < 0x7f)

s.add(username[0] != 109) # uncomment to find a password

s.check()

m = s.model()

print ''.join([chr(int(str(m[u]))) for u in username])

# username: m(tm6b
# password: lGtkuC