#!/usr/bin/env python2

from pwn import *
from z3 import *

fd = open("./Crackme_6.exe", "rb")

data = fd.read()[0x1400:0x1490]

d = []
for x in range(0, 0x90, 4):
    d.append(u32(data[x:x+4]))
print d

s = Solver()

a = [ [ BitVec("a_%s_%s" % (i, j), 8) for j in range(6) ]
      for i in range(6) ]

b = [ [ 0 for j in range(6) ]
      for i in range(6) ]

for i in range(6):
    for j in range(6):
        b[j][i] = a[i][j]

c = [ [ 0 for j in range(6) ]
      for i in range(6) ]

for i in range(6):
    for j in range(6):
        for k in range(6):
            c[i][j] += a[i][k]*b[k][j]

for k in range(27):
    j = k%6
    i = k/6
    s.add(And(a[i][j] < 0x7f, a[i][j] >= 47))

for i in range(6):
    for j in range(6):
       s.add(c[i][j] == d[i*6+j])

for k in range(27, 36):
    j = k%6
    i = k/6
    s.add(a[i][j]==1)

s.add(a[0][0] == ord("w"))
s.add(a[0][1] == ord("h"))
s.add(a[0][2] == ord("c"))
s.add(a[0][3] == ord("t"))
s.add(a[0][4] == ord("f"))
s.add(a[0][5] == ord("{"))

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

# print A["a_1_1"]
A ={
"a_4_1" : 104,
"a_2_4" : 48,
"a_3_5" : 52,
"a_1_2" : 117,
"a_2_0" : 51,
"a_2_3" : 48,
"a_1_1" : 48,
"a_2_5" : 100,
"a_2_1" : 95,
"a_1_3" : 95,
"a_3_2" : 55,
"a_3_3" : 95,
"a_3_4" : 109,
"a_1_0" : 89,
"a_4_0" : 116,
"a_2_2" : 103,
"a_3_1" : 97,
"a_1_5" : 114,
"a_1_4" : 97,
"a_3_0" : 95,
"a_4_2" : 125,
"a_0_5" : 123,
"a_0_4" : 102,
"a_0_3" : 116,
"a_0_2" : 99,
"a_0_1" : 104,
"a_0_0" : 119,
"a_5_5" : 1,
"a_5_4" : 1,
"a_5_3" : 1,
"a_5_2" : 1,
"a_5_1" : 1,
"a_5_0" : 1,
"a_4_5" : 1,
"a_4_4" : 1,
"a_4_3" : 1}


res = []
for i in range(6):
    for j in range(6):
        res.append(A["a_%s_%s"%(i, j)])

print "".join(chr(x) for x in res)