diff options
| author | Miodrag Milanović <mmicko@gmail.com> | 2022-03-29 21:20:07 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-03-29 21:20:07 +0200 |
| commit | d44f618de52af4122a4d927863516d91a2145314 (patch) | |
| tree | 58c09be23af44eecc58c9acb473f3af9ab501860 | |
| parent | 48d7a6c477e24eba64716d12a1ac17b5c9109450 (diff) | |
| parent | 8b15f3a548571fd4736c76b5cc0b0b8e8cfc4fad (diff) | |
| download | yosys-d44f618de52af4122a4d927863516d91a2145314.tar.gz yosys-d44f618de52af4122a4d927863516d91a2145314.tar.bz2 yosys-d44f618de52af4122a4d927863516d91a2145314.zip | |
Merge pull request #3258 from jix/fix-no-assertions
smtbmc: fix bmc with no assertions
| -rw-r--r-- | backends/smt2/smtbmc.py | 2 |
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": |