From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 11 Jan 2017 13:14:12 +0000 (+0100)
Subject: Fix $initstate handling bug in yosys-smtbmc
X-Git-Tag: yosys-0.8~536
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7cfb7dbd250a8595589f86e1b38b67015c7b9c5;p=yosys.git

Fix $initstate handling bug in yosys-smtbmc
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 8dbb047aa..ecee6795e 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -789,6 +789,7 @@ else:  # not tempind
         for i in range(1, step_size):
             if step+i < num_steps:
                 smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
+                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i))
                 smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
                 smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
                 smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
@@ -812,6 +813,7 @@ else:  # not tempind
                         for i in range(last_check_step+1, last_check_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))