diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-09 03:18:00 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-09 03:18:00 +0000 |
| commit | cad60d99f8fe38dd5098d14958d2dd844bbe6584 (patch) | |
| tree | 17c94c55f1b3165b800c6781cd840c9bdb77179e /src/theory/arrays | |
| parent | 2979089be3bc655d8bdd6245e193f356b4f7c93c (diff) | |
Fix for another model assertion failure
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 |
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); |