TranslatorZ3: Fixed from_ExprId when expr.name is an asmlabel

TODO: replace the asmlabel str by its offset?

2 files changed, 7 insertions, 1 deletions

diff --git a/miasm2/ir/translators/z3_ir.py b/miasm2/ir/translators/z3_ir.py
index 564670a6..db038fe1 100644
--- a/miasm2/ir/translators/z3_ir.py
+++ b/miasm2/ir/translators/z3_ir.py
@@ -117,7 +117,7 @@ class TranslatorZ3(Translator):
 
     @classmethod
     def from_ExprId(cls, expr):
-        return z3.BitVec(expr.name, expr.size)
+        return z3.BitVec(str(expr), expr.size)
 
     @classmethod
     def from_ExprMem(cls, expr):
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index 5f8f3e45..fa656ed0 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -1,5 +1,6 @@
 import z3
 
+from miasm2.core.asmbloc import asm_label
 from miasm2.expression.expression import *
 from miasm2.ir.translators.translator import Translator
 from miasm2.ir.translators.z3_ir import TranslatorZ3, Z3Mem
@@ -137,5 +138,10 @@ for miasm_int, res in [(five, -5), (four, -4)]:
     z3_e6 = z3.BitVecVal(res, 32)
     assert equiv(ez3, z3_e6)
 
+# --------------------------------------------------------------------------
+# Should just not throw anything
+e7 = ExprId(asm_label("label_histoire", 0xdeadbeef), 32)
+ez3 = Translator.to_language('z3').from_expr(e7)
+
 print "TranslatorZ3 tests are OK."