From 7cdbeb90aacb3cacacfc01fdbb9c8a6816f22d65 Mon Sep 17 00:00:00 2001 From: Tim Blazytko Date: Sun, 13 Mar 2016 15:25:27 +0100 Subject: smt2 translator: added model generation flag --- miasm2/ir/translators/smt2.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'miasm2') 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 -- cgit 1.4.1