ex03.py

from z3 import *
from random import shuffle

# define the variables
chars = IntVector("", 16)

solver = Solver()

# all values are printable chararacters (33 - 126)
for i in range(16):
	solver.add(chars[i] >= 33, chars[i] <= 126)

# checking conditions: edi == 239
solver.add(sum(chars) % 255 == 239)

# solve
if solver.check() == sat:
	model = solver.model()
	array = [model[name].as_long() for name in model.decls()]

	# randomize until ebx == 126
	while True:
		edi = 0
		ebx = 0
		string = ""
		shuffle(array)
		for decimal in array:
			string += chr(decimal)
			edi = (decimal + edi) % 255
			ebx = (ebx + edi) % 255
		if ebx == 126:
			print string
			break
else:
	print "not satisfied"