Make collect model info return a Bool (#1421)

2 files changed, 15 insertions, 10 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;
 }
 
 /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 08d1618c2..24c286e92 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -248,12 +248,11 @@ class TheoryArrays : public Theory {
   private:
 
   public:
+   bool collectModelInfo(TheoryModel* m) override;
 
-  void collectModelInfo(TheoryModel* m);
-
-  /////////////////////////////////////////////////////////////////////////////
-  // NOTIFICATIONS
-  /////////////////////////////////////////////////////////////////////////////
+   /////////////////////////////////////////////////////////////////////////////
+   // NOTIFICATIONS
+   /////////////////////////////////////////////////////////////////////////////
 
   private:
   public: