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 03f001bfd0952cb28e5652c594e631e979c123bf..69dab5590373c41d2c1a050a68bac1e19102079d 100644 (file)
--- 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 72ab39d396fc4079f370a0c13e6d38de2fe776e8..4ac437c36a916c1b9bbbe48fbf14267f69c8b96c 100644 (file)
--- 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: