473 lines
15 KiB
Python
473 lines
15 KiB
Python
import re
|
|
from z3 import *
|
|
|
|
# ==============================================================================
|
|
# 1. RAW DATA (The C++ code you provided)
|
|
# ==============================================================================
|
|
raw_cpp_code = """
|
|
*((_DWORD *)this + 15) = 1;
|
|
*((_DWORD *)this + 16) = 2;
|
|
*((_DWORD *)this + 25) = 2;
|
|
*((_DWORD *)this + 26) = 4;
|
|
*((_DWORD *)this + 27) = 5;
|
|
*((_DWORD *)this + 28) = 3;
|
|
*((_DWORD *)this + 30) = 6;
|
|
*((_DWORD *)this + 31) = 3;
|
|
*((_DWORD *)this + 32) = 3;
|
|
*((_DWORD *)this + 34) = 4;
|
|
*((_DWORD *)this + 37) = 6;
|
|
*((_DWORD *)this + 43) = 4;
|
|
*((_DWORD *)this + 44) = 5;
|
|
*((_DWORD *)this + 46) = 5;
|
|
*((_DWORD *)this + 47) = 6;
|
|
*((_DWORD *)this + 53) = 5;
|
|
*((_DWORD *)this + 56) = 7;
|
|
*((_DWORD *)this + 65) = 10;
|
|
*((_DWORD *)this + 66) = 10;
|
|
*((_DWORD *)this + 67) = 7;
|
|
*((_DWORD *)this + 68) = 8;
|
|
*((_DWORD *)this + 70) = 4;
|
|
*((_DWORD *)this + 71) = 11;
|
|
*((_DWORD *)this + 72) = 9;
|
|
*((_DWORD *)this + 77) = 11;
|
|
*((_DWORD *)this + 81) = 10;
|
|
*((_DWORD *)this + 90) = 6;
|
|
*((_DWORD *)this + 91) = 12;
|
|
*((_DWORD *)this + 92) = 11;
|
|
*((_DWORD *)this + 94) = 12;
|
|
*((_DWORD *)this + 101) = 11;
|
|
*((_DWORD *)this + 103) = 13;
|
|
*((_DWORD *)this + 112) = 16;
|
|
*((_DWORD *)this + 113) = 14;
|
|
*((_DWORD *)this + 122) = 15;
|
|
*((_DWORD *)this + 131) = 16;
|
|
*((_DWORD *)this + 140) = 17;
|
|
*((_DWORD *)this + 142) = 19;
|
|
*((_DWORD *)this + 143) = 19;
|
|
*((_DWORD *)this + 144) = 18;
|
|
*((_DWORD *)this + 149) = 13;
|
|
*((_DWORD *)this + 153) = 21;
|
|
*((_DWORD *)this + 154) = 21;
|
|
*((_DWORD *)this + 155) = 19;
|
|
*((_DWORD *)this + 164) = 20;
|
|
*((_DWORD *)this + 166) = 21;
|
|
*((_DWORD *)this + 173) = 22;
|
|
*((_DWORD *)this + 175) = 21;
|
|
*((_DWORD *)this + 176) = 21;
|
|
*((_DWORD *)this + 177) = 17;
|
|
*((_DWORD *)this + 178) = 21;
|
|
*((_DWORD *)this + 179) = 22;
|
|
*((_DWORD *)this + 188) = 23;
|
|
*((_DWORD *)this + 190) = 25;
|
|
*((_DWORD *)this + 191) = 24;
|
|
*((_DWORD *)this + 197) = 25;
|
|
*((_DWORD *)this + 200) = 25;
|
|
*((_DWORD *)this + 209) = 26;
|
|
*((_DWORD *)this + 218) = 28;
|
|
*((_DWORD *)this + 219) = 27;
|
|
*((_DWORD *)this + 228) = 28;
|
|
*((_DWORD *)this + 230) = 29;
|
|
*((_DWORD *)this + 237) = 28;
|
|
*((_DWORD *)this + 239) = 30;
|
|
*((_DWORD *)this + 248) = 26;
|
|
*((_DWORD *)this + 249) = 30;
|
|
*((_DWORD *)this + 250) = 26;
|
|
*((_DWORD *)this + 251) = 31;
|
|
*((_DWORD *)this + 260) = 32;
|
|
*((_DWORD *)this + 262) = 33;
|
|
*((_DWORD *)this + 269) = 32;
|
|
*((_DWORD *)this + 271) = 35;
|
|
*((_DWORD *)this + 272) = 34;
|
|
*((_DWORD *)this + 281) = 36;
|
|
*((_DWORD *)this + 282) = 37;
|
|
*((_DWORD *)this + 283) = 35;
|
|
*((_DWORD *)this + 292) = 36;
|
|
*((_DWORD *)this + 294) = 37;
|
|
*((_DWORD *)this + 301) = 36;
|
|
*((_DWORD *)this + 303) = 38;
|
|
*((_DWORD *)this + 312) = 39;
|
|
*((_DWORD *)this + 321) = 40;
|
|
*((_DWORD *)this + 330) = 41;
|
|
*((_DWORD *)this + 339) = 41;
|
|
*((_DWORD *)this + 340) = 42;
|
|
*((_DWORD *)this + 342) = 43;
|
|
*((_DWORD *)this + 349) = 45;
|
|
*((_DWORD *)this + 351) = 45;
|
|
*((_DWORD *)this + 352) = 43;
|
|
*((_DWORD *)this + 353) = 46;
|
|
*((_DWORD *)this + 354) = 43;
|
|
*((_DWORD *)this + 355) = 44;
|
|
*((_DWORD *)this + 364) = 45;
|
|
*((_DWORD *)this + 366) = 47;
|
|
*((_DWORD *)this + 367) = 41;
|
|
*((_DWORD *)this + 368) = 46;
|
|
*((_DWORD *)this + 373) = 41;
|
|
*((_DWORD *)this + 377) = 47;
|
|
*((_DWORD *)this + 386) = 49;
|
|
*((_DWORD *)this + 387) = 48;
|
|
*((_DWORD *)this + 396) = 49;
|
|
*((_DWORD *)this + 398) = 50;
|
|
*((_DWORD *)this + 405) = 52;
|
|
*((_DWORD *)this + 407) = 51;
|
|
*((_DWORD *)this + 416) = 52;
|
|
*((_DWORD *)this + 425) = 53;
|
|
*((_DWORD *)this + 434) = 55;
|
|
*((_DWORD *)this + 435) = 54;
|
|
*((_DWORD *)this + 444) = 55;
|
|
*((_DWORD *)this + 446) = 58;
|
|
*((_DWORD *)this + 447) = 56;
|
|
*((_DWORD *)this + 453) = 57;
|
|
*((_DWORD *)this + 456) = 57;
|
|
*((_DWORD *)this + 465) = 58;
|
|
*((_DWORD *)this + 474) = 60;
|
|
*((_DWORD *)this + 475) = 59;
|
|
*((_DWORD *)this + 484) = 60;
|
|
*((_DWORD *)this + 486) = 61;
|
|
*((_DWORD *)this + 493) = 60;
|
|
*((_DWORD *)this + 495) = 62;
|
|
*((_DWORD *)this + 504) = 63;
|
|
*((_DWORD *)this + 513) = 66;
|
|
*((_DWORD *)this + 514) = 66;
|
|
*((_DWORD *)this + 515) = 64;
|
|
*((_DWORD *)this + 524) = 65;
|
|
*((_DWORD *)this + 526) = 66;
|
|
*((_DWORD *)this + 533) = 68;
|
|
*((_DWORD *)this + 535) = 67;
|
|
*((_DWORD *)this + 544) = 68;
|
|
*((_DWORD *)this + 553) = 69;
|
|
*((_DWORD *)this + 562) = 70;
|
|
*((_DWORD *)this + 571) = 66;
|
|
*((_DWORD *)this + 572) = 71;
|
|
*((_DWORD *)this + 574) = 73;
|
|
*((_DWORD *)this + 575) = 74;
|
|
*((_DWORD *)this + 576) = 72;
|
|
*((_DWORD *)this + 581) = 67;
|
|
*((_DWORD *)this + 585) = 74;
|
|
*((_DWORD *)this + 586) = 73;
|
|
*((_DWORD *)this + 595) = 74;
|
|
*((_DWORD *)this + 604) = 75;
|
|
*((_DWORD *)this + 606) = 76;
|
|
*((_DWORD *)this + 613) = 75;
|
|
*((_DWORD *)this + 615) = 77;
|
|
*((_DWORD *)this + 624) = 78;
|
|
*((_DWORD *)this + 633) = 79;
|
|
*((_DWORD *)this + 642) = 82;
|
|
*((_DWORD *)this + 643) = 80;
|
|
*((_DWORD *)this + 652) = 81;
|
|
*((_DWORD *)this + 654) = 82;
|
|
*((_DWORD *)this + 661) = 81;
|
|
*((_DWORD *)this + 663) = 83;
|
|
*((_DWORD *)this + 672) = 84;
|
|
*((_DWORD *)this + 681) = 85;
|
|
*((_DWORD *)this + 690) = 86;
|
|
*((_DWORD *)this + 699) = 88;
|
|
*((_DWORD *)this + 700) = 87;
|
|
*((_DWORD *)this + 702) = 89;
|
|
*((_DWORD *)this + 703) = 87;
|
|
*((_DWORD *)this + 704) = 88;
|
|
*((_DWORD *)this + 709) = 83;
|
|
*((_DWORD *)this + 713) = 91;
|
|
*((_DWORD *)this + 714) = 89;
|
|
*((_DWORD *)this + 723) = 90;
|
|
*((_DWORD *)this + 732) = 91;
|
|
*((_DWORD *)this + 734) = 94;
|
|
*((_DWORD *)this + 735) = 87;
|
|
*((_DWORD *)this + 736) = 87;
|
|
*((_DWORD *)this + 737) = 92;
|
|
*((_DWORD *)this + 741) = 93;
|
|
*((_DWORD *)this + 746) = 88;
|
|
*((_DWORD *)this + 747) = 93;
|
|
*((_DWORD *)this + 756) = 94;
|
|
*((_DWORD *)this + 758) = 95;
|
|
*((_DWORD *)this + 765) = 97;
|
|
*((_DWORD *)this + 767) = 97;
|
|
*((_DWORD *)this + 768) = 96;
|
|
*((_DWORD *)this + 777) = 99;
|
|
*((_DWORD *)this + 778) = 99;
|
|
*((_DWORD *)this + 779) = 97;
|
|
*((_DWORD *)this + 788) = 98;
|
|
*((_DWORD *)this + 790) = 99;
|
|
*((_DWORD *)this + 797) = 100;
|
|
*((_DWORD *)this + 799) = 100;
|
|
*((_DWORD *)this + 808) = 101;
|
|
*((_DWORD *)this + 817) = 102;
|
|
*((_DWORD *)this + 826) = 103;
|
|
*((_DWORD *)this + 835) = 99;
|
|
*((_DWORD *)this + 836) = 104;
|
|
*((_DWORD *)this + 838) = 106;
|
|
*((_DWORD *)this + 839) = 105;
|
|
*((_DWORD *)this + 845) = 100;
|
|
*((_DWORD *)this + 848) = 108;
|
|
*((_DWORD *)this + 849) = 108;
|
|
*((_DWORD *)this + 850) = 101;
|
|
*((_DWORD *)this + 851) = 106;
|
|
*((_DWORD *)this + 860) = 107;
|
|
*((_DWORD *)this + 862) = 108;
|
|
*((_DWORD *)this + 869) = 107;
|
|
*((_DWORD *)this + 871) = 109;
|
|
*((_DWORD *)this + 880) = 109;
|
|
*((_DWORD *)this + 881) = 109;
|
|
*((_DWORD *)this + 882) = 110;
|
|
*((_DWORD *)this + 891) = 111;
|
|
*((_DWORD *)this + 894) = 107;
|
|
*((_DWORD *)this + 895) = 111;
|
|
*((_DWORD *)this + 896) = 112;
|
|
*((_DWORD *)this + 900) = 114;
|
|
*((_DWORD *)this + 901) = 114;
|
|
*((_DWORD *)this + 905) = 108;
|
|
*((_DWORD *)this + 906) = 113;
|
|
*((_DWORD *)this + 915) = 114;
|
|
*((_DWORD *)this + 918) = 116;
|
|
*((_DWORD *)this + 919) = 114;
|
|
*((_DWORD *)this + 920) = 115;
|
|
*((_DWORD *)this + 924) = 110;
|
|
*((_DWORD *)this + 925) = 110;
|
|
*((_DWORD *)this + 929) = 115;
|
|
*((_DWORD *)this + 930) = 116;
|
|
*((_DWORD *)this + 939) = 117;
|
|
*((_DWORD *)this + 948) = 118;
|
|
*((_DWORD *)this + 950) = 119;
|
|
*((_DWORD *)this + 957) = 120;
|
|
*((_DWORD *)this + 959) = 120;
|
|
*((_DWORD *)this + 968) = 121;
|
|
*((_DWORD *)this + 977) = 122;
|
|
*((_DWORD *)this + 986) = 123;
|
|
*((_DWORD *)this + 995) = 125;
|
|
*((_DWORD *)this + 996) = 124;
|
|
*((_DWORD *)this + 998) = 125;
|
|
*((_DWORD *)this + 1005) = 124;
|
|
*((_DWORD *)this + 1007) = 126;
|
|
*((_DWORD *)this + 1016) = 127;
|
|
*((_DWORD *)this + 1025) = 128;
|
|
*((_DWORD *)this + 1034) = 130;
|
|
*((_DWORD *)this + 1035) = 129;
|
|
*((_DWORD *)this + 1044) = 130;
|
|
*((_DWORD *)this + 1046) = 133;
|
|
*((_DWORD *)this + 1047) = 131;
|
|
*((_DWORD *)this + 1053) = 126;
|
|
*((_DWORD *)this + 1056) = 132;
|
|
*((_DWORD *)this + 1065) = 128;
|
|
*((_DWORD *)this + 1066) = 132;
|
|
*((_DWORD *)this + 1067) = 133;
|
|
*((_DWORD *)this + 1076) = 134;
|
|
*((_DWORD *)this + 1078) = 135;
|
|
*((_DWORD *)this + 1085) = 136;
|
|
*((_DWORD *)this + 1087) = 136;
|
|
*((_DWORD *)this + 1096) = 137;
|
|
*((_DWORD *)this + 1105) = 138;
|
|
*((_DWORD *)this + 1114) = 139;
|
|
*((_DWORD *)this + 1123) = 142;
|
|
*((_DWORD *)this + 1124) = 140;
|
|
*((_DWORD *)this + 1126) = 142;
|
|
*((_DWORD *)this + 1127) = 143;
|
|
*((_DWORD *)this + 1128) = 141;
|
|
*((_DWORD *)this + 1133) = 140;
|
|
*((_DWORD *)this + 1137) = 144;
|
|
*((_DWORD *)this + 1138) = 142;
|
|
*((_DWORD *)this + 1147) = 143;
|
|
*((_DWORD *)this + 1156) = 144;
|
|
*((_DWORD *)this + 1158) = 147;
|
|
*((_DWORD *)this + 1159) = 144;
|
|
*((_DWORD *)this + 1160) = 146;
|
|
*((_DWORD *)this + 1161) = 145;
|
|
*((_DWORD *)this + 1165) = 146;
|
|
*((_DWORD *)this + 1170) = 141;
|
|
*((_DWORD *)this + 1171) = 146;
|
|
*((_DWORD *)this + 1180) = 147;
|
|
*((_DWORD *)this + 1182) = 148;
|
|
*((_DWORD *)this + 1189) = 147;
|
|
*((_DWORD *)this + 1191) = 148;
|
|
*((_DWORD *)this + 1192) = 149;
|
|
*((_DWORD *)this + 1201) = 151;
|
|
*((_DWORD *)this + 1202) = 151;
|
|
*((_DWORD *)this + 1203) = 150;
|
|
*((_DWORD *)this + 1212) = 151;
|
|
*((_DWORD *)this + 1214) = 152;
|
|
*((_DWORD *)this + 1221) = 154;
|
|
*((_DWORD *)this + 1223) = 153;
|
|
*((_DWORD *)this + 1232) = 154;
|
|
*((_DWORD *)this + 1241) = 155;
|
|
*((_DWORD *)this + 1250) = 156;
|
|
*((_DWORD *)this + 1259) = 156;
|
|
*((_DWORD *)this + 1260) = 157;
|
|
*((_DWORD *)this + 1262) = 157;
|
|
*((_DWORD *)this + 1263) = 158;
|
|
*((_DWORD *)this + 1269) = 160;
|
|
*((_DWORD *)this + 1272) = 159;
|
|
*((_DWORD *)this + 1281) = 159;
|
|
*((_DWORD *)this + 1282) = 155;
|
|
*((_DWORD *)this + 1283) = 160;
|
|
*((_DWORD *)this + 1292) = 161;
|
|
*((_DWORD *)this + 1294) = 164;
|
|
*((_DWORD *)this + 1295) = 164;
|
|
*((_DWORD *)this + 1296) = 162;
|
|
*((_DWORD *)this + 1301) = 161;
|
|
*((_DWORD *)this + 1305) = 163;
|
|
*((_DWORD *)this + 1314) = 159;
|
|
*((_DWORD *)this + 1315) = 164;
|
|
*((_DWORD *)this + 1324) = 165;
|
|
*((_DWORD *)this + 1326) = 167;
|
|
*((_DWORD *)this + 1327) = 161;
|
|
*((_DWORD *)this + 1328) = 166;
|
|
*((_DWORD *)this + 1333) = 168;
|
|
*((_DWORD *)this + 1337) = 169;
|
|
*((_DWORD *)this + 1338) = 167;
|
|
*((_DWORD *)this + 1347) = 168;
|
|
*((_DWORD *)this + 1350) = 169;
|
|
*((_DWORD *)this + 1356) = 171;
|
|
*((_DWORD *)this + 1357) = 170;
|
|
*((_DWORD *)this + 1359) = 170;
|
|
*((_DWORD *)this + 1368) = 171;
|
|
*((_DWORD *)this + 1377) = 167;
|
|
*((_DWORD *)this + 1378) = 173;
|
|
*((_DWORD *)this + 1379) = 172;
|
|
*((_DWORD *)this + 1388) = 173;
|
|
*((_DWORD *)this + 1390) = 174;
|
|
*((_DWORD *)this + 1397) = 169;
|
|
*((_DWORD *)this + 1399) = 170;
|
|
*((_DWORD *)this + 1400) = 174;
|
|
*((_DWORD *)this + 1401) = 177;
|
|
*((_DWORD *)this + 1402) = 177;
|
|
*((_DWORD *)this + 1403) = 175;
|
|
*((_DWORD *)this + 1406) = 176;
|
|
*((_DWORD *)this + 1412) = 175;
|
|
*((_DWORD *)this + 1413) = 177;
|
|
*((_DWORD *)this + 1415) = 176;
|
|
*((_DWORD *)this + 1416) = 177;
|
|
*((_DWORD *)this + 1425) = 178;
|
|
*((_DWORD *)this + 1434) = 179;
|
|
*((_DWORD *)this + 1443) = 180;
|
|
*((_DWORD *)this + 1452) = 181;
|
|
*((_DWORD *)this + 1461) = 184;
|
|
*((_DWORD *)this + 1478) = 0;
|
|
*((_DWORD *)this + 1479) = 23;
|
|
*((_DWORD *)this + 1480) = 21;
|
|
*((_DWORD *)this + 1481) = 32;
|
|
*((_DWORD *)this + 1482) = 19;
|
|
*((_DWORD *)this + 1483) = 17;
|
|
*((_DWORD *)this + 1484) = 31;
|
|
*((_DWORD *)this + 1485) = 38;
|
|
*((_DWORD *)this + 1486) = 0;
|
|
"""
|
|
|
|
# ==============================================================================
|
|
# 2. PARSE DATA
|
|
# ==============================================================================
|
|
# We need to extract TransitionTable and TargetHistogram
|
|
# Transition table offset base = 6 (offset 24 bytes / 4)
|
|
# Target histogram offset base = 1479
|
|
|
|
TABLE_OFFSET_BASE = 6
|
|
HIST_OFFSET_BASE = 1479
|
|
NUM_HITS = 8
|
|
|
|
transition_table = {} # (state, hit) -> next_state
|
|
target_histogram = [0] * NUM_HITS
|
|
|
|
# Regex to find assignments: *((_DWORD *)this + OFFSET) = VALUE;
|
|
pattern = re.compile(r'\*\(\(_DWORD \*\)this \+ (\d+)\) = (\d+);')
|
|
|
|
print("[*] Parsing C++ code...")
|
|
|
|
matches = pattern.findall(raw_cpp_code)
|
|
for offset_str, value_str in matches:
|
|
offset = int(offset_str)
|
|
value = int(value_str)
|
|
|
|
# Check if it belongs to Transition Table
|
|
# The table is roughly between offset 6 and 1470
|
|
if TABLE_OFFSET_BASE <= offset < 1478:
|
|
# Calculate State and Hit
|
|
# equation: offset = base + (state * 8) + hit
|
|
local_off = offset - TABLE_OFFSET_BASE
|
|
state = local_off // NUM_HITS
|
|
hit = local_off % NUM_HITS
|
|
transition_table[(state, hit)] = value
|
|
|
|
# Check if it belongs to Target Histogram
|
|
elif HIST_OFFSET_BASE <= offset < HIST_OFFSET_BASE + NUM_HITS:
|
|
idx = offset - HIST_OFFSET_BASE
|
|
target_histogram[idx] = value
|
|
|
|
print(f"[*] Parsed {len(transition_table)} transition rules.")
|
|
print(f"[*] Target Histogram: {target_histogram}")
|
|
|
|
# Calculate Flag Length from histogram
|
|
FLAG_LEN = sum(target_histogram)
|
|
print(f"[*] Calculated Flag Length: {FLAG_LEN}")
|
|
|
|
# The Success State is usually the state we reach after the last char.
|
|
# Based on the main(), it is 181.
|
|
SUCCESS_STATE = 181
|
|
|
|
# Initial state (offset +1478 = 0)
|
|
START_STATE = 0
|
|
# Also, there is a distinct assignment `*v2 = 1`. v2 is offset 6.
|
|
# offset 6 -> state 0, hit 0 -> next_state 1.
|
|
transition_table[(0, 0)] = 1
|
|
|
|
# ==============================================================================
|
|
# 3. Z3 SOLVER
|
|
# ==============================================================================
|
|
s = Solver()
|
|
|
|
# Variables: The sequence of hits (0-7)
|
|
hits = [Int(f'h_{i}') for i in range(FLAG_LEN)]
|
|
# Variables: The sequence of states
|
|
states = [Int(f's_{i}') for i in range(FLAG_LEN + 1)]
|
|
|
|
# 1. Domain Constraints
|
|
for h in hits:
|
|
s.add(h >= 0, h < NUM_HITS)
|
|
|
|
# 2. Histogram Constraints
|
|
for k in range(NUM_HITS):
|
|
s.add(Sum([If(h == k, 1, 0) for h in hits]) == target_histogram[k])
|
|
|
|
# 3. FSM Simulation
|
|
s.add(states[0] == START_STATE)
|
|
|
|
# We need to construct the lookup logic.
|
|
# Since many transitions are missing (implied 0/fail), we only encode the valid ones.
|
|
# If a transition (state, hit) is NOT in our dictionary, it defaults to 0.
|
|
|
|
# Determine max state index to iterate safely
|
|
max_state = max([k[0] for k in transition_table.keys()] + [0])
|
|
|
|
print("[*] Building Z3 constraints (this might take a second)...")
|
|
|
|
for i in range(FLAG_LEN):
|
|
curr_s = states[i]
|
|
next_s = states[i+1]
|
|
curr_h = hits[i]
|
|
|
|
# Logic: next_s == Table[curr_s][curr_h]
|
|
# We construct a big If-Else chain or rely on the fact that the path MUST exist.
|
|
# Optimization: Only allow valid transitions found in the table.
|
|
|
|
# Collect all valid transitions as a constraint:
|
|
# Or( (curr_s == S1 And curr_h == H1 And next_s == S_next), ... )
|
|
|
|
valid_transitions = []
|
|
|
|
# We iterate through our known transitions
|
|
for (t_state, t_hit), t_next in transition_table.items():
|
|
valid_transitions.append(And(curr_s == t_state, curr_h == t_hit, next_s == t_next))
|
|
|
|
# If the solver picks a state/hit combo not in our table, it goes to state 0
|
|
# But since we demand the final state be 181, valid transitions must be taken.
|
|
# So we simply enforce that one of the valid transitions MUST occur.
|
|
s.add(Or(valid_transitions))
|
|
|
|
# 4. Success Condition
|
|
s.add(states[FLAG_LEN] == SUCCESS_STATE)
|
|
|
|
print("[*] Solving...")
|
|
if s.check() == sat:
|
|
m = s.model()
|
|
sol = "".join([str(m.evaluate(h).as_long()) for h in hits])
|
|
print("\n[SUCCESS] Sequence Found:")
|
|
print(sol)
|
|
else:
|
|
print("\n[FAIL] UNSAT. No solution found.")
|