From 3dcf7766ea716ddddea428268cae26f004afcf9f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 23 Jun 2022 13:15:58 +0200 Subject: [PATCH] smtbmc: Fix induction trace filename with --keep-going for the basecase --keep-going only applies to the basecase and induction runs without that option, so the trace filename for induction should have no placeholder. --- sbysrc/sby_engine_smtbmc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 4ec365d..0917763 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -131,7 +131,7 @@ def run(mode, task, engine_idx, engine): smtbmc_opts.append("-c") trace_prefix += "%" - if keep_going: + if keep_going and mode != "prove_induction": smtbmc_opts.append("--keep-going") trace_prefix += "%" -- 2.30.2