from z3 import * x = [BitVec("x%d" % i, 8) for i in range(15)] res = x[:] op = [0x0000000A, 0x00000004, 0x00000010, 0x00000008, 0x00000003, 0x00000005, 0x00000001, 0x00000004, 0x00000020, 0x00000008, 0x00000005, 0x00000003, 0x00000001, 0x00000003, 0x00000002, 0x00000008, 0x0000000B, 0x00000001, 0x0000000C, 0x00000008, 0x00000004, 0x00000004, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000003, 0x00000021, 0x00000001, 0x0000000B, 0x00000008, 0x0000000B, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000051, 0x00000008, 0x00000004, 0x00000024, 0x00000001, 0x0000000C, 0x00000008, 0x0000000B, 0x00000001, 0x00000005, 0x00000002, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000002, 0x00000036, 0x00000008, 0x00000004, 0x00000041, 0x00000001, 0x00000002, 0x00000020, 0x00000008, 0x00000005, 0x00000001, 0x00000001, 0x00000005, 0x00000003, 0x00000008, 0x00000002, 0x00000025, 0x00000001, 0x00000004, 0x00000009, 0x00000008, 0x00000003, 0x00000020, 0x00000001, 0x00000002, 0x00000041, 0x00000008, 0x0000000C, 0x00000001, 0x00000007, 0x00000022, 0x00000007, 0x0000003F, 0x00000007, 0x00000034, 0x00000007, 0x00000032, 0x00000007, 0x00000072, 0x00000007, 0x00000033, 0x00000007, 0x00000018, 0x00000007, 0xFFFFFFA7, 0x00000007, 0x00000031, 0x00000007, 0xFFFFFFF1, 0x00000007, 0x00000028, 0x00000007, 0xFFFFFF84, 0x00000007, 0xFFFFFFC1, 0x00000007, 0x0000001E, 0x00000007, 0x0000007A] s = Solver()
index = 0 j = 0 t = 0 check_num = [0 for i in range(100)] check_numi = 0 check_numj = 0
ip = 0 while (ip < len(op)): if op[ip] == 1: check_num[check_numi] = t ip += 1 index += 1 check_numi += 1 elif op[ip] == 2: t = x[index]+op[ip+1] ip += 2 elif op[ip] == 3: t = x[index]-op[ip+1] ip += 2 elif op[ip] == 4: t = x[index] ^ op[ip+1] ip += 2 elif op[ip] == 5: t = x[index]*op[ip+1] ip += 2 elif op[ip] == 6: ip += 1 elif op[ip] == 7: s.add(check_num[check_numj] == op[ip+1]) check_numj += 1 ip += 2 elif op[ip] == 8: x[j] = t j += 1 ip += 1 elif op[ip] == 10: ip += 1 elif op[ip] == 11: t = x[index] - 1 ip += 1 elif op[ip] == 12: t = x[index] + 1 ip += 1
if s.check() == sat: m = s.model() flag = "" print(m) for i in res: flag += chr(m[i].as_long()) print(flag)
|