projects
/
yosys.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
48d7a6c
)
smtbmc: fix bmc with no assertions
author
Jannis Harder
<me@jix.one>
Tue, 29 Mar 2022 18:41:50 +0000
(20:41 +0200)
committer
Jannis Harder
<me@jix.one>
Tue, 29 Mar 2022 18:41:50 +0000
(20:41 +0200)
this was broken by the `--keep-going` changes
backends/smt2/smtbmc.py
patch
|
blob
|
history
diff --git
a/backends/smt2/smtbmc.py
b/backends/smt2/smtbmc.py
index df60b9b261bdbe9bb651e610326609ed99fdb463..137182f333a57bab27f0e1e2a0ce9e79552f4346 100644
(file)
--- 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":