Make collect model info return a Bool (#1421)

2 files changed, 12 insertions, 4 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 66e05b1cd..a278274c3 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -120,16 +120,24 @@ void TheoryQuantifiers::computeCareGraph() {
   //do nothing
 }
 
-void TheoryQuantifiers::collectModelInfo(TheoryModel* m) {
+bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
+{
   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
     if((*i).assertion.getKind() == kind::NOT) {
       Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
-      m->assertPredicate((*i).assertion[0], false);
+      if (!m->assertPredicate((*i).assertion[0], false))
+      {
+        return false;
+      }
     } else {
       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
-      m->assertPredicate(*i, true);
+      if (!m->assertPredicate(*i, true))
+      {
+        return false;
+      }
     }
   }
+  return true;
 }
 
 void TheoryQuantifiers::check(Effort e) {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 9c621dbd6..295a39464 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -56,7 +56,7 @@ public:
   void check(Effort e);
   Node getNextDecisionRequest( unsigned& priority );
   Node getValue(TNode n);
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m) override;
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);