From: Jannis Harder <me@jix.one>
Date: Tue, 29 Mar 2022 18:41:50 +0000 (+0200)
Subject: smtbmc: fix bmc with no assertions
X-Git-Tag: yosys-0.16~16^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad;p=yosys.git

smtbmc: fix bmc with no assertions

this was broken by the `--keep-going` changes
---

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":