MarsAnalytica z3 solver

solve_marsanalytica.py

from z3 import *

def display_model(m):
    block = {}
    for x in m:
        if str(x)[0] == "p":
            block[int(str(x)[1:])] = int(str(m[x]))
    password = "".join(map(chr, block.values()))
    print password

def is_printable(x):
    return And(x >= 0x20, x <= 0x7E)
    
s = Solver()
length = 19
password = [BitVec("p%d" % i, 32) for i in range(length)]
for i in xrange(0, length):
    s.add(is_printable(password[i]))

s.add((((password[12] - password[10]) ^ password[13]) * (password[6] * password[14])) == 0x00003FCF)
s.add(((password[18] ^ password[1]) ^ (password[15] - password[7])) == 0x53)
s.add(((password[17] - password[16]) * (password[0] ^ (password[5] + password[9]))) == 0xFFFFE8F2)
s.add((password[3] - password[11]) == 0x0B)
s.add((password[8] ^ (password[4] + password[2])) == 0x03)
s.add((password[8] + (password[15] - password[4])) == 0xB0)
s.add((password[6] ^ ((password[9] ^ password[10]) - (password[18] + password[11]))) == 0xFFFFFF39)
s.add(((password[16] * password[2]) + (password[1] * (password[0] ^ password[17]))) == 0x00002701)
s.add(((password[13] * password[14]) - password[7]) == 0x823)
s.add((((password[3] + password[12]) - password[5])) == 0x6E)
s.add(((password[13] + password[9]) + (password[10] * password[8])) == 0x000015FE)
s.add(((password[5] - password[16]) - (password[0] + password[2])) == 0xFFFFFF4A)
s.add(((password[14] ^ password[7]) * password[17]) == 0x00001C20)
s.add(((password[6] * password[11]) + (password[1] * password[3])) == 0x000045D0)
s.add(((password[12] - password[15]) - (password[18] * password[4])) == 0xFFFFEAE0)
s.add(((password[3] * password[15]) + (password[11] * password[2])) == 0x000049C8)
s.add((password[16] * (password[5] + password[13])) == 0x00003AC9)
s.add((password[17] * (password[0] + password[10])) == 0x00002F76)
s.add(((password[14] ^ password[6]) * password[18]) == 0x00002760)
s.add(((password[12] + password[7]) - password[4]) == 0x84)
s.add((password[8] + (password[1] * password[9])) == 0x00000995)
s.add((password[8] + (password[1] * password[9])) == 0x00000995)
s.add((((password[12] - password[10]) ^ password[13]) * (password[6] * password[14])) == 0x00003FCF)

print s.check()
while s.check() == sat:
    model = s.model()
    print model
    display_model(model)
    s.add(Or([sym != model[sym] for sym in password]))

# x_00 = password[6] * password[14]
# x_01 = password[12] - password[10]
# x_02 = (password[12] - password[10]) ^ password[13]
# x_03 = ((password[12] - password[10]) ^ password[13]) * (password[6] * password[14])
# x_03 == 0x00003FCF
# 
# ----
# 
# x_00 = password[18] ^ password[01]
# x_01 = password[15] - password[7]
# x_02 = (password[18] ^ password[01]) ^ (password[15] - password[7])
# x_02 == 0x53
# 
# ----
# 
# x_00 = password[17] - password[16]
# x_01 = password[5] + password[9]
# x_02 = password[0] ^ (password[5] + password[9])
# x_03 = (password[17] - password[16]) * (password[0] ^ (password[5] + password[9]))
# x_03 == 0xFFFFE8F2
# 
# ----
# 
# x_00 = password[3] - password[11]
# x_00 == 0x0B
# 
# ----
# 
# x_00 = password[4] + password[2]
# x_01 = password[8] ^ x_00
# x_01 == 0x03
# 
# ----
# 
# x_00 = password[15] - password[4]
# x_01 = password[8] + x_00
# x_01 == 0xB0
# 
# ----
# 
# x_00 = password[9] ^ password[10]
# x_01 = password[18] + password[11]
# x_02 = (password[9] ^ password[10]) - (password[18] + password[11])
# x_03 = password[6] ^ ((password[9] ^ password[10]) - (password[18] + password[11]))
# x_03 == 0xFFFFFF39
# 
# ----
# 
# x_00 = password[16] * password[2]
# x_01 = password[0] ^ password[17]
# x_03 = password[1] * (password[0] ^ password[17])
# x_04 = (password[16] * password[2]) + (password[1] * (password[0] ^ password[17]))
# x_04 == 0x00002701
# 
# ----
# 
# x_00 = password[13] * password[14]
# x_01 = (password[13] * password[14]) - password[7]
# x_01 == 0x823
# 
# ----
# 
# x_00 = password[3] + password[12]
# x_01 = (password[3] + password[12]) - password[5] 
# x_01 == 0x6E
# 
# ----
# 
# x_00 = password[13] + password[9]
# x_01 = password[10] * password[8]
# x_02 = (password[13] + password[9]) + (password[10] * password[8])
# x_02 == 0x000015FE
# 
# ----
# 
# x_00 = password[5] - password[16]
# x_01 = password[0] + password[2]
# x_02 = (password[5] - password[16]) - (password[0] + password[2])
# x_02 == 0xFFFFFF4A
# 
# ----
# 
# x_00 = password[14] ^ password[7]
# x_01 = (password[14] ^ password[7]) * password[17]
# x_01 == 0x00001C20
# 
# ----
# 
# x_00 = password[6] * password[11]
# x_01 = password[1] * password[3]
# x_02 = (password[6] * password[11]) + (password[1] * password[3])
# x_02 == 0x000045D0
# 
# ----
# 
# x_00 = password[12] - password[15]
# x_01 = password[18] * password[4]
# x_02 = (password[12] - password[15]) - (password[18] * password[4])
# x_02 == 0xFFFFEAE0
# 
# ----
# 
# x_00 = password[3] * password[15]
# x_01 = password[11] * password[2]
# x_02 = (password[3] * password[15]) + (password[11] * password[2])
# x_02 == 0x000049C8
# 
# ----
# 
# x_00 = password[5] + password[13]
# x_01 = password[16] * (password[5] + password[13])
# x_01 == 0x00003AC9
# 
# ----
# 
# x_00 = password[0] + password[10]
# x_01 = password[17] * (password[0] + password[10])
# x_01 == 0x00002F76
# 
# ----
# 
# x_00 = password[14] ^ password[6]
# x_01 = (password[14] ^ password[6]) * password[18]
# x_01 == 0x00002760
# 
# ----
# 
# x_00 = password[12] + password[7]
# x_01 = (password[12] + password[7]) - password[4]
# x_01 == 0x84
# 
# ----
# 
# x_00 = password[1] * password[9]
# x_01 = password[8] + (password[1] * password[9])
# x_01 == 0x00000995