From 3d66e7cec548dcd25b77e3991fa6090421eebe86 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 8 Dec 2018 07:16:19 +0100 Subject: [PATCH] Fixes and improvements in BTOR engine Signed-off-by: Clifford Wolf --- sbysrc/sby_core.py | 4 ++-- sbysrc/sby_engine_btor.py | 6 +++++- 2 files changed, 7 insertions(+), 3 deletions(-) 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: -- 2.30.2