smt2 mem init bugfix

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 000240a731c3ef5f50fd305ca747708734873032..8d82d1baa525e2882497f3fc6f2e5775f2970997 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -742,7 +742,7 @@ struct Smt2Worker
 
                                        for (int i = 0; i < memsize; i++)
                                        {
-                                               if (GetSize(init_data) < i*width)
+                                               if (i*width >= GetSize(init_data))
                                                        break;
 
                                                Const initword = init_data.extract(i*width, width, State::Sx);
@@ -752,9 +752,11 @@ struct Smt2Worker
                                                        if (bit == State::S0 || bit == State::S1)
                                                                gen_init_constr = true;
 
-                                               init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
-                                                               get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-                                                               initword.as_string().c_str(), get_id(cell), i));
+                                               if (gen_init_constr) {
+                                                       init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+                                                                       get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+                                                                       initword.as_string().c_str(), get_id(cell), i));
+                                               }
                                        }
                                }
                        }