import z3 orig_flag = [z3.Int(f"f{i}") for i in range(36)] s = z3.Solver() for f in orig_flag: s.add(f >= 32) s.add(f <= 126) s.add(orig_flag[0] == ord('b')) s.add(orig_flag[1] == ord('c')) s.add(orig_flag[2] == ord('t')) s.add(orig_flag[3] == ord('f')) s.add(orig_flag[4] == ord('{')) s.add(orig_flag[-1] == ord('}')) flag = list(orig_flag) def assign(flag, idx, expr, solver): flag[idx] = expr solver.add(expr >= 0) def assign2(flag, idx, expr, solver): flag[idx] = expr solver.add(expr == 0) # 0x40161e assign(flag, 26, flag[26] - flag[13], s) # 0x40162d assign(flag, 30, flag[30] + 218, s) # 0x401646 assign(flag, 28, flag[28] - flag[20], s) # 0x40165c assign(flag, 29, flag[29] + flag[28], s) # 0x40166f assign(flag, 14, flag[14] - flag[17], s) # 0x40167e assign(flag, 16, flag[16] + flag[8], s) # 0x401691 assign(flag, 26, flag[26] + flag[24], s) # 0x40169c assign(flag, 8, flag[8] - flag[20], s) # 0x4016a8 assign(flag, 22, flag[22] * 231, s) # 0x4016b4 assign(flag, 3, flag[3] * 427, s) # 0x4016c7 assign(flag, 14, flag[14] + flag[28], s) # 0x4016d3 assign(flag, 2, flag[2] + 122, s) # 0x4016e6 assign(flag, 10, flag[10] + flag[29], s) # 0x4016f8 assign(flag, 17, flag[17] - flag[8], s) # 0x40170e assign(flag, 6, flag[6] - flag[17], s) # 0x40171a assign(flag, 4, flag[4] * 385, s) # 0x40172d assign(flag, 24, flag[24] - flag[28], s) # 0x401739 assign(flag, 6, flag[6] * 271, s) # 0x40174c assign(flag, 29, flag[29] - flag[11], s) # 0x401758 assign(flag, 35, flag[35] + 225, s) # 0x401764 assign(flag, 1, flag[1] * 441, s) # 0x40176c assign(flag, 7, flag[7] + 295, s) # 0x401778 assign(flag, 6, flag[6] + 283, s) # 0x401784 assign(flag, 5, flag[5] * 251, s) # 0x401790 assign(flag, 16, flag[16] + 455, s) # 0x40179b assign(flag, 7, flag[7] + flag[8], s) # 0x4017b1 assign(flag, 34, flag[34] + flag[21], s) # 0x4017c3 assign(flag, 33, flag[33] - flag[20], s) # 0x4017d6 assign(flag, 26, flag[26] - flag[24], s) # 0x4017e9 assign(flag, 22, flag[22] + flag[18], s) # 0x4017f8 assign(flag, 8, flag[8] - flag[28], s) # 0x40180b assign(flag, 30, flag[30] - flag[2], s) # 0x401821 assign(flag, 33, flag[33] - flag[11], s) # 0x401834 assign(flag, 9, flag[9] + flag[31], s) # 0x401843 assign(flag, 21, flag[21] + 117, s) # 0x401852 assign(flag, 7, flag[7] - flag[15], s) # 0x40185e assign(flag, 18, flag[18] + 344, s) # 0x40186a assign(flag, 24, flag[24] + 315, s) # 0x401880 assign(flag, 15, flag[15] + flag[9], s) # 0x401892 assign(flag, 8, flag[8] + flag[15], s) # 0x4018a5 assign(flag, 22, flag[22] + flag[32], s) # 0x4018b1 assign(flag, 19, flag[19] + 457, s) # 0x4018c4 assign(flag, 19, flag[19] - flag[13], s) # 0x4018d0 assign(flag, 2, flag[2] + 159, s) # 0x4018dc assign(flag, 15, flag[15] + -134, s) # 0x4018ef assign(flag, 35, flag[35] - flag[0], s) # 0x401902 assign(flag, 2, flag[2] - flag[13], s) # 0x401915 assign(flag, 28, flag[28] - flag[11], s) # 0x401921 assign(flag, 24, flag[24] + -215, s) # 0x401934 assign(flag, 3, flag[3] + flag[12], s) # 0x401940 assign(flag, 29, flag[29] + -112, s) # 0x401953 assign(flag, 21, flag[21] - flag[30], s) # 0x40195f assign(flag, 17, flag[17] + 254, s) # 0x401972 assign(flag, 17, flag[17] - flag[13], s) # 0x401981 assign(flag, 26, flag[26] + flag[8], s) # 0x40198d assign(flag, 27, flag[27] + 339, s) # 0x4019a0 assign(flag, 28, flag[28] - flag[33], s) # 0x4019ac assign(flag, 29, flag[29] * 183, s) # 0x4019bb assign(flag, 30, flag[30] + flag[7], s) # 0x4019c7 assign(flag, 27, flag[27] * 101, s) # 0x4019da assign(flag, 5, flag[5] - flag[21], s) # 0x4019e6 assign(flag, 27, flag[27] + 262, s) # 0x4019f5 assign(flag, 20, flag[20] - flag[28], s) # 0x401a04 assign(flag, 23, flag[23] + flag[20], s) # 0x401a17 assign(flag, 2, flag[2] - flag[25], s) # 0x401a23 assign(flag, 14, flag[14] * 363, s) # 0x401a2f assign(flag, 1, flag[1] + -500, s) # 0x401a42 assign(flag, 2, flag[2] + flag[26], s) # 0x401a55 assign(flag, 29, flag[29] - flag[15], s) # 0x401a5d assign(flag, 7, flag[7] + -288, s) # 0x401a70 assign(flag, 13, flag[13] - flag[33], s) # 0x401a7c assign(flag, 16, flag[16] + -141, s) # 0x401a8f assign(flag, 1, flag[1] + flag[29], s) # 0x401a9b assign(flag, 24, flag[24] + 278, s) # 0x401aa7 assign(flag, 31, flag[31] + 283, s) # 0x401abd assign(flag, 26, flag[26] - flag[12], s) # 0x401ad0 assign(flag, 0, flag[0] - flag[28], s) # 0x401ae3 assign(flag, 17, flag[17] + flag[1], s) # 0x401afc assign(flag, 31, flag[31] - flag[26], s) # 0x401b12 assign(flag, 29, flag[29] + flag[4], s) # 0x401b21 assign(flag, 16, flag[16] - flag[8], s) # 0x401b34 assign(flag, 21, flag[21] - flag[32], s) # 0x401b47 assign(flag, 19, flag[19] + flag[10], s) # 0x401b5a assign(flag, 18, flag[18] + flag[34], s) # 0x401b70 assign(flag, 30, flag[30] - flag[31], s) # 0x401b7f assign(flag, 4, flag[4] + 352, s) # 0x401b8e assign(flag, 20, flag[20] + flag[12], s) # 0x401b9a assign(flag, 9, flag[9] + -113, s) # 0x401bad assign(flag, 25, flag[25] + flag[14], s) # 0x401bb9 assign(flag, 30, flag[30] + -219, s) # 0x401bc8 assign(flag, 8, flag[8] - flag[28], s) # 0x401bd7 assign(flag, 22, flag[22] + flag[8], s) # 0x401bed assign(flag, 24, flag[24] - flag[21], s) # 0x401c00 assign(flag, 24, flag[24] + flag[25], s) # 0x401c0c assign(flag, 6, flag[6] + 231, s) # 0x401c18 assign(flag, 16, flag[16] + 343, s) # 0x401c2e assign(flag, 34, flag[34] + flag[12], s) # 0x401c3d assign(flag, 29, flag[29] + flag[7], s) # 0x401c50 assign(flag, 9, flag[9] + flag[2], s) # 0x401c66 assign(flag, 23, flag[23] + flag[34], s) # 0x401c72 assign(flag, 31, flag[31] + 110, s) # 0x401c81 assign(flag, 7, flag[7] + flag[9], s) # 0x401c8d assign(flag, 10, flag[10] + -127, s) # 0x401c99 assign(flag, 3, flag[3] + -469, s) # 0x401cac assign(flag, 5, flag[5] - flag[0], s) # 0x401cb8 assign(flag, 1, flag[1] + -129, s) # 0x401cce assign(flag, 10, flag[10] - flag[21], s) # 0x401ce1 assign(flag, 10, flag[10] - flag[33], s) # 0x401ced assign(flag, 16, flag[16] + -108, s) # 0x401cf5 assign(flag, 7, flag[7] + -386, s) # 0x401cfd assign(flag, 20, flag[20] + 200, s) # 0x401d0f assign(flag, 7, flag[7] + flag[12], s) # 0x401d22 assign(flag, 29, flag[29] + flag[12], s) # 0x401d35 assign(flag, 13, flag[13] - flag[10], s) # 0x401d41 assign(flag, 24, flag[24] + -428, s) # 0x401d54 assign(flag, 9, flag[9] - flag[28], s) # 0x401d63 assign(flag, 17, flag[17] - flag[8], s) # 0x401d6f assign(flag, 35, flag[35] + 374, s) # 0x401d82 assign(flag, 30, flag[30] - flag[21], s) # 0x401d8e assign(flag, 31, flag[31] + 365, s) # 0x401da1 assign(flag, 3, flag[3] - flag[27], s) # 0x401db4 assign(flag, 5, flag[5] - flag[32], s) # 0x401dc0 assign(flag, 23, flag[23] * 110, s) # 0x401dcc assign(flag, 19, flag[19] + -100, s) # 0x401dd4 assign(flag, 8, flag[8] + 214, s) # 0x401ded assign(flag, 32, flag[32] + flag[5], s) # 0x401e06 assign(flag, 16, flag[16] + flag[24], s) # 0x401e18 assign(flag, 32, flag[32] - flag[8], s) # 0x401e2e assign(flag, 0, flag[0] + flag[24], s) # 0x401e44 assign(flag, 11, flag[11] - flag[13], s) # 0x401e57 assign(flag, 35, flag[35] + flag[26], s) # 0x401e69 assign(flag, 16, flag[16] + flag[11], s) # 0x401e75 assign(flag, 18, flag[18] + flag[11], s) # 0x401e8b assign(flag, 3, flag[3] + flag[15], s) # 0x401ea1 assign(flag, 17, flag[17] + flag[10], s) # 0x401eb0 assign(flag, 7, flag[7] + flag[4], s) # 0x401ec9 assign(flag, 17, flag[17] - flag[15], s) # 0x401edc assign(flag, 34, flag[34] + flag[14], s) # 0x401ef5 assign(flag, 11, flag[11] + flag[5], s) # 0x401f01 assign(flag, 25, flag[25] + -143, s) # 0x401f14 assign(flag, 0, flag[0] + flag[15], s) # 0x401f20 assign(flag, 32, flag[32] + 126, s) # 0x401f2c assign(flag, 30, flag[30] + 369, s) # 0x401f38 assign(flag, 26, flag[26] * 161, s) # 0x401f4b assign(flag, 14, flag[14] + flag[10], s) # 0x401f5a assign(flag, 23, flag[23] - flag[7], s) # 0x401f6d assign(flag, 27, flag[27] - flag[18], s) # 0x401f75 assign(flag, 7, flag[7] + -237, s) # 0x401f88 assign(flag, 19, flag[19] - flag[15], s) # 0x401f94 assign(flag, 32, flag[32] + 459, s) # 0x401fa3 assign(flag, 35, flag[35] + flag[7], s) # 0x401faf assign(flag, 9, flag[9] + -210, s) # 0x401fb7 assign(flag, 20, flag[20] + -184, s) # 0x401fca assign(flag, 32, flag[32] - flag[23], s) # 0x401fd6 assign(flag, 12, flag[12] * 311, s) # 0x401fe2 assign(flag, 16, flag[16] + 406, s) # 0x401ff1 assign(flag, 6, flag[6] - flag[8], s) # 0x402000 assign(flag, 31, flag[31] + flag[7], s) # 0x40200c assign(flag, 18, flag[18] + 224, s) # 0x402018 assign(flag, 15, flag[15] + 375, s) # 0x402024 assign(flag, 32, flag[32] + 197, s) # 0x40203a assign(flag, 5, flag[5] - flag[16], s) # 0x40204d assign(flag, 3, flag[3] - flag[9], s) # 0x402060 assign(flag, 33, flag[33] + flag[15], s) # 0x40206f assign(flag, 22, flag[22] + flag[20], s) # 0x402088 assign(flag, 16, flag[16] - flag[2], s) # 0x40209b assign(flag, 32, flag[32] + flag[23], s) # 0x4020b1 assign(flag, 26, flag[26] - flag[13], s) # 0x4020c7 assign(flag, 13, flag[13] - flag[28], s) # 0x4020d6 assign(flag, 2, flag[2] + 488, s) # 0x4020e2 assign(flag, 16, flag[16] + 350, s) # 0x4020f5 assign(flag, 30, flag[30] + flag[5], s) # 0x402104 assign(flag, 35, flag[35] + flag[20], s) # 0x402117 assign(flag, 4, flag[4] + flag[2], s) # 0x402122 assign(flag, 8, flag[8] + flag[20], s) # 0x402131 assign(flag, 7, flag[7] + flag[33], s) # 0x402144 assign(flag, 9, flag[9] + flag[22], s) # 0x402153 assign(flag, 29, flag[29] - flag[20], s) # 0x40215f assign(flag, 13, flag[13] + 273, s) # 0x40216b assign(flag, 16, flag[16] + -303, s) # 0x40217e assign(flag, 9, flag[9] - flag[30], s) # 0x40218d assign(flag, 20, flag[20] - flag[3], s) # 0x40219c assign(flag, 17, flag[17] + flag[8], s) # 0x4021b2 assign(flag, 22, flag[22] - flag[32], s) # 0x4021c1 assign(flag, 0, flag[0] + flag[8], s) # 0x4021d0 assign(flag, 22, flag[22] + 188, s) # 0x4021e6 assign(flag, 31, flag[31] - flag[26], s) # 0x4021f9 assign(flag, 9, flag[9] + flag[0], s) # 0x40220c assign(flag, 33, flag[33] + flag[1], s) # 0x40221b assign(flag, 26, flag[26] + -246, s) # 0x402231 assign(flag, 34, flag[34] - flag[24], s) # 0x402247 assign(flag, 12, flag[12] + flag[34], s) # 0x402253 assign(flag, 32, flag[32] + -162, s) # 0x40225f assign(flag, 1, flag[1] + -118, s) # 0x402272 assign(flag, 14, flag[14] - flag[24], s) # 0x40227e assign(flag, 28, flag[28] + 160, s) # 0x402286 assign(flag, 7, flag[7] + 457, s) # 0x402299 assign(flag, 33, flag[33] + flag[19], s) # 0x4022a5 assign(flag, 29, flag[29] + 237, s) # 0x4022bb assign(flag, 31, flag[31] + flag[22], s) # 0x4022ce assign(flag, 2, flag[2] - flag[18], s) # 0x4022e1 assign(flag, 33, flag[33] + flag[6], s) # 0x4022f0 assign(flag, 11, flag[11] - flag[31], s) # 0x402303 assign(flag, 12, flag[12] + flag[31], s) # 0x40230f assign(flag, 30, flag[30] + 235, s) # 0x40231e assign(flag, 21, flag[21] - flag[20], s) # 0x40232a assign(flag, 23, flag[23] + 219, s) # 0x40233d assign(flag, 13, flag[13] + flag[19], s) # 0x402353 assign(flag, 23, flag[23] + flag[11], s) # 0x402369 assign(flag, 1, flag[1] - flag[23], s) # 0x402375 assign(flag, 30, flag[30] + -113, s) # 0x402381 assign(flag, 19, flag[19] + 297, s) # 0x402390 assign(flag, 0, flag[0] + flag[20], s) # 0x40239c assign(flag, 2, flag[2] * 114, s) # 0x4023a8 assign(flag, 27, flag[27] + -464, s) # 0x4023be assign(flag, 6, flag[6] - flag[10], s) # 0x4023d1 assign(flag, 34, flag[34] + flag[28], s) # 0x4023e0 assign(flag, 6, flag[6] + -294, s) # 0x4023f3 assign(flag, 35, flag[35] + flag[15], s) # 0x4023fb assign(flag, 8, flag[8] + -171, s) # 0x40240d assign(flag, 20, flag[20] - flag[21], s) # 0x40241c assign(flag, 21, flag[21] + 493, s) # 0x402432 assign(flag, 35, flag[35] + flag[28], s) # 0x402445 assign(flag, 22, flag[22] + flag[3], s) # 0x402457 assign(flag, 13, flag[13] + flag[28], s) # 0x40246d assign(flag, 9, flag[9] + flag[13], s) # 0x402483 assign(flag, 2, flag[2] - flag[28], s) # 0x402496 assign(flag, 5, flag[5] + flag[6], s) # 0x4024a2 assign(flag, 25, flag[25] + 235, s) # 0x4024b5 assign(flag, 6, flag[6] - flag[3], s) # 0x4024cb assign(flag, 9, flag[9] - flag[10], s) # 0x4024da assign(flag, 10, flag[10] * 252, s) # 0x4024e6 assign(flag, 2, flag[2] + 400, s) # 0x4024f5 assign(flag, 20, flag[20] + flag[12], s) # 0x4024fd assign(flag, 7, flag[7] + 174, s) # 0x402513 assign(flag, 18, flag[18] - flag[19], s) # 0x402522 assign(flag, 20, flag[20] - flag[21], s) # 0x402538 assign(flag, 24, flag[24] + flag[3], s) # 0x40254a assign(flag, 19, flag[19] + flag[7], s) # 0x40255c assign(flag, 7, flag[7] + flag[3], s) # 0x402572 assign(flag, 12, flag[12] - flag[25], s) # 0x40257e assign(flag, 12, flag[12] + -315, s) # 0x40258a assign(flag, 17, flag[17] + -448, s) # 0x40259d assign(flag, 5, flag[5] - flag[14], s) # 0x4025b3 assign(flag, 3, flag[3] + flag[24], s) # 0x4025c6 assign(flag, 3, flag[3] - flag[30], s) # 0x4025d2 assign(flag, 32, flag[32] + 171, s) # 0x4025e5 assign(flag, 12, flag[12] - flag[18], s) # 0x4025f4 assign(flag, 7, flag[7] - flag[3], s) # 0x402600 assign(flag, 6, flag[6] + -180, s) # 0x40260f assign(flag, 11, flag[11] - flag[8], s) # 0x40261b assign(flag, 0, flag[0] + 241, s) # 0x402627 assign(flag, 17, flag[17] + -197, s) # 0x402633 assign(flag, 19, flag[19] + -405, s) # 0x402646 assign(flag, 31, flag[31] + flag[21], s) # 0x40265f assign(flag, 11, flag[11] - flag[6], s) # 0x402675 assign(flag, 3, flag[3] + flag[11], s) # 0x40268b assign(flag, 22, flag[22] - flag[6], s) # 0x40269e assign(flag, 33, flag[33] - flag[10], s) # 0x4026aa assign(flag, 2, flag[2] + -152, s) # 0x4026bd assign(flag, 21, flag[21] + flag[35], s) # 0x4026c9 assign2(flag, 0, flag[0] + -19947, s) # 0x4026d5 assign2(flag, 1, flag[1] + -36338, s) # 0x4026e1 assign2(flag, 2, flag[2] + -15136, s) # 0x4026ed assign2(flag, 3, flag[3] + -17102, s) # 0x4026f9 assign2(flag, 4, flag[4] + -48722, s) # 0x402705 assign2(flag, 5, flag[5] + -6273, s) # 0x402711 assign2(flag, 6, flag[6] + -1602, s) # 0x402719 assign2(flag, 7, flag[7] + -34918, s) # 0x402721 assign2(flag, 8, flag[8] + -431, s) # 0x40272d assign2(flag, 9, flag[9] + -44585, s) # 0x402739 assign2(flag, 10, flag[10] + -14112, s) # 0x402745 assign2(flag, 11, flag[11] + -2980, s) # 0x402751 assign2(flag, 12, flag[12] + -24712, s) # 0x40275d assign2(flag, 13, flag[13] + -951, s) # 0x402769 assign2(flag, 14, flag[14] + -70, s) # 0x402775 assign2(flag, 15, flag[15] + -467, s) # 0x402781 assign2(flag, 16, flag[16] + -19345, s) # 0x40278d assign2(flag, 17, flag[17] + -43155, s) # 0x402799 assign2(flag, 18, flag[18] + -77, s) # 0x4027a5 assign2(flag, 19, flag[19] + -49333, s) # 0x4027ad assign2(flag, 20, flag[20] + -43705, s) # 0x4027b9 assign2(flag, 21, flag[21] + -49948, s) # 0x4027c5 assign2(flag, 22, flag[22] + -2499, s) # 0x4027d1 assign2(flag, 23, flag[23] + -6665, s) # 0x4027dd assign2(flag, 24, flag[24] + -18970, s) # 0x4027e9 assign2(flag, 25, flag[25] + -19054, s) # 0x4027f5 assign2(flag, 26, flag[26] + -32911, s) # 0x402801 assign2(flag, 27, flag[27] + -41660, s) # 0x40280d assign2(flag, 28, flag[28] + -160, s) # 0x402819 assign2(flag, 29, flag[29] + -47694, s) # 0x402825 assign2(flag, 30, flag[30] + -4956, s) # 0x402831 assign2(flag, 31, flag[31] + -19797, s) # 0x40283d assign2(flag, 32, flag[32] + -24709, s) # 0x402849 assign2(flag, 33, flag[33] + -32229, s) # 0x402855 assign2(flag, 34, flag[34] + -451, s) # 0x402861 assign2(flag, 35, flag[35] + -49449, s) res = s.check() print(res) if res == z3.sat: model = s.model() print("satisfiable") result = ''.join([chr(model.eval(c).as_long()) for c in orig_flag]) print(result)