# PicoCTF 2k14 - Bit Puzzle

# cat bitpuzzle.py 
from z3 import *

v1 = BitVec('v1', 32)
v2 = BitVec('v2', 32)
v3 = BitVec('v3', 32)
v4 = BitVec('v4', 32)
v5 = BitVec('v5', 32)
v6 = BitVec('v6', 32)
v7 = BitVec('v7', 32)
v8 = BitVec('v8', 32)

s = Solver()

s.add(v3 + v2 == 0xc0dcdfce)
s.add(v1 + v2 == 0xd5d3dddc)
s.add((5 * v2) + (3 * v1) == 0x404a7666)
s.add(v1 ^ v4 == 0x18030607)
s.add(v4 & v1 == 0x666c6970)
s.add(v5 * v2 == 0xb180902b)
s.add(v3 * v5 == 0x3e436b5f)
s.add(v5 + (2 * v6) == 0x5c483831)
s.add(v6 & 0x70000000 == 0x70000000)
s.add(v6 / v7 == 1)
s.add(v6 % v7 == 0xe000cec)
s.add((3 * v5) + (2 * v8) == 0x3726eb17)
s.add((7 * v8) + (4 * v3) == 0x8b0b922d)
s.add(v4 + (3 * v8) == 0xb9cf9c91)

import struct

d = {}

if s.check() == sat:
 m = s.model()
 print m
 for v in m:
  d[str(v)] = struct.pack('<I', int(str(m[v])))

flag = ''

for k in sorted(d):
 flag += d[k]

print flag

# python bitpuzzle.py 
[v6 = 1953459295,
 v7 = 1718574963,
 v2 = 1600613993,
 v4 = 1852795252,
 v8 = 1853187679,
 v3 = 1635086693,
 v1 = 1986817907,
 v5 = 1936285555]
solving_equations_is_lots_of_fun