diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-23 20:02:56 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-23 20:02:56 +0000 |
| commit | 62ff31bde206239d7abc9bb66c658131d8138f62 (patch) | |
| tree | 32c5fdd79c9208c7563d027bb7352f239595668e /src/theory/arrays | |
| parent | 408855d37c90c701508b5207cb3588e09cc12583 (diff) | |
Added reads that were missing in collectModelInfo
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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); |