github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-03-06 11:34:02 +00:00
Code Issues Releases Wiki Activity

Do not change solver output parsing for non-exists-forall problems.

Browse Source
This commit is contained in:
Alberto Gonzalez
2020-03-26 21:23:07 +00:00
parent 5accf08ef9
commit d72cb8ea2a
1 changed files with 6 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
backends/smt2/smtio.py
View File

@@ -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: