From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Thu, 26 Mar 2020 21:23:07 +0000 (+0000)
Subject: Do not change solver output parsing for non-exists-forall problems.
X-Git-Tag: working-ls180~727^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d72cb8ea2abfd0346e67868ef4ba04d2069db271;p=yosys.git

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

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: