assembly - 有没有什么有效的方法可以将 Z3 转换成汇编代码？

Question

对于 x86 拱门，我需要类似的东西：

mov edi, dword ptr [0x7fc70000]
add edi, 0x11
sub edi, 0x33F0B753

Z3简化后我得到了（内存0x7FC70000被符号化）：

bvadd (_ bv3423553726 32) MEM_0x7FC70000

最后一步是将 Z3 的 AST 转换为 ASM 代码以获得如下结果：

mov edi, dword ptr [0x7fc70000]
add edi, 0xCC0F48BE

有没有什么有效的方法来执行最后一步？我应该解析 SMT 公式并手动转换（bv -> mov ...）吗？