RTLxHA_2021_Reverse_Bad_Developers_a.py

#!/usr/bin/env python3
from z3 import *

a = "LTR"
b = "0D"
c = "S1"

s=Solver()
inp=[BitVec(f'v{x}', 16) for x in range(17)]

for x in range(17):
    s.add(inp[0] == ord(a[2]))
    s.add(inp[1] == ord(a[1]))
    s.add(inp[2] == ord(a[0]))
    s.add(inp[3] == ord('{'))
    s.add(inp[4] == ord(b[1]))
    s.add(inp[5] == ord(b[0]))
    s.add(inp[6] == ord('N'))
    s.add(inp[7] == ord('T'))
    s.add(inp[8] == 95)
    s.add(inp[9] == ord(b[1]))
    s.add(inp[10] == ord(b[0]))
    s.add(inp[11] == ord("_"))
    s.add(inp[12] == ord("T"))
    s.add(inp[13] == ord('H'))
    s.add(inp[14] == ord(c[1]))
    s.add(inp[15] == ord(c[0]))
    s.add(inp[16] == ord('}'))


if s.check()==sat:
    raw = str(s.model()).replace("[", "").replace("]", "").replace(" ","").split(",\n")
    final=""
    for x in raw:
        n=x.split("=")[1]
        final+=chr(int(n))
    print(final[::-1])