Added reads that were missing in collectModelInfo

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9015ac741cb88dc39aba0f54d6ed7a0f95166bd6..7aa6d8597833b6a5532f67b59bfa6a46a9195373 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -698,6 +698,8 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
     // For each read, require that the rep stores the right value
     vector<Node>& reads = selects[n];
     for (unsigned j = 0; j < reads.size(); ++j) {
+      m->addTerm(reads[j]);
+      m->addTerm(reads[j][1]);
       rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
     }
     m->assertEquality(n, rep, true);