Fix smt2 code generation for partially initialized memowy words, fixes #831

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 418f8d76651f3677dc3aad23fb346dd7b172e874..7f3cc94cadbcb33063f248306ffe8b078c6b3aab 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1103,20 +1103,27 @@ struct Smt2Worker
                                                        break;
 
                                                Const initword = init_data.extract(i*width, width, State::Sx);
+                                               Const initmask = initword;
                                                bool gen_init_constr = false;
 
-                                               for (auto bit : initword.bits)
-                                                       if (bit == State::S0 || bit == State::S1)
+                                               for (int k = 0; k < GetSize(initword); k++) {
+                                                       if (initword[k] == State::S0 || initword[k] == State::S1) {
                                                                gen_init_constr = true;
+                                                               initmask[k] = State::S1;
+                                                       } else {
+                                                               initmask[k] = State::S0;
+                                                               initword[k] = State::S0;
+                                                       }
+                                               }
 
                                                if (gen_init_constr)
                                                {
                                                        if (statebv)
                                                                /* FIXME */;
                                                        else
-                                                               init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+                                                               init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #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));
+                                                                               initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
                                                }
                                        }
                                }