From 6f416c19537fcaab27b26d66c3144b468cec136a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 11 Sep 2016 18:08:56 +0200 Subject: [PATCH] Added missing :produce-models setting to smtio.py --- backends/smt2/smtio.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 62fb5154f..5d0a78485 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -90,7 +90,7 @@ class SmtIo: popen_vargs = ['mathsat'] if self.solver == "boolector": - popen_vargs = ['boolector', '--smt2', '-i', '-m'] + popen_vargs = ['boolector', '--smt2', '-i'] self.unroll = True if self.unroll: @@ -110,6 +110,7 @@ class SmtIo: self.topmod = None def setup(self, logic="ALL", info=None): + self.write("(set-option :produce-models true)") self.write("(set-logic %s)" % logic) if info is not None: self.write("(set-info :source |%s|)" % info) -- 2.30.2