From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 23 Oct 2012 20:02:56 +0000 (+0000)
Subject: Added reads that were missing in collectModelInfo
X-Git-Tag: cvc5-1.0.0~7685
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=62ff31bde206239d7abc9bb66c658131d8138f62;p=cvc5.git

Added reads that were missing in collectModelInfo
---

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);