summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/theory_arrays.cpp2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f66f3f7a4..4931a18f0 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -707,8 +707,6 @@ 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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback