darkCON CTF 2021 - Too Much [ RE ]

solver_toomuch.py

from z3 import *

a = [BitVec("x{}".format(i), 8) for i in range(200)]
arr=[70, 22, 39, 182, 52, 244, 228, 183, 67, 39, 51, 245, 151, 3, 87, 245, 39, 51, 67, 198, 198, 151, 245, 71, 134, 19, 230, 182, 19, 230, 147, 245, 71, 134, 67, 71, 245, 151, 3, 87, 245, 54, 67, 230, 245, 71, 39, 151, 245, 71, 134, 19, 83, 245, 214, 67, 230, 87, 67, 198, 198, 151, 243, 243, 243, 245, 244, 182, 245, 148, 245, 71, 134, 19, 230, 182, 245, 151, 3, 87, 245, 38, 51, 71, 71, 51, 39, 245, 87, 55, 51, 245, 55, 3, 214, 51, 245, 22, 87, 71, 3, 214, 67, 71, 51, 70, 245, 71, 3, 3, 198, 55, 245, 198, 19, 182, 51, 245, 67, 230, 147, 39, 245, 3, 39, 245, 165, 51, 245, 71, 3, 245, 214, 67, 182, 51, 245, 151, 3, 87, 39, 245, 198, 19, 102, 51, 245, 214, 87, 54, 134, 245, 86, 67, 55, 19, 51, 39, 226, 52, 3, 230, 118, 39, 67, 71, 55, 245, 102, 3, 39, 245, 55, 3, 198, 103, 19, 150, 230, 147, 245, 71, 134, 51, 245, 86, 67, 55, 151, 245, 54, 134, 67, 198, 198, 51, 230, 118, 51, 215]

s=Solver()
for i in range(200):
	eval("s.add((16 * a["+str(i)+"]) + (a["+str(i)+"] >> 4) == "+str(arr[i])+")")

s.check()
model=s.model()
flag=""
for i in a:
    flag+=chr(model[i].as_long())
print(flag)