from z3 import * 

flag_data = [72571,144964,217224,289496,361110,433332,502467,574096,645273,716520,792891,858024,925756,995232,1070055,1137952,1209193,1292004,1349513,1414840,1473885,1560372,1617866,1714032,1744800,1852864,1876770,1983016,2014108,2089260,2160607,2225216,2339469,2408560,2418745,2515320,2597400,2604444,2697669,2705680]

solver = Solver()

# Create 41 symbolic bytes
passwd = [BitVec(f'p{i}', 8) for i in range(40)]


# Add ASCII printable constraints for all
for p in passwd:
    solver.add(p >= 32, p <= 126)

# Apply known format: GPNCTF{.....}
known = b"GPNCTF{"
for i, c in enumerate(known):
    solver.add(passwd[i] == c)
solver.add(passwd[39] == ord('}'))

# Implement compute_secret logic
for index in range(40):
    total = flag_data[index]
    for pass_char in range(40):
        multi = index + pass_char + index * pass_char + 1
        if pass_char == index:
            multi = 0
        total -= ZeroExt(56, passwd[pass_char]) * multi
    solver.add(total == 0)
# Solve

print(solver.check())
if solver.check() == sat:
    model = solver.model()
    result = ''.join(chr(model[p].as_long()) for p in passwd)
    print("Recovered flag:", result)
else:
    print("No solution found.")