From 7824460e27eb65cf240ab92e306b4be57eb0b161 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 21 Mar 2022 18:36:09 +0100 Subject: [PATCH] Initial support for the new smtbmc --keep-going option So far this only passes on the option and adjusts the trace_prefix to support multiple numbered traces. Further changes are needed to correctly associate individual traces with the assertions failing in that trace. --- sbysrc/sby_engine_smtbmc.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 492e2a5..9b7ff2b 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -31,11 +31,12 @@ def run(mode, task, engine_idx, engine): progress = False basecase_only = False induction_only = False + keep_going = False random_seed = None task.precise_prop_status = True opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", - "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="]) + "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "keep-going", "seed="]) for o, a in opts: if o == "--nomem": @@ -66,6 +67,10 @@ def run(mode, task, engine_idx, engine): if basecase_only: task.error("smtbmc options --basecase and --induction are exclusive.") induction_only = True + elif o == "--keep-going": + if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"): + task.error("smtbmc option --keep-going is only supported in bmc and prove mode.") + keep_going = True elif o == "--seed": random_seed = a else: @@ -126,6 +131,10 @@ def run(mode, task, engine_idx, engine): smtbmc_opts.append("-c") trace_prefix += "%" + if keep_going: + smtbmc_opts.append("--keep-going") + trace_prefix += "%" + if dumpsmt2: smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"] -- 2.30.2