From 62ff31bde206239d7abc9bb66c658131d8138f62 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 23 Oct 2012 20:02:56 +0000
Subject: [PATCH] Added reads that were missing in collectModelInfo

---
 src/theory/arrays/theory_arrays.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9015ac741..7aa6d8597 100644
--- 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);
-- 
2.30.2