z3solver.py

#!/usr/bin/python
from z3 import *

# Declare a 32 bit verctor representing register eax
reg_eax = BitVec('eax', 32)

# add eax, 0xDEADBEEF
eax = reg_eax + 0xDEADBEEF

# xor eax, 0x1337
eax = eax ^ 0x1337

# shr eax, 0x3
eax = eax >> 0x3

# Create a solver instance
s = Solver()

# Add the constraint
s.add(eax == 0x31337)

# Check if satisfied
if s.check() == sat:
	# Print value
	print hex(s.model()[reg_eax].as_long())