import z3

ANS = [0x48, 0x5f, 0x36, 0x35, 0x35, 0x25, 0x14, 0x2c, 0x1d, 0x1, 0x3, 0x2d, 0xc, 0x6f, 0x35, 0x61, 0x7e, 0x34, 0xa, 0x44, 0x24, 0x2c, 0x4a, 0x46, 0x19, 0x59, 0x5b, 0xe, 0x78, 0x74, 0x29, 0x13, 0x2c]
COUNT=len(ANS)


a1 = [ z3.BitVec('a%d'%i,8) for i in range(COUNT) ]
s = z3.Solver()
s.add(a1[0] == ord('p'))
s.add(a1[1] == ord('c'))
s.add(a1[2] == ord('t'))
s.add(a1[3] == ord('f'))
s.add(a1[4] == ord('{'))

v2 = 80
for i in range(1337):
   for j in range(COUNT):
      a1[j] ^= v2;
      v2 ^= a1[j]

for i in range(COUNT):
   s.add(a1[i] == ANS[i])

print s.check()
model = s.model()
print model

print a1[-1].__class__
print model[0].as_int()
#flag = [ model[a1[i]].as_int() for i in range(4,COUNT) ]
#print flag