aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
diff options
context:
space:
mode:
authorAlberto Gonzalez <boqwxp@airmail.cc>2020-03-26 21:23:07 +0000
committerAlberto Gonzalez <boqwxp@airmail.cc>2020-03-26 23:00:00 +0000
commitd72cb8ea2abfd0346e67868ef4ba04d2069db271 (patch)
treea9c63356722dd7f6373f28c1eb8b1a6fcf8539fb /backends/smt2
parent5accf08ef9f226b78cbd47c83522cce6afffb280 (diff)
downloadyosys-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.py8
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: