From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 8 Dec 2018 06:16:19 +0000 (+0100)
Subject: Fixes and improvements in BTOR engine
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d66e7cec548dcd25b77e3991fa6090421eebe86;p=SymbiYosys.git

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 7d9e76f..e572f5c 100644
--- 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 146a91e..ec536b6 100644
--- 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: