smtbmc: fix bmc with no assertions
authorJannis Harder <me@jix.one>
Tue, 29 Mar 2022 18:41:50 +0000 (20:41 +0200)
committerJannis 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

index df60b9b261bdbe9bb651e610326609ed99fdb463..137182f333a57bab27f0e1e2a0ce9e79552f4346 100644 (file)
@@ -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":