From 5accf08ef9f226b78cbd47c83522cce6afffb280 Mon Sep 17 00:00:00 2001
From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Thu, 26 Mar 2020 01:19:47 +0000
Subject: [PATCH 1/2] Skip reading stdout from the solver that if it isn't a
line reading only "sat", "unsat", or "unknown".
---
backends/smt2/smtio.py | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3559781ec..f7b2ec647 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -704,7 +704,9 @@ class SmtIo:
if msg is not None:
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
- result = self.read()
+ result = ""
+ while result not in ["sat", "unsat", "unknown"]:
+ result = self.read()
if self.debug_file:
print("(set-info :status %s)" % result, file=self.debug_file)
From d72cb8ea2abfd0346e67868ef4ba04d2069db271 Mon Sep 17 00:00:00 2001
From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Thu, 26 Mar 2020 21:23:07 +0000
Subject: [PATCH 2/2] Do not change solver output parsing for non-exists-forall
problems.
---
backends/smt2/smtio.py | 8 ++++++--
1 file 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: