smtbmc: Fix induction trace filename with --keep-going for the basecase
authorJannis Harder <me@jix.one>
Thu, 23 Jun 2022 11:15:58 +0000 (13:15 +0200)
committerJannis Harder <me@jix.one>
Thu, 23 Jun 2022 11:15:58 +0000 (13:15 +0200)
--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

index 4ec365de18b00927eaecd08b65b706328b4b471d..091776342f888cb3394cd794ecc4fedc02e0eb04 100644 (file)
@@ -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 += "%"