diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-09-11 18:08:56 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-09-11 18:17:22 +0200 |
| commit | 6f416c19537fcaab27b26d66c3144b468cec136a (patch) | |
| tree | 308dc9868795617576551840562c8ee78291ad1a | |
| parent | 5199aafca0579aceb3b4a2ad1af610bcb4ccfcd1 (diff) | |
| download | yosys-6f416c19537fcaab27b26d66c3144b468cec136a.tar.gz yosys-6f416c19537fcaab27b26d66c3144b468cec136a.tar.bz2 yosys-6f416c19537fcaab27b26d66c3144b468cec136a.zip | |
Added missing :produce-models setting to smtio.py
| -rw-r--r-- | backends/smt2/smtio.py | 3 |
1 files changed, 2 insertions, 1 deletions
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) |