Rating: 0

Encode asm into z3, then solve. Use SSA for efficiency.