Is there any efficient way to convert Z3's into assembly code?

Question

I need something like that for x86 arch:

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

After Z3 simplification I have got (memory 0x7FC70000 is symbolized):

bvadd (_ bv3423553726 32) MEM_0x7FC70000

The last step is converting Z3's AST into ASM code to get result like this:

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

Is there any efficient way to perform last step? Should I parse SMT formula and convert it manually (bv -> mov...)?