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...)?