diff options
| -rw-r--r-- | miasm2/ir/translators/smt2.py | 7 |
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 |