Unoptimized solution script for 'reee' chall from Plaid CTF 2020, solved using z3

reee_plaid20_z3.py

from z3 import *
import time
start_time = time.time()

s = Solver()

enc = ['0x48', '0x5f', '0x36', '0x35', '0x35', '0x25', '0x14', '0x2c', '0x1d', '0x01', '0x03', '0x2d', '0x0c', '0x6f', '0x35', '0x61', '0x7e', '0x34', '0x0a', '0x44', '0x24', '0x2c', '0x4a', '0x46', '0x19', '0x59', '0x5b', '0x0e', '0x78', '0x74', '0x29', '0x13','0x2c']
enc = [int(x,16) for x in enc]

inp = []

for i in range(len(enc)):
	b = BitVec("%d" % i, 16)
	inp.append(b)

seed = 0x50

tmp = inp

for x in range(1337):
	res = [None]*len(inp)

	res[0] = seed ^ tmp[0]
	seed = tmp[len(inp)-1]
	
	for i in range(1, len(inp)):
		res[i] = (tmp[i-1] ^ tmp[i])

	tmp = res

for i in range(len(inp)):
	s.add(res[i] == enc[i])

if s.check() == sat:
	solution = s.model()
	
	flag = ""
	for i in range(len(inp)):
		flag += (chr(int(str(solution[inp[i]])))) 
	print flag
	print solution


print("--- %s seconds ---" % (time.time() - start_time))