aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-03-29 20:41:50 +0200
committerJannis Harder <me@jix.one>2022-03-29 20:41:50 +0200
commit8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad (patch)
tree58c09be23af44eecc58c9acb473f3af9ab501860 /backends/smt2/smtbmc.py
parent48d7a6c477e24eba64716d12a1ac17b5c9109450 (diff)
downloadyosys-8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad.tar.gz
yosys-8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad.tar.bz2
yosys-8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad.zip
smtbmc: fix bmc with no assertions
this was broken by the `--keep-going` changes
Diffstat (limited to 'backends/smt2/smtbmc.py')
-rw-r--r--backends/smt2/smtbmc.py2
1 files changed, 2 insertions, 0 deletions
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":