Add support for "yosys-smtbmc -c --append"

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 39ac181dd0f9d6a7bd57301d0d071b943fde4c2d..92a9a1a218bdcea2c55663d075f5f0e8592280a1 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -872,6 +872,18 @@ elif covermode:
                 smt.write("(pop 1)")
                 break
 
+            if append_steps > 0:
+                for i in range(step+1, step+1+append_steps):
+                    print_msg("Appending additional step %d." % i)
+                    smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod))
+                    smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i))
+                    smt.write("(assert (|%s_u| s%d))" % (topmod, i))
+                    smt.write("(assert (|%s_h| s%d))" % (topmod, i))
+                    smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i))
+                    smt.write("(assert %s)" % get_constr_expr(constr_assumes, i))
+                print_msg("Re-solving with appended steps..")
+                assert smt.check_sat() == "sat"
+
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
             assert len(reached_covers) == len(cover_desc)
 
@@ -891,7 +903,7 @@ elif covermode:
                 if print_failed_asserts(i, extrainfo=" (step %d)" % i):
                     found_failed_assert = True
 
-            write_trace(0, step+1, "%d" % coveridx)
+            write_trace(0, step+1+append_steps, "%d" % coveridx)
 
             if found_failed_assert:
                 break