From: Claire Wolf <claire@symbioticeda.com>
Date: Mon, 20 Jul 2020 17:35:32 +0000 (+0200)
Subject: Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
X-Git-Tag: working-ls180~369^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a207cb362cc4b682a37060f380362b23c927805e;p=yosys.git

Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 03f001bfd..69dab5590 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1275,10 +1275,10 @@ def smt_pop():
     asserts_consequent_cache.pop()
     smt.write("(pop 1)")
 
-def smt_check_sat():
+def smt_check_sat(expected=["sat", "unsat"]):
     if asserts_cache_dirty:
         smt_forall_assert()
-    return smt.check_sat()
+    return smt.check_sat(expected=expected)
 
 if tempind:
     retstatus = "FAILED"
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 72ab39d39..4ac437c36 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -653,7 +653,7 @@ class SmtIo:
 
         return stmt
 
-    def check_sat(self):
+    def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]):
         if self.debug_print:
             print("> (check-sat)")
         if self.debug_file and not self.nocomments:
@@ -740,7 +740,7 @@ class SmtIo:
             print("(check-sat)", file=self.debug_file)
             self.debug_file.flush()
 
-        if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]:
+        if result not in expected:
             if result == "":
                 print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
             else: