babymix.py

from z3 import *

s = Solver()
t = BitVecs(' '.join([f'c{i}' for i in range(32)]), 8)

s.add(t[0x15] + t[1] + (t[0xb] - t[2]) + (t[0x11] - t[0xd]) + (t[8] - t[0xc]) + (t[5] - t[0x10]) == 0x62)
s.add((t[0x11] - t[9]) + t[4] + t[0xb] + (t[0x11] - t[1]) == 0xa6)
s.add((t[0x12] ^ t[0xc]) + (t[7] - t[0x12]) + (t[0x15] - t[0x13]) + (t[0x10] - t[0x15]) == 0x4b)
s.add((t[0xd] - t[0x13]) + (t[0xb] ^ t[0]) + (t[0xe] ^ t[0]) + (t[0x10] - t[0xe]) == 0x6a)
s.add((t[3] - t[0x11]) + (t[10] - t[0x14]) + (t[0xd] - t[8]) == 0x55)
s.add(t[0x12] + t[0x14] + (t[0] - t[0xf]) == 0x9c)
s.add((t[0x15] - t[0xb]) + (t[8] - t[0xf]) + (t[9] - t[2]) + (t[6] - t[0xe]) == -0x6d)
s.add((t[0xc] - t[10]) + (t[0xb] - t[0x15]) == 0x24)
s.add(t[6] + t[9] + (t[2] ^ t[10]) + t[7] + t[2] + t[0xd] + t[0x14] + (t[0x10] ^ t[3]) == 0x26d)
s.add((t[0x10] ^ t[0]) + t[3] + t[0x10] + (t[0x10] ^ t[5]) == 0xe8)
s.add((t[0] ^ t[0x13]) + t[10] + t[3] + (t[3] - t[0x13]) == 0x148)
s.add((t[1] - t[0x13]) + (t[2] ^ t[0xe]) + t[0] + t[0xb] + (t[8] - t[3]) == 0x11b)
s.add(t[10] + t[5] + (t[0x12] - t[9]) + t[10] + t[0xe] == 0x19d)
s.add(t[6] + t[7] + (t[0x15] - t[0x12]) + t[2] + t[0xf] + (t[0x11] - t[4]) + (t[5] - t[0x12]) == 0xfa)
s.add((t[0x15] - t[5]) + (t[6] - t[0xd]) + (t[0xf] ^ t[10]) == -0x30)
s.add((t[3] - t[0x12]) + (t[0] - t[0x14]) + t[0x13] + t[10] + t[10] + t[0x13] == 0x129)
s.add((t[0x10] ^ t[5]) + (t[6] - t[0x10]) + (t[0x13] ^ t[0x12]) == 0x66)
s.add((t[7] ^ t[2]) + (t[4] - t[0x10]) == 0x4d)
s.add((t[0xc] ^ t[0x10]) + (t[6] - t[0xd]) + (t[0x11] - t[0xb]) + (t[0xd] ^ t[0x13]) == 0x55)
s.add(t[0x11] + t[0xb] + t[0] + t[0x10] + (t[0x13] - t[7]) == 0x169)
s.add((t[4] ^ t[6]) + (t[0xc] - t[0xb]) + (t[3] ^ t[5]) == 0x1d)
s.add(t[8] + t[0xc] + (t[0xc] - t[0x11]) == 0x99)
s.add(t[10] + t[7] + (t[0xe] ^ t[8]) + t[1] + t[5] + (t[0xe] - t[3]) + (t[8] - t[0x11]) == 0x180)
s.add((t[2] - t[0x13]) + (t[10] - t[8]) == 0x4a)
s.add((t[0x13] ^ t[0xf]) + t[0xf] + t[3] == 0x128)
s.add((t[2] ^ t[0x13]) + t[0x15] + t[10] == 0xd9)
s.add(t[2] + t[0x11] + (t[0xf] - t[0x15]) + (t[2] - t[4]) + (t[4] - t[0]) == 0x109)
s.add((t[10] - t[2]) + t[4] + t[0x13] + (t[0x11] ^ t[0xc]) + (t[3] - t[0x11]) == 0xa0)

s.check()
model = s.model()

password = ""
for char in t:
    if model[char] != None:
        password += chr(model[char].as_long())

print('Found password:', password)

What version of z3 is this? I get an error on Solver?

What version of z3 is this? I get an error on Solver?

It's 4.8.9.0. Python package for z3 is "z3-solver" and not "z3".

ha yep that was it...i installed some rando package....thanks