Another Z3 crackme Solver

reee-z3.py

from z3 import *
import sys
sys.setrecursionlimit(133337)
unk = [72, 95, 54, 53, 53, 37, 20, 44, 29, 1, 3, 45, 12, 111, 53, 97, 126, 52, 10, 68, 36, 44, 74, 70, 25, 89, 91, 14, 120, 116, 41, 19, 44, 0]
length=33
s = Solver()
vec = ""
for i in range(length):
	vec += F"{i} "
m = BitVecs(vec,8)
s.add(m[0] == ord('p'))
s.add(m[1] == ord('c'))
s.add(m[2] == ord('t'))
s.add(m[3] == ord('f'))
s.add(m[4] == ord('{'))
for i in range(length):
	s.add(m[i]>=0x20)
	s.add(m[i]<=127)
bVar5 = 0x50
for iv6 in range(0x539):
	for i in range(length):
		m[i] = m[i] ^ bVar5
		bVar5 = m[i]^ bVar5
for i in range(length):
	s.add(m[i] == unk[i])
print(s.check())
while s.check() == z3.sat:
	model = s.model()
	nope = []
	out = ''
	model = sorted([(str(d),model[d]) for d in model],key=lambda x:int(x[0]))
	[print(chr(x[1].as_long()&0xff),end='') for x in model]
	break