Fixes and improvements in BTOR engine

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 7d9e76faf091d881679fbf1bde064fc2561e31fc..e572f5cb77eb263de9bc6a6a470ccef880fe7a24 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -533,8 +533,8 @@ class SbyJob:
                 self.opt_skip = None
             else:
                 for engine in self.engines:
-                    if engine[0] != "smtbmc":
-                        self.error("Option skip is only valid for smtbmc engine.")
+                    if engine[0] not in ["smtbmc", "btor"]:
+                        self.error("Option skip is only valid for smtbmc and btor engines.")
 
         self.copy_src()
 

diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index 146a91e079b0b88e7dc6780cc470394eb7563c8f..ec536b6f283b221d22950b70ac0a042c2e92f6f7 100644 (file)
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -29,7 +29,7 @@ def run(mode, job, engine_idx, engine):
         job.error("Unexpected BTOR engine options.")
 
     if solver_args[0] == "btormc":
-        solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax %d" % job.opt_depth
+        solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax %d" % (job.opt_depth - 1)
         if job.opt_skip is not None:
             solver_cmd += " -kmin %d" % job.opt_skip
         solver_cmd += " ".join([""] + solver_args[1:])
@@ -64,6 +64,10 @@ def run(mode, job, engine_idx, engine):
             return "No CEX up to depth %d." % (int(line[1:])-1)
 
         if solver_args[0] == "btormc":
+            if "calling BMC on" in line:
+                return line
+            if "SATISFIABLE" in line:
+                return line
             if "bad state properties at bound" in line:
                 return line
             if "deleting model checker:" in line: