mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Merge pull request #244 from jix/smtbmc-cover-keepgoing

Browse source
This commit is contained in:
Jannis Harder 2023-06-26 16:35:56 +02:00 committed by GitHub
parent c027aea3db 28c053bd94
commit 4d1ac0115c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_engine_smtbmc.py
View file

@ -69,8 +69,6 @@ def run(mode, task, engine_idx, engine):
task.error("smtbmc options --basecase and --induction are exclusive.") task.error("smtbmc options --basecase and --induction are exclusive.")
induction_only = True induction_only = True
elif o == "--keep-going": 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 keep_going = True
elif o == "--seed": elif o == "--seed":
random_seed = a random_seed = a
@ -134,7 +132,8 @@ def run(mode, task, engine_idx, engine):
if keep_going and mode != "prove_induction": if keep_going and mode != "prove_induction":
smtbmc_opts.append("--keep-going") smtbmc_opts.append("--keep-going")
trace_prefix += "%" if mode != "cover":
trace_prefix += "%"
if dumpsmt2: if dumpsmt2:
smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"] smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]