from z3 import *

# Create a Z3 BitVec variable for key
key = BitVec('key', 64)

# Create Z3 variables for tmp1, tmp2, tmp3, tmp4
tmp1 = BitVec('tmp1', 64)
tmp2 = BitVec('tmp2', 64)
tmp3 = BitVec('tmp3', 64)
tmp4 = BitVec('tmp4', 64)

# Create a Z3 Solver instance
solver = Solver()

# Stage 1
stage1_formula = tmp1 == (key & 0xF0F0F0F0F0F0F0F0)
solver.add(stage1_formula)

# Stage 2
stage2_formula = tmp2 == ((tmp1 << 5) & 0xFFFFFFFFFFFFFFFF)
solver.add(stage2_formula)

# Stage 3
stage3_formula = tmp3 == (tmp2 ^ 0x4841434B45525321)
solver.add(stage3_formula)

# Stage 4
stage4_formula = tmp4 == (tmp3 - 12345678)
solver.add(stage4_formula)

# Final constraint
final_constraint = tmp4 == 0x5443474D489DFDD3
solver.add(final_constraint)

# Check for a solution
if solver.check() == sat:
    model = solver.model()
    key_value = model[key].as_long()
    print(f"The correct value of key is: {hex(key_value)}")
else:
    print("No solution found.")