smt2 translator: added model generation flag

1 files changed, 6 insertions, 1 deletions

diff --git a/miasm2/ir/translators/smt2.py b/miasm2/ir/translators/smt2.py
index e832d3b8..695d62cf 100644
--- a/miasm2/ir/translators/smt2.py
+++ b/miasm2/ir/translators/smt2.py
@@ -286,13 +286,14 @@ class TranslatorSMT2(Translator):
         dst = self.from_expr(expr.dst)
         return smt2_assert(smt2_eq(src, dst))
 
-    def to_smt2(self, exprs, logic="QF_ABV"):
+    def to_smt2(self, exprs, logic="QF_ABV", model=False):
         """
         Converts a valid SMT2 file for a given list of
         SMT2 expressions.
 
         :param exprs: list of SMT2 expressions
         :param logic: SMT2 logic
+        :param model: model generation flag
         :return: String of the SMT2 file
         """
         ret = ""
@@ -315,6 +316,10 @@ class TranslatorSMT2(Translator):
         # define action
         ret += "(check-sat)\n"
 
+        # enable model generation
+        if model:
+            ret += "(get-model)\n"
+
         return ret