keygen for challenge4_ok using Z3 theorem prover

keygen.py

# challenge4_ok.exe - https://drive.google.com/open?id=0B_bQeUUGe4uLcXNqRnBBand5Yk0

from z3 import *
import sys

# argv[1] == key length
length = int(sys.argv[1])
if length < 5:
    print "length must be more than 4!"
    exit()

# define vars
chars = [BitVec("%i" % i, 8) for i in xrange(length)]
solver = Solver()
constraint = []

# all values are printable chararacters excluding space (33 - 126)
for i in xrange(length):
    constraint += [chars[i] >= 33, chars[i] <= 126]

equal = [0x30, 0x5b, 0x6f, 0x2] # little endian == reversed
for i in xrange(4):
    placeholder = chars[i]
    for j in xrange(i + 1, i + 16):
        placeholder ^= chars[j] if j < length else 0
    constraint.append(placeholder == equal[i])

# argv[2] == max key generated
for loop in xrange(int(sys.argv[2])):
    solver.add(constraint)
    if solver.check() == sat:
        model = solver.model()
        # print and add current model as constraint
        block = []
        pwd = list("a" * length) # dummy list
        for name in model:
            pwd[int(name.__str__())] = chr(model[name].as_long())
            block.append(name() != model[name])
        print "".join(pwd)
        constraint.append(Or(block))
        solver.reset()
    else: break