keygen for challenge3

keygen.py

# challenge3 - https://drive.google.com/file/d/0B_bQeUUGe4uLM3BWd1dqTVF4TVE/view?usp=sharing

from z3 import *
import sys

# define the variables
chars = IntVector("", 7)
solver = Solver()
constraint = []

# all values are small alphabet chararacters (97 - 122)
for i in range(7):
    constraint += [chars[i] >= 97, chars[i] <= 122]

# additional constraint
treshold = [2, 3, 5, 7, 1, 3, 7]
constraint.append(sum([chars[i] * treshold[i] for i in range(7)]) * sum(chars) == 2108268)

# argv[1] == max key generated
for loop in range(0, int(sys.argv[1])):
    solver.add(constraint)
    if solver.check() == sat:
        model = solver.model()
        # print and add current model as constraint
        block = []
        pwd = ''
        for name in model:
            pwd += chr(model[name].as_long())
            block.append(name() != model[name])
        print pwd[::-1]
        constraint.append(Or(block))
        solver.reset()
    else: break