diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-26 21:23:07 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-03-26 23:00:00 +0000 |
| commit | d72cb8ea2abfd0346e67868ef4ba04d2069db271 (patch) | |
| tree | a9c63356722dd7f6373f28c1eb8b1a6fcf8539fb /backends/smt2 | |
| parent | 5accf08ef9f226b78cbd47c83522cce6afffb280 (diff) | |
| download | yosys-d72cb8ea2abfd0346e67868ef4ba04d2069db271.tar.gz yosys-d72cb8ea2abfd0346e67868ef4ba04d2069db271.tar.bz2 yosys-d72cb8ea2abfd0346e67868ef4ba04d2069db271.zip | |
Do not change solver output parsing for non-exists-forall problems.
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smtio.py | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index f7b2ec647..69f59df79 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -704,8 +704,12 @@ class SmtIo: if msg is not None: print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True) - result = "" - while result not in ["sat", "unsat", "unknown"]: + 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: |