diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index af417f740..508c9d8ff 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1038,8 +1038,7 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - -void TheoryArrays::collectModelInfo( TheoryModel* m ) +bool TheoryArrays::collectModelInfo(TheoryModel* m) { set<Node> termSet; @@ -1140,7 +1139,10 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) } while (changed); // Send the equality engine information to the model - m->assertEqualityEngine(&d_equalityEngine, &termSet); + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + { + return false; + } // Build a list of all the relevant reads, indexed by the store representative std::map<Node, std::vector<Node> > selects; @@ -1215,11 +1217,15 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) for (unsigned j = 0; j < reads.size(); ++j) { rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]); } - m->assertEquality(n, rep, true); + if (!m->assertEquality(n, rep, true)) + { + return false; + } if (!n.isConst()) { - m->assertRepresentative(rep); + m->assertSkeleton(rep); } } + return true; } ///////////////////////////////////////////////////////////////////////////// |