2k
Categories: re
2021-07-12
by not_really
nc mc.ax 31361
Author: EvilMuffinHa
Files: 2k prog.bin prog.bin disassembly
nc mc.ax 31361
Author: EvilMuffinHa
Files: 2k prog.bin prog.bin disassembly
There’s not really much to say here other than it’s a really simple vm.
Instructions:
0x01: dupStack
push(stack[-1])
0x03: exit
return pop
0x10: addStack
push(pop + pop)
0x11: subStack
push(pop - pop)
0x12: mulStack
push(pop * pop)
0x13:
push(pop / pop)
0x14:
push(pop % pop)
0x15: mulModStack
c = pop
b = pop
a = pop
push((a * b) % c)
0x16: eqozStack
if (stack[-1] == stack[-2])
stack[-2] = 1
else
stack[-2] = 0
pop
0x17: negzStack
if (stack[-1] == 0) stack[-1] = -1
0x20: getc
0x21: printc
0x22: pushShort
push(a0)
0x30: uncJmp
jmp(pop)
0x31: eqzJmp
if (stack[-2] == 0) jmp(stack[-1])
0x32: neqJmp
if (stack[-2] != 0) jmp(stack[-1])
0x40: setMem
mem[cx] = pop
0x41: getMem
push(mem[cx])
0x50: ecxPlus1
cx++
0x51: ecxMins1
cx--
0x52: addCx
cx += pop
0x53: subCx
cx -= pop
I wrote a script to read prog.bin and it just takes the input and does a bunch of checks on it, jumping if a check fails. You can see the disassembly in the files above.
f = open("prog.bin", "rb")
while True:
ba = f.read(1)
if not ba:
break
b = ba[0]
usingArg = False
name = "idklol"
pos = f.tell()
if b == 0x01:
#push(stack[-1])
name = "dupStack"
elif b == 0x03:
#return pop
name = "exit"
elif b == 0x10:
#push(pop + pop)
name = "addStack"
elif b == 0x11:
#push(pop - pop)
name = "subStack"
elif b == 0x12:
#push(pop * pop)
name = "mulStack"
elif b == 0x13:
#push(pop / pop)
name = "divStack"
elif b == 0x14:
#push(pop % pop)
name = "modStack"
elif b == 0x15:
#c = pop
#b = pop
#a = pop
#push((a * b) % c)
name = "mulModStack"
elif b == 0x16:
#if (stack[-1] == stack[-2]) stack[-2] = 1 else stack[-2] = 0 pop
name = "eqozStack"
elif b == 0x17:
#if (stack[-1] == 0) stack[-1] = -1
name = "negzStack"
elif b == 0x20:
name = "getc"
elif b == 0x21:
name = "printChar"
elif b == 0x22:
#push(arg)
usingArg = True
arg = f.read(2)[0]
name = "pushShort"
elif b == 0x30:
#jmp(pop)
name = "uncJmp\n"
elif b == 0x31:
#if (stack[-2] == 0) jmp(stack[-1])
name = "eqzJmp\n"
elif b == 0x32:
#if (stack[-2] != 0) jmp(stack[-1])
name = "neqJmp\n"
elif b == 0x40:
#note: mem has words, not bytes
#mem[cx] = pop
name = "setMem"
elif b == 0x41:
#push(mem[cx])
name = "getMem"
elif b == 0x50:
#cx++
name = "ecxPlus1"
elif b == 0x51:
#cx--
name = "ecxMins1"
elif b == 0x52:
#cx += pop
name = "addCx"
elif b == 0x53:
#cx -= pop
name = "subCx"
if (usingArg):
print(f"{str(pos).zfill(8)} {hex(b)[2:].zfill(2)} {name} {arg}");
else:
print(f"{str(pos).zfill(8)} {hex(b)[2:].zfill(2)} {name}");
To make this solvable in z3, I created a script to emulate the stack and print it whenever a jmp was reached.
from z3 import *
mem = [BitVec(f'{i}', 32) for i in range(64)]
s = Solver()
for i in range(64):
s.add(mem[i] >= 0)
s.add(mem[i] <= 70) #idk close enough
def add(a, b):
return a + b
def sub(a, b):
return a - b
def mul(a, b):
return a * b
def div(a, b):
return a / b
def mod(a, b):
return a % b
def compEq(a, b):
if a == b:
return 1
else:
return 0
def compNz(a):
return -1
s.add(sub(mem[0], mem[1]) != 0)
s.add(sub(mem[0], mem[8]) != 0)
s.add(sub(mem[0], mem[2]) != 0)
s.add(sub(mem[0], mem[16]) != 0)
s.add(sub(mem[1], mem[2]) != 0)
s.add(sub(mem[8], mem[16]) != 0)
s.add(sub(mem[0], mem[3]) != 0)
s.add(sub(mem[0], mem[24]) != 0)
s.add(sub(mem[1], mem[3]) != 0)
s.add(sub(mem[8], mem[24]) != 0)
s.add(sub(mem[2], mem[3]) != 0)
s.add(sub(mem[16], mem[24]) != 0)
s.add(sub(mem[0], mem[4]) != 0)
s.add(sub(mem[0], mem[32]) != 0)
s.add(sub(mem[1], mem[4]) != 0)
s.add(sub(mem[8], mem[32]) != 0)
s.add(sub(mem[2], mem[4]) != 0)
s.add(sub(mem[16], mem[32]) != 0)
s.add(sub(mem[3], mem[4]) != 0)
s.add(sub(mem[24], mem[32]) != 0)
s.add(sub(mem[0], mem[5]) != 0)
s.add(sub(mem[0], mem[40]) != 0)
s.add(sub(mem[1], mem[5]) != 0)
s.add(sub(mem[8], mem[40]) != 0)
s.add(sub(mem[2], mem[5]) != 0)
s.add(sub(mem[16], mem[40]) != 0)
s.add(sub(mem[3], mem[5]) != 0)
s.add(sub(mem[24], mem[40]) != 0)
s.add(sub(mem[4], mem[5]) != 0)
s.add(sub(mem[32], mem[40]) != 0)
s.add(sub(mem[0], mem[6]) != 0)
s.add(sub(mem[0], mem[48]) != 0)
s.add(sub(mem[1], mem[6]) != 0)
s.add(sub(mem[8], mem[48]) != 0)
s.add(sub(mem[2], mem[6]) != 0)
s.add(sub(mem[16], mem[48]) != 0)
s.add(sub(mem[3], mem[6]) != 0)
s.add(sub(mem[24], mem[48]) != 0)
s.add(sub(mem[4], mem[6]) != 0)
s.add(sub(mem[32], mem[48]) != 0)
s.add(sub(mem[5], mem[6]) != 0)
s.add(sub(mem[40], mem[48]) != 0)
s.add(sub(mem[0], mem[7]) != 0)
s.add(sub(mem[0], mem[56]) != 0)
s.add(sub(mem[1], mem[7]) != 0)
s.add(sub(mem[8], mem[56]) != 0)
s.add(sub(mem[2], mem[7]) != 0)
s.add(sub(mem[16], mem[56]) != 0)
s.add(sub(mem[3], mem[7]) != 0)
s.add(sub(mem[24], mem[56]) != 0)
s.add(sub(mem[4], mem[7]) != 0)
s.add(sub(mem[32], mem[56]) != 0)
s.add(sub(mem[5], mem[7]) != 0)
s.add(sub(mem[40], mem[56]) != 0)
s.add(sub(mem[6], mem[7]) != 0)
s.add(sub(mem[48], mem[56]) != 0)
s.add(sub(mem[8], mem[9]) != 0)
s.add(sub(mem[1], mem[9]) != 0)
s.add(sub(mem[8], mem[10]) != 0)
s.add(sub(mem[1], mem[17]) != 0)
s.add(sub(mem[9], mem[10]) != 0)
s.add(sub(mem[9], mem[17]) != 0)
s.add(sub(mem[8], mem[11]) != 0)
s.add(sub(mem[1], mem[25]) != 0)
s.add(sub(mem[9], mem[11]) != 0)
s.add(sub(mem[9], mem[25]) != 0)
s.add(sub(mem[10], mem[11]) != 0)
s.add(sub(mem[17], mem[25]) != 0)
s.add(sub(mem[8], mem[12]) != 0)
s.add(sub(mem[1], mem[33]) != 0)
s.add(sub(mem[9], mem[12]) != 0)
s.add(sub(mem[9], mem[33]) != 0)
s.add(sub(mem[10], mem[12]) != 0)
s.add(sub(mem[17], mem[33]) != 0)
s.add(sub(mem[11], mem[12]) != 0)
s.add(sub(mem[25], mem[33]) != 0)
s.add(sub(mem[8], mem[13]) != 0)
s.add(sub(mem[1], mem[41]) != 0)
s.add(sub(mem[9], mem[13]) != 0)
s.add(sub(mem[9], mem[41]) != 0)
s.add(sub(mem[10], mem[13]) != 0)
s.add(sub(mem[17], mem[41]) != 0)
s.add(sub(mem[11], mem[13]) != 0)
s.add(sub(mem[25], mem[41]) != 0)
s.add(sub(mem[12], mem[13]) != 0)
s.add(sub(mem[33], mem[41]) != 0)
s.add(sub(mem[8], mem[14]) != 0)
s.add(sub(mem[1], mem[49]) != 0)
s.add(sub(mem[9], mem[14]) != 0)
s.add(sub(mem[9], mem[49]) != 0)
s.add(sub(mem[10], mem[14]) != 0)
s.add(sub(mem[17], mem[49]) != 0)
s.add(sub(mem[11], mem[14]) != 0)
s.add(sub(mem[25], mem[49]) != 0)
s.add(sub(mem[12], mem[14]) != 0)
s.add(sub(mem[33], mem[49]) != 0)
s.add(sub(mem[13], mem[14]) != 0)
s.add(sub(mem[41], mem[49]) != 0)
s.add(sub(mem[8], mem[15]) != 0)
s.add(sub(mem[1], mem[57]) != 0)
s.add(sub(mem[9], mem[15]) != 0)
s.add(sub(mem[9], mem[57]) != 0)
s.add(sub(mem[10], mem[15]) != 0)
s.add(sub(mem[17], mem[57]) != 0)
s.add(sub(mem[11], mem[15]) != 0)
s.add(sub(mem[25], mem[57]) != 0)
s.add(sub(mem[12], mem[15]) != 0)
s.add(sub(mem[33], mem[57]) != 0)
s.add(sub(mem[13], mem[15]) != 0)
s.add(sub(mem[41], mem[57]) != 0)
s.add(sub(mem[14], mem[15]) != 0)
s.add(sub(mem[49], mem[57]) != 0)
s.add(sub(mem[16], mem[17]) != 0)
s.add(sub(mem[2], mem[10]) != 0)
s.add(sub(mem[16], mem[18]) != 0)
s.add(sub(mem[2], mem[18]) != 0)
s.add(sub(mem[17], mem[18]) != 0)
s.add(sub(mem[10], mem[18]) != 0)
s.add(sub(mem[16], mem[19]) != 0)
s.add(sub(mem[2], mem[26]) != 0)
s.add(sub(mem[17], mem[19]) != 0)
s.add(sub(mem[10], mem[26]) != 0)
s.add(sub(mem[18], mem[19]) != 0)
s.add(sub(mem[18], mem[26]) != 0)
s.add(sub(mem[16], mem[20]) != 0)
s.add(sub(mem[2], mem[34]) != 0)
s.add(sub(mem[17], mem[20]) != 0)
s.add(sub(mem[10], mem[34]) != 0)
s.add(sub(mem[18], mem[20]) != 0)
s.add(sub(mem[18], mem[34]) != 0)
s.add(sub(mem[19], mem[20]) != 0)
s.add(sub(mem[26], mem[34]) != 0)
s.add(sub(mem[16], mem[21]) != 0)
s.add(sub(mem[2], mem[42]) != 0)
s.add(sub(mem[17], mem[21]) != 0)
s.add(sub(mem[10], mem[42]) != 0)
s.add(sub(mem[18], mem[21]) != 0)
s.add(sub(mem[18], mem[42]) != 0)
s.add(sub(mem[19], mem[21]) != 0)
s.add(sub(mem[26], mem[42]) != 0)
s.add(sub(mem[20], mem[21]) != 0)
s.add(sub(mem[34], mem[42]) != 0)
s.add(sub(mem[16], mem[22]) != 0)
s.add(sub(mem[2], mem[50]) != 0)
s.add(sub(mem[17], mem[22]) != 0)
s.add(sub(mem[10], mem[50]) != 0)
s.add(sub(mem[18], mem[22]) != 0)
s.add(sub(mem[18], mem[50]) != 0)
s.add(sub(mem[19], mem[22]) != 0)
s.add(sub(mem[26], mem[50]) != 0)
s.add(sub(mem[20], mem[22]) != 0)
s.add(sub(mem[34], mem[50]) != 0)
s.add(sub(mem[21], mem[22]) != 0)
s.add(sub(mem[42], mem[50]) != 0)
s.add(sub(mem[16], mem[23]) != 0)
s.add(sub(mem[2], mem[58]) != 0)
s.add(sub(mem[17], mem[23]) != 0)
s.add(sub(mem[10], mem[58]) != 0)
s.add(sub(mem[18], mem[23]) != 0)
s.add(sub(mem[18], mem[58]) != 0)
s.add(sub(mem[19], mem[23]) != 0)
s.add(sub(mem[26], mem[58]) != 0)
s.add(sub(mem[20], mem[23]) != 0)
s.add(sub(mem[34], mem[58]) != 0)
s.add(sub(mem[21], mem[23]) != 0)
s.add(sub(mem[42], mem[58]) != 0)
s.add(sub(mem[22], mem[23]) != 0)
s.add(sub(mem[50], mem[58]) != 0)
s.add(sub(mem[24], mem[25]) != 0)
s.add(sub(mem[3], mem[11]) != 0)
s.add(sub(mem[24], mem[26]) != 0)
s.add(sub(mem[3], mem[19]) != 0)
s.add(sub(mem[25], mem[26]) != 0)
s.add(sub(mem[11], mem[19]) != 0)
s.add(sub(mem[24], mem[27]) != 0)
s.add(sub(mem[3], mem[27]) != 0)
s.add(sub(mem[25], mem[27]) != 0)
s.add(sub(mem[11], mem[27]) != 0)
s.add(sub(mem[26], mem[27]) != 0)
s.add(sub(mem[19], mem[27]) != 0)
s.add(sub(mem[24], mem[28]) != 0)
s.add(sub(mem[3], mem[35]) != 0)
s.add(sub(mem[25], mem[28]) != 0)
s.add(sub(mem[11], mem[35]) != 0)
s.add(sub(mem[26], mem[28]) != 0)
s.add(sub(mem[19], mem[35]) != 0)
s.add(sub(mem[27], mem[28]) != 0)
s.add(sub(mem[27], mem[35]) != 0)
s.add(sub(mem[24], mem[29]) != 0)
s.add(sub(mem[3], mem[43]) != 0)
s.add(sub(mem[25], mem[29]) != 0)
s.add(sub(mem[11], mem[43]) != 0)
s.add(sub(mem[26], mem[29]) != 0)
s.add(sub(mem[19], mem[43]) != 0)
s.add(sub(mem[27], mem[29]) != 0)
s.add(sub(mem[27], mem[43]) != 0)
s.add(sub(mem[28], mem[29]) != 0)
s.add(sub(mem[35], mem[43]) != 0)
s.add(sub(mem[24], mem[30]) != 0)
s.add(sub(mem[3], mem[51]) != 0)
s.add(sub(mem[25], mem[30]) != 0)
s.add(sub(mem[11], mem[51]) != 0)
s.add(sub(mem[26], mem[30]) != 0)
s.add(sub(mem[19], mem[51]) != 0)
s.add(sub(mem[27], mem[30]) != 0)
s.add(sub(mem[27], mem[51]) != 0)
s.add(sub(mem[28], mem[30]) != 0)
s.add(sub(mem[35], mem[51]) != 0)
s.add(sub(mem[29], mem[30]) != 0)
s.add(sub(mem[43], mem[51]) != 0)
s.add(sub(mem[24], mem[31]) != 0)
s.add(sub(mem[3], mem[59]) != 0)
s.add(sub(mem[25], mem[31]) != 0)
s.add(sub(mem[11], mem[59]) != 0)
s.add(sub(mem[26], mem[31]) != 0)
s.add(sub(mem[19], mem[59]) != 0)
s.add(sub(mem[27], mem[31]) != 0)
s.add(sub(mem[27], mem[59]) != 0)
s.add(sub(mem[28], mem[31]) != 0)
s.add(sub(mem[35], mem[59]) != 0)
s.add(sub(mem[29], mem[31]) != 0)
s.add(sub(mem[43], mem[59]) != 0)
s.add(sub(mem[30], mem[31]) != 0)
s.add(sub(mem[51], mem[59]) != 0)
s.add(sub(mem[32], mem[33]) != 0)
s.add(sub(mem[4], mem[12]) != 0)
s.add(sub(mem[32], mem[34]) != 0)
s.add(sub(mem[4], mem[20]) != 0)
s.add(sub(mem[33], mem[34]) != 0)
s.add(sub(mem[12], mem[20]) != 0)
s.add(sub(mem[32], mem[35]) != 0)
s.add(sub(mem[4], mem[28]) != 0)
s.add(sub(mem[33], mem[35]) != 0)
s.add(sub(mem[12], mem[28]) != 0)
s.add(sub(mem[34], mem[35]) != 0)
s.add(sub(mem[20], mem[28]) != 0)
s.add(sub(mem[32], mem[36]) != 0)
s.add(sub(mem[4], mem[36]) != 0)
s.add(sub(mem[33], mem[36]) != 0)
s.add(sub(mem[12], mem[36]) != 0)
s.add(sub(mem[34], mem[36]) != 0)
s.add(sub(mem[20], mem[36]) != 0)
s.add(sub(mem[35], mem[36]) != 0)
s.add(sub(mem[28], mem[36]) != 0)
s.add(sub(mem[32], mem[37]) != 0)
s.add(sub(mem[4], mem[44]) != 0)
s.add(sub(mem[33], mem[37]) != 0)
s.add(sub(mem[12], mem[44]) != 0)
s.add(sub(mem[34], mem[37]) != 0)
s.add(sub(mem[20], mem[44]) != 0)
s.add(sub(mem[35], mem[37]) != 0)
s.add(sub(mem[28], mem[44]) != 0)
s.add(sub(mem[36], mem[37]) != 0)
s.add(sub(mem[36], mem[44]) != 0)
s.add(sub(mem[32], mem[38]) != 0)
s.add(sub(mem[4], mem[52]) != 0)
s.add(sub(mem[33], mem[38]) != 0)
s.add(sub(mem[12], mem[52]) != 0)
s.add(sub(mem[34], mem[38]) != 0)
s.add(sub(mem[20], mem[52]) != 0)
s.add(sub(mem[35], mem[38]) != 0)
s.add(sub(mem[28], mem[52]) != 0)
s.add(sub(mem[36], mem[38]) != 0)
s.add(sub(mem[36], mem[52]) != 0)
s.add(sub(mem[37], mem[38]) != 0)
s.add(sub(mem[44], mem[52]) != 0)
s.add(sub(mem[32], mem[39]) != 0)
s.add(sub(mem[4], mem[60]) != 0)
s.add(sub(mem[33], mem[39]) != 0)
s.add(sub(mem[12], mem[60]) != 0)
s.add(sub(mem[34], mem[39]) != 0)
s.add(sub(mem[20], mem[60]) != 0)
s.add(sub(mem[35], mem[39]) != 0)
s.add(sub(mem[28], mem[60]) != 0)
s.add(sub(mem[36], mem[39]) != 0)
s.add(sub(mem[36], mem[60]) != 0)
s.add(sub(mem[37], mem[39]) != 0)
s.add(sub(mem[44], mem[60]) != 0)
s.add(sub(mem[38], mem[39]) != 0)
s.add(sub(mem[52], mem[60]) != 0)
s.add(sub(mem[40], mem[41]) != 0)
s.add(sub(mem[5], mem[13]) != 0)
s.add(sub(mem[40], mem[42]) != 0)
s.add(sub(mem[5], mem[21]) != 0)
s.add(sub(mem[41], mem[42]) != 0)
s.add(sub(mem[13], mem[21]) != 0)
s.add(sub(mem[40], mem[43]) != 0)
s.add(sub(mem[5], mem[29]) != 0)
s.add(sub(mem[41], mem[43]) != 0)
s.add(sub(mem[13], mem[29]) != 0)
s.add(sub(mem[42], mem[43]) != 0)
s.add(sub(mem[21], mem[29]) != 0)
s.add(sub(mem[40], mem[44]) != 0)
s.add(sub(mem[5], mem[37]) != 0)
s.add(sub(mem[41], mem[44]) != 0)
s.add(sub(mem[13], mem[37]) != 0)
s.add(sub(mem[42], mem[44]) != 0)
s.add(sub(mem[21], mem[37]) != 0)
s.add(sub(mem[43], mem[44]) != 0)
s.add(sub(mem[29], mem[37]) != 0)
s.add(sub(mem[40], mem[45]) != 0)
s.add(sub(mem[5], mem[45]) != 0)
s.add(sub(mem[41], mem[45]) != 0)
s.add(sub(mem[13], mem[45]) != 0)
s.add(sub(mem[42], mem[45]) != 0)
s.add(sub(mem[21], mem[45]) != 0)
s.add(sub(mem[43], mem[45]) != 0)
s.add(sub(mem[29], mem[45]) != 0)
s.add(sub(mem[44], mem[45]) != 0)
s.add(sub(mem[37], mem[45]) != 0)
s.add(sub(mem[40], mem[46]) != 0)
s.add(sub(mem[5], mem[53]) != 0)
s.add(sub(mem[41], mem[46]) != 0)
s.add(sub(mem[13], mem[53]) != 0)
s.add(sub(mem[42], mem[46]) != 0)
s.add(sub(mem[21], mem[53]) != 0)
s.add(sub(mem[43], mem[46]) != 0)
s.add(sub(mem[29], mem[53]) != 0)
s.add(sub(mem[44], mem[46]) != 0)
s.add(sub(mem[37], mem[53]) != 0)
s.add(sub(mem[45], mem[46]) != 0)
s.add(sub(mem[45], mem[53]) != 0)
s.add(sub(mem[40], mem[47]) != 0)
s.add(sub(mem[5], mem[61]) != 0)
s.add(sub(mem[41], mem[47]) != 0)
s.add(sub(mem[13], mem[61]) != 0)
s.add(sub(mem[42], mem[47]) != 0)
s.add(sub(mem[21], mem[61]) != 0)
s.add(sub(mem[43], mem[47]) != 0)
s.add(sub(mem[29], mem[61]) != 0)
s.add(sub(mem[44], mem[47]) != 0)
s.add(sub(mem[37], mem[61]) != 0)
s.add(sub(mem[45], mem[47]) != 0)
s.add(sub(mem[45], mem[61]) != 0)
s.add(sub(mem[46], mem[47]) != 0)
s.add(sub(mem[53], mem[61]) != 0)
s.add(sub(mem[48], mem[49]) != 0)
s.add(sub(mem[6], mem[14]) != 0)
s.add(sub(mem[48], mem[50]) != 0)
s.add(sub(mem[6], mem[22]) != 0)
s.add(sub(mem[49], mem[50]) != 0)
s.add(sub(mem[14], mem[22]) != 0)
s.add(sub(mem[48], mem[51]) != 0)
s.add(sub(mem[6], mem[30]) != 0)
s.add(sub(mem[49], mem[51]) != 0)
s.add(sub(mem[14], mem[30]) != 0)
s.add(sub(mem[50], mem[51]) != 0)
s.add(sub(mem[22], mem[30]) != 0)
s.add(sub(mem[48], mem[52]) != 0)
s.add(sub(mem[6], mem[38]) != 0)
s.add(sub(mem[49], mem[52]) != 0)
s.add(sub(mem[14], mem[38]) != 0)
s.add(sub(mem[50], mem[52]) != 0)
s.add(sub(mem[22], mem[38]) != 0)
s.add(sub(mem[51], mem[52]) != 0)
s.add(sub(mem[30], mem[38]) != 0)
s.add(sub(mem[48], mem[53]) != 0)
s.add(sub(mem[6], mem[46]) != 0)
s.add(sub(mem[49], mem[53]) != 0)
s.add(sub(mem[14], mem[46]) != 0)
s.add(sub(mem[50], mem[53]) != 0)
s.add(sub(mem[22], mem[46]) != 0)
s.add(sub(mem[51], mem[53]) != 0)
s.add(sub(mem[30], mem[46]) != 0)
s.add(sub(mem[52], mem[53]) != 0)
s.add(sub(mem[38], mem[46]) != 0)
s.add(sub(mem[48], mem[54]) != 0)
s.add(sub(mem[6], mem[54]) != 0)
s.add(sub(mem[49], mem[54]) != 0)
s.add(sub(mem[14], mem[54]) != 0)
s.add(sub(mem[50], mem[54]) != 0)
s.add(sub(mem[22], mem[54]) != 0)
s.add(sub(mem[51], mem[54]) != 0)
s.add(sub(mem[30], mem[54]) != 0)
s.add(sub(mem[52], mem[54]) != 0)
s.add(sub(mem[38], mem[54]) != 0)
s.add(sub(mem[53], mem[54]) != 0)
s.add(sub(mem[46], mem[54]) != 0)
s.add(sub(mem[48], mem[55]) != 0)
s.add(sub(mem[6], mem[62]) != 0)
s.add(sub(mem[49], mem[55]) != 0)
s.add(sub(mem[14], mem[62]) != 0)
s.add(sub(mem[50], mem[55]) != 0)
s.add(sub(mem[22], mem[62]) != 0)
s.add(sub(mem[51], mem[55]) != 0)
s.add(sub(mem[30], mem[62]) != 0)
s.add(sub(mem[52], mem[55]) != 0)
s.add(sub(mem[38], mem[62]) != 0)
s.add(sub(mem[53], mem[55]) != 0)
s.add(sub(mem[46], mem[62]) != 0)
s.add(sub(mem[54], mem[55]) != 0)
s.add(sub(mem[54], mem[62]) != 0)
s.add(sub(mem[56], mem[57]) != 0)
s.add(sub(mem[7], mem[15]) != 0)
s.add(sub(mem[56], mem[58]) != 0)
s.add(sub(mem[7], mem[23]) != 0)
s.add(sub(mem[57], mem[58]) != 0)
s.add(sub(mem[15], mem[23]) != 0)
s.add(sub(mem[56], mem[59]) != 0)
s.add(sub(mem[7], mem[31]) != 0)
s.add(sub(mem[57], mem[59]) != 0)
s.add(sub(mem[15], mem[31]) != 0)
s.add(sub(mem[58], mem[59]) != 0)
s.add(sub(mem[23], mem[31]) != 0)
s.add(sub(mem[56], mem[60]) != 0)
s.add(sub(mem[7], mem[39]) != 0)
s.add(sub(mem[57], mem[60]) != 0)
s.add(sub(mem[15], mem[39]) != 0)
s.add(sub(mem[58], mem[60]) != 0)
s.add(sub(mem[23], mem[39]) != 0)
s.add(sub(mem[59], mem[60]) != 0)
s.add(sub(mem[31], mem[39]) != 0)
s.add(sub(mem[56], mem[61]) != 0)
s.add(sub(mem[7], mem[47]) != 0)
s.add(sub(mem[57], mem[61]) != 0)
s.add(sub(mem[15], mem[47]) != 0)
s.add(sub(mem[58], mem[61]) != 0)
s.add(sub(mem[23], mem[47]) != 0)
s.add(sub(mem[59], mem[61]) != 0)
s.add(sub(mem[31], mem[47]) != 0)
s.add(sub(mem[60], mem[61]) != 0)
s.add(sub(mem[39], mem[47]) != 0)
s.add(sub(mem[56], mem[62]) != 0)
s.add(sub(mem[7], mem[55]) != 0)
s.add(sub(mem[57], mem[62]) != 0)
s.add(sub(mem[15], mem[55]) != 0)
s.add(sub(mem[58], mem[62]) != 0)
s.add(sub(mem[23], mem[55]) != 0)
s.add(sub(mem[59], mem[62]) != 0)
s.add(sub(mem[31], mem[55]) != 0)
s.add(sub(mem[60], mem[62]) != 0)
s.add(sub(mem[39], mem[55]) != 0)
s.add(sub(mem[61], mem[62]) != 0)
s.add(sub(mem[47], mem[55]) != 0)
s.add(sub(mem[56], mem[63]) != 0)
s.add(sub(mem[7], mem[63]) != 0)
s.add(sub(mem[57], mem[63]) != 0)
s.add(sub(mem[15], mem[63]) != 0)
s.add(sub(mem[58], mem[63]) != 0)
s.add(sub(mem[23], mem[63]) != 0)
s.add(sub(mem[59], mem[63]) != 0)
s.add(sub(mem[31], mem[63]) != 0)
s.add(sub(mem[60], mem[63]) != 0)
s.add(sub(mem[39], mem[63]) != 0)
s.add(sub(mem[61], mem[63]) != 0)
s.add(sub(mem[47], mem[63]) != 0)
s.add(sub(mem[62], mem[63]) != 0)
s.add(sub(mem[55], mem[63]) != 0)
s.add(sub(mul(Int2BV(If((sub(mem[8], mem[0]) == 0), 0xffff, 1), 32), sub(mem[8], mem[0])), 2) == 0)
s.add(sub(mod(mul(mem[1], mod(mul(mem[9], mem[10]), 32767)), 32767), 8) == 0)
s.add(sub(add(mem[3], mem[2]), 12) == 0)
s.add(sub(add(add(mem[6], mem[5]), mem[4]), 17) == 0)
s.add(sub(mod(mul(mem[7], mod(mul(mem[15], mem[23]), 32767)), 32767), 15) == 0)
s.add(sub(mem[11], 7) == 0)
s.add(sub(add(add(mem[28], mem[20]), mem[12]), 7) == 0)
s.add(sub(mem[13], 8) == 0)
s.add(sub(add(mem[22], mem[14]), 12) == 0)
s.add(sub(mul(Int2BV(If((sub(mem[17], mem[16]) == 0), 0xffff, 1), 32), sub(mem[17], mem[16])), 2) == 0)
s.add(sub(mod(mul(mem[18], mod(mul(mem[26], mem[27]), 32767)), 32767), 144) == 0)
s.add(sub(mem[19], 1) == 0)
s.add(sub(mul(Int2BV(If((sub(mem[29], mem[21]) == 0), 0xffff, 1), 32), sub(mem[29], mem[21])), 5) == 0)
s.add(sub(mem[24], 5) == 0)
s.add(sub(mem[25], 3) == 0)
s.add(mul(mod(mem[30], mem[38]), mod(mem[38], mem[30])) == 0)
s.add(sub(div(add(div(mem[30], mem[38]), div(mem[38], mem[30])), add(1, Int2BV(If((mem[38] == mem[30]), 1, 0), 32))), 2) == 0)
s.add(mul(mod(mem[31], mem[39]), mod(mem[39], mem[31])) == 0)
s.add(sub(div(add(div(mem[31], mem[39]), div(mem[39], mem[31])), add(1, Int2BV(If((mem[39] == mem[31]), 1, 0), 32))), 3) == 0)
s.add(sub(mem[32], 1) == 0)
s.add(sub(add(mem[41], mem[33]), 12) == 0)
s.add(sub(mem[34], 4) == 0)
s.add(sub(mod(mul(mem[35], mod(mul(mem[36], mod(mul(mem[37], mem[45]), 32767)), 32767)), 32767), 30) == 0)
s.add(sub(mem[40], 7) == 0)
s.add(mul(mod(mem[42], mem[50]), mod(mem[50], mem[42])) == 0)
s.add(sub(div(add(div(mem[42], mem[50]), div(mem[50], mem[42])), add(1, Int2BV(If((mem[50] == mem[42]), 1, 0), 32))), 3) == 0)
s.add(sub(add(add(mem[59], mem[51]), mem[43]), 15) == 0)
s.add(sub(mem[44], 3) == 0)
s.add(mul(mod(mem[46], mem[54]), mod(mem[54], mem[46])) == 0)
s.add(sub(div(add(div(mem[46], mem[54]), div(mem[54], mem[46])), add(1, Int2BV(If((mem[54] == mem[46]), 1, 0), 32))), 3) == 0)
s.add(mul(mod(mem[47], mem[55]), mod(mem[55], mem[47])) == 0)
s.add(sub(div(add(div(mem[47], mem[55]), div(mem[55], mem[47])), add(1, Int2BV(If((mem[55] == mem[47]), 1, 0), 32))), 2) == 0)
s.add(sub(add(add(mem[57], mem[49]), mem[48]), 12) == 0)
s.add(sub(mul(Int2BV(If((sub(mem[53], mem[52]) == 0), 0xffff, 1), 32), sub(mem[53], mem[52])), 2) == 0)
s.add(sub(mem[56], 2) == 0)
s.add(sub(mem[58], 5) == 0)
s.add(sub(mul(Int2BV(If((sub(mem[61], mem[60]) == 0), 0xffff, 1), 32), sub(mem[61], mem[60])), 2) == 0)
s.add(mul(mod(mem[62], mem[63]), mod(mem[63], mem[62])) == 0)
s.add(sub(div(add(div(mem[62], mem[63]), div(mem[63], mem[62])), add(1, Int2BV(If((mem[63] == mem[62]), 1, 0), 32))), 7) == 0)
print(s.check())
model = s.model()
results = ([int(str(model[mem[i]])) for i in range(len(model))])
pc = ""
for ri in results:
pc += chr(ri + 0x2f)
print(pc)
oB0:;4/2qHt61740OQ7031644281063_0/3O7o1?6;<52k:336V/GIP11048NP6
This can be passed to the netcat thing to print the flag.
flag{kenken_is_just_z3_064c4}