From 8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 29 Mar 2022 20:41:50 +0200 Subject: [PATCH] smtbmc: fix bmc with no assertions this was broken by the `--keep-going` changes --- backends/smt2/smtbmc.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index df60b9b26..137182f33 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1589,6 +1589,8 @@ else: # not tempind, covermode active_assert_expr = "(and %s)" % " ".join(active_assert_exprs) smt_assert("(not %s)" % active_assert_expr) + else: + smt_assert("false") if smt_check_sat() == "sat": -- 2.30.2