From 40b387a70b2e3757bd8c8612758b0333761473a1 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 3 Jul 2024 22:12:06 +0100 Subject: [PATCH] smtbmc: Support skipping steps in cover mode --- backends/smt2/smtbmc.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c3bdcebbe..1dcedc8ca 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1866,6 +1866,11 @@ elif covermode: smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step)) smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) + if step < skip_steps: + print_msg("Skipping step %d.." % (step)) + step += 1 + continue + while "1" in cover_mask: print_msg("Checking cover reachability in step %d.." % (step)) smt_push()