Add "Unexpected response" handling to smtbmc engine

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

diff --git a/docs/examples/puzzles/primegen.sby b/docs/examples/puzzles/primegen.sby
index 20e5072d173467c698c7659ca6515fe5b9395b61..6d88b88511569ed178cb2e4cf64da2530bed2d21 100644 (file)
--- a/docs/examples/puzzles/primegen.sby
+++ b/docs/examples/puzzles/primegen.sby
@@ -6,7 +6,7 @@ primes_pass
 [options]
 mode cover
 depth 1
-primes_fail: expect fail
+primes_fail: expect fail,error
 
 [engines]
 smtbmc --dumpsmt2 --progress --stbv z3

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 65933d06c97ce7e92b1ebf21d529a45398400ee8..6d2ffc4765229c3fa1a2628672cf7ee37e51db66 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -37,7 +37,6 @@ def run(mode, job, engine_idx, engine):
             "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
 
     for o, a in opts:
-        print(o, a)
         if o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
@@ -169,6 +168,11 @@ def run(mode, job, engine_idx, engine):
             task_status = "ERROR"
             return line
 
+        match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line)
+        if match:
+            task_status = "ERROR"
+            return line
+
         return line
 
     def exit_callback(retcode):