from z3 import *

### from png extract zip, for example using stegsolve,
### zip contains a file name STMFD SP!, {R11,LR}, with a 2 hex numbers per line
### decode it as address and arm code, load it in IDA,decompile and transform to following 
### set of equations.


inp = [BitVec('a%d'%i,8) for i in range(16)]

sol_0 = 32 * inp[14]  + -55 * inp[13]+ -55 * inp[15]+ -83 * inp[10]+ 27 * inp[9]+ -26 * inp[12]+ -100 * inp[11]+ -32 * inp[0]+ 46 * inp[2]+ 97 * inp[1]+ 67 * inp[4]+ 45 * inp[3]+ -73 * inp[6]+ 79 * inp[5]+ -5 * inp[8]+ -13 * inp[7]
  
sol_1 = 6 * inp[14]+ 89 * inp[13]+ 84 * inp[15]+ 15 * inp[10]+ -76 * inp[9]+ 85 * inp[12]+ 72 * inp[11]+ -31 * inp[0]+ 20 * inp[2]+ -90 * inp[1]+ -89 * inp[4]+ -66 * inp[3]+ -73 * inp[6]+ -64 * inp[5]+ 87 * inp[8]+ 26 * inp[7]
  
sol_2 = 83 * inp[14]+ -7 * inp[13]+ 57 * inp[15]+ 27 * inp[10]+ 14 * inp[9]+ -42 * inp[12]+ 92 * inp[11]+ 78 * inp[0]+ 94 * inp[2]+ 22 * inp[1]+ 34 * inp[4]+ 75 * inp[3]+ 61 * inp[6]+ 31 * inp[5]+ 100 * inp[8]+ -16 * inp[7];
  
sol_3 = 96 * inp[14]+ -89 * inp[13]+ -27 * inp[15]+ 76 * inp[10]+ -68 * inp[9]+ 48 * inp[12]+ 72 * inp[11]+ 43 * inp[0]+ 75 * inp[2]+ 44 * inp[1]+ -17 * inp[4]+ -59 * inp[3]- inp[6]+ 82 * inp[5]+ 47 * inp[8]+ -44 * inp[7];
  
sol_4 = 42 * inp[14]+ 89 * inp[13]+ -97 * inp[15]+ 24 * inp[10]+ -33 * inp[9]+ 62 * inp[12]+ 84 * inp[11]+ 44 * inp[0]+ 87 * inp[2]+ -60 * inp[1]+ 57 * inp[4]+ -64 * inp[3]+ -60 * inp[6]+ -18 * inp[5]+ -81 * inp[8]+ 9 * inp[7]
  
sol_5 = 89 * inp[14]+ -97 * inp[13]+ 79 * inp[15]+ -57 * inp[10]+ 54 * inp[9]+ 48 * inp[12]+ 59 * inp[11]+ 30 * inp[0]+ 23 * inp[2]+ 68 * inp[1]+ 46 * inp[4]+ 91 * inp[3]+ -62 * inp[6]+ 32 * inp[5]+ -5 * inp[8]+ 42 * inp[7]
  
sol_6 = 62 * inp[14]+ 9 * inp[13]+ -97 * inp[15]+ -99 * inp[10]+ -86 * inp[9]+ -10 * inp[12]+ -57 * inp[11]+ -29 * inp[0]+ 14 * inp[2]+ -14 * inp[1]+ -60 * inp[4]+ -89 * inp[3]+ 49 * inp[6]+ 11 * inp[5]+ 75 * inp[8]+ -79 * inp[7]
  
sol_7 = 31 * inp[14]+ 6 * inp[13]+ -69 * inp[15]+ -81 * inp[10]+ 83 * inp[9]+ 97 * inp[12]+ 80 * inp[11]+ 58 * inp[0]+ 17 * inp[2]+ 58 * inp[1]+ -98 * inp[4]+ 91 * inp[3]+ -5 * inp[6]+ -75 * inp[5]+ -26 * inp[8]+ -60 * inp[7]
  
sol_8 = 19 * inp[14]- inp[13]+ 73 * inp[15]+ -4 * inp[10]+ 26 * inp[9]+ -43 * inp[12]+ -27 * inp[11]+ -21 * inp[0]+ 62 * inp[2]+ -11 * inp[1]+ 84 * inp[4]+ -77 * inp[3]+ 49 * inp[6]+ -86 * inp[5]- inp[8]+ -66 * inp[7]
  
sol_9 = 42 * inp[14]+ -75 * inp[13]+ 35 * inp[15]+ -23 * inp[10]+ -60 * inp[9]+ -51 * inp[12]+ 68 * inp[11]+ 83 * inp[0]+ 77 * inp[2]+ 43 * inp[1]+ 83 * inp[4]+ 96 * inp[3]+ 26 * inp[6]+ -20 * inp[5]+ -89 * inp[8]+ -7 * inp[7]
  
sol_10 = 45 * inp[14]+ 14 * inp[13]+ -91 * inp[15]+ 48 * inp[10]+ 50 * inp[9]+ -52 * inp[12]+ 58 * inp[11]+ 74 * inp[0]+ 73 * inp[2]+ 58 * inp[1]+ -100 * inp[4]+ -86 * inp[3]+ 12 * inp[6]+ 71 * inp[5]+ 69 * inp[8]+ 66 * inp[7]
  
sol_11 = 30 * inp[14]+ -27 * inp[13]+ 8 * inp[15]+ -41 * inp[10]+ -90 * inp[9]+ 48 * inp[12]+ -74 * inp[11]+ -60 * inp[0]+ 26 * inp[2]+ -61 * inp[1]+ 20 * inp[4]+ -31 * inp[3]+ -53 * inp[6]+ -59 * inp[5]+ 68 * inp[8]+ 72 * inp[7]
  
sol_12 = 25 * inp[14]+ -12 * inp[13]+ -34 * inp[15]+ -35 * inp[10]+ 98 * inp[9]+ 7 * inp[12]+ -76 * inp[11]+ -26 * inp[0]+ 31 * inp[2]+ 19 * inp[1]+ -95 * inp[4]+ -16 * inp[3]+ (inp[6] << 6)+ 33 * inp[5]+ 10 * inp[8]+ -83 * inp[7]
  
sol_13 = 51 * inp[14]+ 4 * inp[13]+ -6 * inp[15]+ 71 * inp[10]+ -16 * inp[9]+ 75 * inp[12]+ 16 * inp[11]+ -89 * inp[0]+ -40 * inp[2]+ 61 * inp[1]+ 20 * inp[4]+ -67 * inp[3]+ 27 * inp[6]+ 42 * inp[5]+ 38 * inp[8]+ -37 * inp[7]
    
sol_14 = 96 * inp[14]+ 38 * inp[13]+ 82 * inp[15]+ (inp[10] << 6)+ 91 * inp[9]+ 7 * inp[12]+ 39 * inp[11]+ 32 * inp[0]+ -92 * inp[2]+ 57 * inp[1]+ 40 * inp[4]+ -47 * inp[3]+ -21 * inp[6]+ -54 * inp[5]+ -14 * inp[8]+ -25 * inp[7]
  
sol_15 = 84 * inp[14]+ -31 * inp[13]+ 100 * inp[15]+ -54 * inp[10]+ 16 * inp[9]+ -96 * inp[12]+ -53 * inp[11]+ -56 * inp[0]+ 55 * inp[2]+ -6 * inp[1]+ -6 * inp[4]+ 42 * inp[3]+ -37 * inp[6]+ -38 * inp[5]+ (inp[8] << 6)+ -27 * inp[7];


s = Solver()  

s.add( sol_0 == -7026)
s.add( sol_1 == -2645)
s.add(  sol_2 == 53442)
s.add(  sol_3 == 20609)
s.add(  sol_4 == 8630)
s.add(  sol_5 == 27564)
s.add(  sol_6 == -27078)
s.add(  sol_7 == 15265)
s.add(  sol_8 == -12183)
s.add( sol_9 == 17452)
s.add( sol_10 == 31435)
s.add( sol_11 == -23099)
s.add( sol_12 == -8136)
s.add( sol_13 == 13019)
s.add( sol_14 == 20430)
s.add( sol_15 == -12714)

print s.check()
m=s.model()
r=[]
for i in inp:
   r.append( chr(m[i].as_long()))
print ''.join(r)