diff options
| author | Claire Wolf <clifford@clifford.at> | 2020-03-27 16:48:38 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-27 16:48:38 +0100 |
| commit | 4c38895fab3ca2426ffc23e40601f3042a953e47 (patch) | |
| tree | 4b8d37358dfc7eb03b17f720a6d1b1de923cc30f | |
| parent | 590d8eccb7d2c58de27ecc7f9ac71cd226b1be29 (diff) | |
| parent | d72cb8ea2abfd0346e67868ef4ba04d2069db271 (diff) | |
| download | yosys-4c38895fab3ca2426ffc23e40601f3042a953e47.tar.gz yosys-4c38895fab3ca2426ffc23e40601f3042a953e47.tar.bz2 yosys-4c38895fab3ca2426ffc23e40601f3042a953e47.zip | |
Merge pull request #1815 from boqwxp/fix-ef-optimize
Fix solver output parsing for exists-forall optimization
| -rw-r--r-- | backends/smt2/smtio.py | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3559781ec..69f59df79 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -704,7 +704,13 @@ class SmtIo: if msg is not None: print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True) - result = self.read() + if self.forall: + result = self.read() + while result not in ["sat", "unsat", "unknown"]: + print("%s %s: %s" % (self.timestamp(), self.solver, result)) + result = self.read() + else: + result = self.read() if self.debug_file: print("(set-info :status %s)" % result, file=self.debug_file) |