From f9744fdfcd8106107e2bef750c36c04ae2406973 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Jun 2023 10:27:38 +0200 Subject: [PATCH] smtbmc: Make cover mode respect --keep-going As cover mode by default stops looking for further traces when an assertion fails, it should respect --keep-going. --- backends/smt2/smtbmc.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 6b81740a2..02e15a1b5 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -174,6 +174,8 @@ def help(): further failed assertions. To output multiple traces covering all found failed assertions, the character '%' is replaced in all dump filenames with an increasing number. + In cover mode, don't stop when a cover trace contains a failed + assertion. --check-witness check that the used witness file contains sufficient @@ -1739,7 +1741,7 @@ elif covermode: smt_pop() smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask)) - if found_failed_assert: + if found_failed_assert and not keep_going: break if "1" not in cover_mask: