z3 solver script for Position Challenge from Reversing.kr

pos_crack.py

from z3 import *

s = Solver()

serial = list("76876-77776")

inp = []

for i in range(4):
	b = BitVec("%d" % i, 16)
	inp.append(b)
	s.add(And(inp[i] >= 97,inp[i] <= 122))


s.add(inp[3] == ord('p'))

v7 = (inp[0] & 1) + 5
v9 = ((inp[1] >> 2) & 1) + 1
s.add(v7+v9 == serial[0])

v46 = ((inp[0] >> 3) & 1) + 5
v38 = ((inp[1] >> 3) & 1) + 1
s.add(v46+v38 == serial[1])

v42 = ((inp[0] >> 1) & 1) + 5
v40 = ((inp[1] >> 4) & 1) + 1
s.add(v42+v40 == serial[2])

v44 = ((inp[0] >> 2) & 1) + 5
v34 = (inp[1] & 1) + 1
s.add(v44+v34 == serial[3])

v48 = ((inp[0] >> 4) & 1) + 5
v36 = ((inp[1] >> 1) & 1) + 1
s.add(v48+v36 == serial[4])

#serial[5] = '-'

v21 = (inp[2] & 1) + 5
v23 = ((inp[3] >> 2) & 1) + 1
s.add(v21+v23 == serial[6])

v47 = ((inp[2] >> 3) & 1) + 5
v39 = ((inp[3] >> 3) & 1) + 1
s.add(v47+v39 == serial[7])

v43 = ((inp[2] >> 1) & 1) + 5
v41 = ((inp[3] >> 4) & 1) + 1
s.add(v43+v41 == serial[8])

v45 = ((inp[2] >> 2) & 1) + 5
v35 = (inp[3] & 1) + 1
s.add(v45+v35 == serial[9])

v49 = ((inp[2] >> 4) & 1) + 5
v37 = ((inp[3] >> 1) & 1) + 1
s.add(v49+v37 == serial[10])


while s.check() == sat:
	sol = s.model()
	#print sol
	block = []

	name = ""
	for i in range(len(inp)):
		c = inp[i]
		name += chr(int(str(sol[c])))
		block.append(c != sol[c])
	s.add(Or(block))

	print "NAME   :: ",name
print "------"
print "SERIAL :: ","".join(serial)