Make collect model info return a Bool (#1421)

48 files changed, 347 insertions, 176 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 985799e88..e354305d7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -106,9 +106,9 @@ bool TheoryArith::isExtfReduced( int effort, Node n, Node on, std::vector< Node
 void TheoryArith::propagate(Effort e) {
   d_internal->propagate(e);
 }
-
-void TheoryArith::collectModelInfo( TheoryModel* m ){
-  d_internal->collectModelInfo(m);
+bool TheoryArith::collectModelInfo(TheoryModel* m)
+{
+  return d_internal->collectModelInfo(m);
 }
 
 void TheoryArith::notifyRestart(){
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e1226279a..1c10bde0d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -61,7 +61,7 @@ public:
   bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
   bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp );
 
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m) override;
 
   void shutdown(){ }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c9a220566..8313abd68 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4252,7 +4252,8 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
   return belowMin;
 }
 
-void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
+bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
+{
   AlwaysAssert(d_qflraStatus ==  Result::SAT);
   //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
 
@@ -4288,7 +4289,10 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
         Node qNode = mkRationalNode(qmodel);
         Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
 
-        m->assertEquality(term, qNode, true);
+        if (!m->assertEquality(term, qNode, true))
+        {
+          return false;
+        }
       }else{
         Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl;
 
@@ -4301,6 +4305,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){
   // m->assertEqualityEngine(&ee);
 
   Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl;
+  return true;
 }
 
 bool TheoryArithPrivate::safeToReset() const {
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index b2471c5e8..08b884a03 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -444,7 +444,7 @@ public:
 
   Rational deltaValueForTotalOrder() const;
 
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m);
 
   void shutdown(){ }
 
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:
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 565c454e3..0e7614221 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -207,7 +207,7 @@ public:
    * @param fullModel whether to create a "full model," i.e., add
    * constants to equivalence classes that don't already have them
    */
-  void collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   void setProofLog( BitVectorProof * bvp );
 
   typedef TNodeSet::const_iterator vars_iterator;
@@ -292,7 +292,7 @@ public:
 
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
-  void collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   void setProofLog( BitVectorProof * bvp );
 };
 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 50070b29a..01282880c 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -123,9 +123,10 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode>& formulas) {
   return true;
 }
 
-void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   AlwaysAssert(!d_useAig && d_bitblaster);
-  d_bitblaster->collectModelInfo(m, fullModel);
+  return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
 void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; }
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index d259d49e6..856de530d 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -47,7 +47,7 @@ class EagerBitblastSolver {
   void turnOffAig();
   bool isInitialized();
   void initialize();
-  void collectModelInfo(theory::TheoryModel* m, bool fullModel);
+  bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
   void setProofLog(BitVectorProof* bvp);
 
  private:
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index b347ddccf..a3442e4c6 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -136,8 +136,9 @@ void BVQuickCheck::popToZero() {
   }
 }
 
-void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) {
-  d_bitblaster->collectModelInfo(model, fullModel);
+bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
+{
+  return d_bitblaster->collectModelInfo(model, fullModel);
 }
 
 BVQuickCheck::~BVQuickCheck() {
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index c5fe63ad6..d163bf7f9 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -97,7 +97,7 @@ public:
    * @return 
    */
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
-  void collectModelInfo(theory::TheoryModel* model, bool fullModel); 
+  bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
 
   typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
   vars_iterator beginVars(); 
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 454f89b6c..63dd53407 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -75,7 +75,7 @@ class SubtheorySolver {
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
   virtual void propagate(Theory::Effort e) {}
-  virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+  virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0;
   virtual Node getModelValue(TNode var) = 0;
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index c5313b9e7..a6e3153cb 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -676,7 +676,8 @@ void AlgebraicSolver::assertFact(TNode fact) {
 EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_UNKNOWN;
 }
-void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
+bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
+{
   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
   AlwaysAssert (!d_quickSolver->inConflict());
   set<Node> termSet;
@@ -729,9 +730,12 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n";
     // Doesn't have to be constant as it may be irrelevant
     Assert (subst.getKind() == kind::CONST_BITVECTOR);
-    model->assertEquality(variables[i], subst, true);
+    if (!model->assertEquality(variables[i], subst, true))
+    {
+      return false;
+    }
   }
-
+  return true;
  }
 
 Node AlgebraicSolver::getModelValue(TNode node) {
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 4b4103e44..0534c0f17 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -227,8 +227,8 @@ public:
   void  preRegister(TNode node) {}
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");}
-  EqualityStatus getEqualityStatus(TNode a, TNode b); 
-  void collectModelInfo(TheoryModel* m, bool fullModel); 
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   Node getModelValue(TNode node); 
   bool isComplete();
   virtual void assertFact(TNode fact);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 77e596d1f..b9467c168 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -234,7 +234,8 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
   return d_bitblaster->getEqualityStatus(a, b);
 }
 
-void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 4bbe4327e..5927feddc 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -69,7 +69,7 @@ public:
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
   void bitblastQueue();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 54f454dca..8ef2b471f 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -396,7 +396,8 @@ bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
   return utils::isEqualityTerm(term, seen); 
 }
 
-void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   if (d_useSlicer) {
     Unreachable(); 
   }
@@ -409,17 +410,24 @@ void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
   set<Node> termSet;
   d_bv->computeRelevantTerms(termSet);
-  m->assertEqualityEngine(&d_equalityEngine, &termSet);
+  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  {
+    return false;
+  }
   if (isComplete()) {
     Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
       Node a = it->first;
       Node b = it->second;
       Debug("bitvector-model") << "CoreSolver::collectModelInfo modelValues "
-                               << a << " => " << b <<")\n"; 
-      m->assertEquality(a, b, true);
+                               << a << " => " << b <<")\n";
+      if (!m->assertEquality(a, b, true))
+      {
+        return false;
+      }
     }
   }
+  return true;
 }
 
 Node CoreSolver::getModelValue(TNode var) {
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index b416e019d..6cc6253ff 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -105,7 +105,7 @@ public:
   void  preRegister(TNode node);
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
-  void  collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   Node  getModelValue(TNode var);
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index d662f056b..d828cc892 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -182,15 +182,19 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 void InequalitySolver::propagate(Theory::Effort e) {
   Assert (false);
 }
-
-void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
   std::vector<Node> model;
   d_inequalityGraph.getAllValuesInModel(model);
   for (unsigned i = 0; i < model.size(); ++i) {
     Assert (model[i].getKind() == kind::EQUAL);
-    m->assertEquality(model[i][0], model[i][1], true);
+    if (!m->assertEquality(model[i][0], model[i][1], true))
+    {
+      return false;
+    }
   }
+  return true;
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 1123d15ae..be0492125 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -69,7 +69,7 @@ public:
   void propagate(Theory::Effort e);
   void explain(TNode literal, std::vector<TNode>& assumptions);
   bool isComplete() { return d_isComplete; }
-  void collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
   Node getModelValue(TNode var);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
   void assertFact(TNode fact);
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 29f6e7800..e2bfec893 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -219,7 +219,8 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   return utils::mkConst(BitVector(bits.size(), value));
 }
 
-void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   TNodeSet::iterator it = d_variables.begin();
   for (; it != d_variables.end(); ++it) {
     TNode var = *it;
@@ -234,10 +235,14 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
         Debug("bitvector-model")
             << "EagerBitblaster::collectModelInfo (assert (= " << var << " "
             << const_value << "))\n";
-        m->assertEquality(var, const_value, true);
+        if (!m->assertEquality(var, const_value, true))
+        {
+          return false;
+        }
       }
     }
   }
+  return true;
 }
 
 void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 32aff1fb0..7976097e1 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -484,7 +484,8 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   return utils::mkConst(BitVector(bits.size(), value));
 }
 
-void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
   std::set<Node> termSet;
   d_bv->computeRelevantTerms(termSet);
 
@@ -504,9 +505,13 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
                                << var << " "
                                << const_value << "))\n";
-        m->assertEquality(var, const_value, true);
+      if (!m->assertEquality(var, const_value, true))
+      {
+        return false;
+      }
     }
   }
+  return true;
 }
 
 void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e03cecdd9..cb214217c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,18 +576,21 @@ bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
 bool TheoryBV::needsCheckLastEffort() {
   return d_needsLastCallCheck;
 }
-
-void TheoryBV::collectModelInfo( TheoryModel* m ){
+bool TheoryBV::collectModelInfo(TheoryModel* m)
+{
   Assert(!inConflict());
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver->collectModelInfo(m, true);
+    if (!d_eagerSolver->collectModelInfo(m, true))
+    {
+      return false;
+    }
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
-      d_subtheories[i]->collectModelInfo(m, true);
-      return;
+      return d_subtheories[i]->collectModelInfo(m, true);
     }
   }
+  return true;
 }
 
 Node TheoryBV::getModelValue(TNode var) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c21938aa7..a425cbdc8 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -80,7 +80,7 @@ public:
 
   Node explain(TNode n);
 
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m) override;
 
   std::string identify() const { return std::string("TheoryBV"); }
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 674e0d6b3..c17c022a1 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1490,7 +1490,8 @@ void TheoryDatatypes::computeCareGraph(){
   Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
 }
 
-void TheoryDatatypes::collectModelInfo( TheoryModel* m ){
+bool TheoryDatatypes::collectModelInfo(TheoryModel* m)
+{
   Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
   Trace("dt-model") << std::endl;
   printModelDebug( "dt-model" );
@@ -1502,7 +1503,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){
   getRelevantTerms(termSet);
 
   //combine the equality engine
-  m->assertEqualityEngine( &d_equalityEngine, &termSet );
+  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  {
+    return false;
+  }
 
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1579,7 +1583,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){
     }
     if( !neqc.isNull() ){
       Trace("dt-cmi") << "Assign : " << neqc << std::endl;
-      m->assertEquality( eqc, neqc, true );
+      if (!m->assertEquality(eqc, neqc, true))
+      {
+        return false;
+      }
       eqc_cons[ eqc ] = neqc;
     }
     if( addCons ){
@@ -1598,14 +1605,18 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){
         std::map< Node, int > vmap;
         Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 );
         Trace("dt-cmi") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
-        m->assertEquality( eqc, v, true );
-        m->assertRepresentative( v );
+        if (!m->assertEquality(eqc, v, true))
+        {
+          return false;
+        }
+        m->assertSkeleton(v);
       }
     }else{
       Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl;
-      m->assertRepresentative( it->second );
+      m->assertSkeleton(it->second);
     }
   }
+  return true;
 }
 
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 3c0a7c7cf..b3d88bb1c 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -264,7 +264,7 @@ public:
   void presolve();
   void addSharedTerm(TNode t);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m) override;
   void shutdown() { }
   std::string identify() const { return std::string("TheoryDatatypes"); }
   /** equality engine */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 276edfc0a..5be4a4601 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -578,7 +578,8 @@ Node TheoryFp::getModelValue(TNode var) {
   return d_conv.getValue(d_valuation, var);
 }
 
-void TheoryFp::collectModelInfo(TheoryModel *m) {
+bool TheoryFp::collectModelInfo(TheoryModel *m)
+{
   std::set<Node> relevantTerms;
 
   Trace("fp-collectModelInfo")
@@ -632,10 +633,13 @@ void TheoryFp::collectModelInfo(TheoryModel *m) {
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    m->assertEquality(node, d_conv.getValue(d_valuation, node), true);
+    if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+    {
+      return false;
+    }
   }
 
-  return;
+  return true;
 }
 
 bool TheoryFp::NotifyClass::eqNotifyTriggerEquality(TNode equality,
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 5205f5e23..614cbff46 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -46,7 +46,7 @@ class TheoryFp : public Theory {
   void check(Effort);
 
   Node getModelValue(TNode var);
-  void collectModelInfo(TheoryModel* m);
+  bool collectModelInfo(TheoryModel* m) override;
 
   std::string identify() const { return "THEORY_FP"; }
 
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);
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 59a85de1f..34dde7fc8 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -562,14 +562,22 @@ void QuantifiersEngine::check( Theory::Effort e ){
           static_cast<QuantifiersModule::QEffort>(qef);
       d_curr_effort_level = quant_e;
       //build the model if any module requested it
-      if( needsModelE==quant_e && !d_model->isBuilt() ){
-        // theory engine's model builder is quantifier engine's builder if it has one
-        Assert( !d_builder || d_builder==d_te->getModelBuilder() );
-        Trace("quant-engine-debug") << "Build model..." << std::endl;
-        if( !d_te->getModelBuilder()->buildModel( d_model ) ){
-          //we are done if model building was unsuccessful
-          Trace("quant-engine-debug") << "...added lemmas." << std::endl;
-          flushLemmas();
+      if (needsModelE == quant_e)
+      {
+        if (!d_model->isBuilt())
+        {
+          // theory engine's model builder is quantifier engine's builder if it
+          // has one
+          Assert(!d_builder || d_builder == d_te->getModelBuilder());
+          Trace("quant-engine-debug") << "Build model..." << std::endl;
+          if (!d_te->getModelBuilder()->buildModel(d_model))
+          {
+            flushLemmas();
+          }
+        }
+        if (!d_model->isBuiltSuccess())
+        {
+          break;
         }
       }
       if( !d_hasAddedLemma ){
@@ -690,16 +698,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
-    if( options::produceModels() ){
-      if( d_model->isBuilt() ){
-        Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl;
-      }else{
-        //use default model builder when no module built the model
-        Trace("quant-engine-debug") << "Build the default model..." << std::endl;
-        d_te->getModelBuilder()->buildModel( d_model );
-        Trace("quant-engine-debug") << "Done building the model." << std::endl;
-      }
-    }
     if( setIncomplete ){
       Trace("quant-engine") << "Set incomplete flag." << std::endl;
       getOutputChannel().setIncomplete();
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 71cde2841..0107b80c8 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -200,15 +200,15 @@ void TheorySep::computeCareGraph() {
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-void TheorySep::collectModelInfo( TheoryModel* m ){
+bool TheorySep::collectModelInfo(TheoryModel* m)
+{
   set<Node> termSet;
 
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
 
   // Send the equality engine information to the model
-  m->assertEqualityEngine( &d_equalityEngine, &termSet );
+  return m->assertEqualityEngine(&d_equalityEngine, &termSet);
 }
 
 void TheorySep::postProcessModel( TheoryModel* m ){
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 591a495d0..65f076631 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -109,13 +109,12 @@ class TheorySep : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   public:
+   bool collectModelInfo(TheoryModel* m) override;
+   void postProcessModel(TheoryModel* m);
 
-  void collectModelInfo(TheoryModel* m);
-  void postProcessModel(TheoryModel* m);
-
-  /////////////////////////////////////////////////////////////////////////////
-  // NOTIFICATIONS
-  /////////////////////////////////////////////////////////////////////////////
+   /////////////////////////////////////////////////////////////////////////////
+   // NOTIFICATIONS
+   /////////////////////////////////////////////////////////////////////////////
 
   private:
   public:
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 263d61934..9fcf3c089 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -50,8 +50,9 @@ bool TheorySets::needsCheckLastEffort() {
   return d_internal->needsCheckLastEffort();
 }
 
-void TheorySets::collectModelInfo(TheoryModel* m) {
-  d_internal->collectModelInfo(m);
+bool TheorySets::collectModelInfo(TheoryModel* m)
+{
+  return d_internal->collectModelInfo(m);
 }
 
 void TheorySets::computeCareGraph() {
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 3ecd404bb..1f0fbdd1f 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -52,7 +52,7 @@ public:
   
   bool needsCheckLastEffort();
 
-  void collectModelInfo(TheoryModel* m);
+  bool collectModelInfo(TheoryModel* m) override;
 
   void computeCareGraph();
 
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 3013711eb..6bafbb0de 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1911,16 +1911,19 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 /******************** Model generation ********************/
 /******************** Model generation ********************/
 
-
-void TheorySetsPrivate::collectModelInfo(TheoryModel* m) {
+bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
+{
   Trace("sets-model") << "Set collect model info" << std::endl;
   set<Node> termSet;
   // Compute terms appearing in assertions and shared terms
   d_external.computeRelevantTerms(termSet);
   
   // Assert equalities and disequalities to the model
-  m->assertEqualityEngine(&d_equalityEngine,&termSet);
-  
+  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  {
+    return false;
+  }
+
   std::map< Node, Node > mvals;
   for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
     Node eqc = d_set_eqc[i];
@@ -1970,10 +1973,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m) {
       rep = Rewriter::rewrite( rep );
       Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
       mvals[eqc] = rep;
-      m->assertEquality( eqc, rep, true );
-      m->assertRepresentative( rep );
+      if (!m->assertEquality(eqc, rep, true))
+      {
+        return false;
+      }
+      m->assertSkeleton(rep);
     }
   }
+  return true;
 }
 
 /********************** Helper functions ***************************/
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 175e82bb8..bd63ff43d 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -178,7 +178,7 @@ public:
   
   bool needsCheckLastEffort();
 
-  void collectModelInfo(TheoryModel* m);
+  bool collectModelInfo(TheoryModel* m);
 
   void computeCareGraph();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9b259bf97..e6b8807e9 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -447,8 +447,8 @@ void TheoryStrings::presolve() {
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-void TheoryStrings::collectModelInfo( TheoryModel* m ) {
+bool TheoryStrings::collectModelInfo(TheoryModel* m)
+{
   Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
   Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
   
@@ -458,9 +458,12 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) {
   // Compute terms appearing in assertions and shared terms
   //computeRelevantTerms(termSet);
   //m->assertEqualityEngine( &d_equalityEngine, &termSet );
-  
-  m->assertEqualityEngine( &d_equalityEngine );
-  
+
+  if (!m->assertEqualityEngine(&d_equalityEngine))
+  {
+    return false;
+  }
+
   // Generate model
   std::vector< Node > nodes;
   getEquivalenceClasses( nodes );
@@ -554,7 +557,10 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) {
         ++sel;
         Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl;
         processed[pure_eq[j]] = c;
-        m->assertEquality( pure_eq[j], c, true );
+        if (!m->assertEquality(pure_eq[j], c, true))
+        {
+          return false;
+        }
       }
     }
   }
@@ -583,11 +589,15 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) {
       Assert( cc.getKind()==kind::CONST_STRING );
       Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl;
       processed[nodes[i]] = cc;
-      m->assertEquality( nodes[i], cc, true );
+      if (!m->assertEquality(nodes[i], cc, true))
+      {
+        return false;
+      }
     }
   }
   //Trace("strings-model") << "String Model : Assigned." << std::endl;
   Trace("strings-model") << "String Model : Finished." << std::endl;
+  return true;
 }
 
 /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 39ab70e2f..70706bbd4 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -214,11 +214,11 @@ private:
   // MODEL GENERATION
   /////////////////////////////////////////////////////////////////////////////
 public:
-  void collectModelInfo(TheoryModel* m);
+ bool collectModelInfo(TheoryModel* m) override;
 
-  /////////////////////////////////////////////////////////////////////////////
-  // NOTIFICATIONS
-  /////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////
+ // NOTIFICATIONS
+ /////////////////////////////////////////////////////////////////////////////
 public:
   void presolve();
   void shutdown() { }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 0f820ac8e..204c514a9 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -512,9 +512,11 @@ public:
    * Get all relevant information in this theory regarding the current
    * model.  This should be called after a call to check( FULL_EFFORT )
    * for all theories with no conflicts and no lemmas added.
+   *
+   * This method returns true if and only if the equality engine of m is
+   * consistent as a result of this call.
    */
-  virtual void collectModelInfo( TheoryModel* m ){ }
-
+  virtual bool collectModelInfo(TheoryModel* m) { return true; }
   /** if theories want to do something with model after building, do it here */
   virtual void postProcessModel( TheoryModel* m ){ }
   /**
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 944185b31..4e2062c43 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -605,8 +605,6 @@ void TheoryEngine::check(Theory::Effort effort) {
             if( theory->needsCheckLastEffort() ){
               if( !d_curr_model->isBuilt() ){
                 if( !d_curr_model_builder->buildModel(d_curr_model) ){
-                  //model building should fail only if the model builder adds lemmas
-                  Assert( needCheck() );
                   break;
                 }
               }
@@ -617,10 +615,14 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
       if( ! d_inConflict && ! needCheck() ){
         if(d_logicInfo.isQuantified()) {
-          // quantifiers engine must pass effort last call check
+          // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
-          // if returning incomplete or SAT, we have ensured that d_curr_model has been built
-        } else if(options::produceModels() && !d_curr_model->isBuilt()) {
+        }
+      }
+      if (!d_inConflict && !needCheck())
+      {
+        if (options::produceModels() && !d_curr_model->isBuilt())
+        {
           // must build model at this point
           d_curr_model_builder->buildModel(d_curr_model);
         }
@@ -631,14 +633,21 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
-      //we will answer SAT
+      // case where we are about to answer SAT
       if( d_masterEqualityEngine != NULL ){
         AlwaysAssert(d_masterEqualityEngine->consistent());
       }
-      if( options::produceModels() ){
-        d_curr_model_builder->debugCheckModel(d_curr_model);  
-        // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
-        postProcessModel(d_curr_model);
+      if (d_curr_model->isBuilt())
+      {
+        // model construction should always succeed unless lemmas were added
+        AlwaysAssert(d_curr_model->isBuiltSuccess());
+        if (options::produceModels())
+        {
+          d_curr_model_builder->debugCheckModel(d_curr_model);
+          // Do post-processing of model from the theories (used for THEORY_SEP
+          // to construct heap model)
+          postProcessModel(d_curr_model);
+        }
       }
     }
   } catch(const theory::Interrupted&) {
@@ -846,7 +855,8 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
   return true;
 }
 
-void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
+bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+{
   //have shared term engine collectModelInfo
   //  d_sharedTerms.collectModelInfo( m );
   // Consult each active theory to get all relevant information
@@ -854,7 +864,10 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_logicInfo.isTheoryEnabled(theoryId)) {
       Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
-      d_theoryTable[theoryId]->collectModelInfo( m );
+      if (!d_theoryTable[theoryId]->collectModelInfo(m))
+      {
+        return false;
+      }
     }
   }
   // Get the Boolean variables
@@ -870,8 +883,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
       value = false;
     }
     Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
-    m->assertPredicate(var, value);
+    if (!m->assertPredicate(var, value))
+    {
+      return false;
+    }
   }
+  return true;
 }
 
 void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 179530240..f380e86aa 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -707,7 +707,7 @@ public:
   /**
    * collect model info
    */
-  void collectModelInfo( theory::TheoryModel* m );
+  bool collectModelInfo(theory::TheoryModel* m);
   /** post process model */
   void postProcessModel( theory::TheoryModel* m );
 
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 02dd92ad7..5555e29e2 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -25,8 +25,13 @@ using namespace CVC4::context;
 namespace CVC4 {
 namespace theory {
 
-TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
-  d_substitutions(c, false), d_modelBuilt(false), d_enableFuncModels(enableFuncModels)
+TheoryModel::TheoryModel(context::Context* c,
+                         std::string name,
+                         bool enableFuncModels)
+    : d_substitutions(c, false),
+      d_modelBuilt(false),
+      d_modelBuiltSuccess(false),
+      d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -53,6 +58,7 @@ TheoryModel::~TheoryModel() throw() {
 
 void TheoryModel::reset(){
   d_modelBuilt = false;
+  d_modelBuiltSuccess = false;
   d_modelCache.clear();
   d_comment_str.clear();
   d_sep_heap = Node::null();
@@ -333,20 +339,24 @@ void TheoryModel::addTermInternal(TNode n)
 }
 
 /** assert equality */
-void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
+bool TheoryModel::assertEquality(TNode a, TNode b, bool polarity)
+{
+  Assert(d_equalityEngine->consistent());
   if (a == b && polarity) {
-    return;
+    return true;
   }
   Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
   d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
-  Assert(d_equalityEngine->consistent());
+  return d_equalityEngine->consistent();
 }
 
 /** assert predicate */
-void TheoryModel::assertPredicate(TNode a, bool polarity ){
+bool TheoryModel::assertPredicate(TNode a, bool polarity)
+{
+  Assert(d_equalityEngine->consistent());
   if ((a == d_true && polarity) ||
       (a == d_false && (!polarity))) {
-    return;
+    return true;
   }
   if (a.getKind() == EQUAL) {
     Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
@@ -354,13 +364,15 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){
   } else {
     Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
     d_equalityEngine->assertPredicate( a, polarity, Node::null() );
-    Assert(d_equalityEngine->consistent());
   }
+  return d_equalityEngine->consistent();
 }
 
 /** assert equality engine */
-void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
+bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
+                                       set<Node>* termSet)
 {
+  Assert(d_equalityEngine->consistent());
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   for (; !eqcs_i.isFinished(); ++eqcs_i) {
     Node eqc = (*eqcs_i);
@@ -384,11 +396,12 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
         continue;
       }
       if (predicate) {
-        if (predTrue) {
-          assertPredicate(*eqc_i, true);
-        }
-        else if (predFalse) {
-          assertPredicate(*eqc_i, false);
+        if (predTrue || predFalse)
+        {
+          if (!assertPredicate(*eqc_i, predTrue))
+          {
+            return false;
+          }
         }
         else {
           if (first) {
@@ -398,7 +411,10 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
           else {
             Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
             d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
-            Assert(d_equalityEngine->consistent());
+            if (!d_equalityEngine->consistent())
+            {
+              return false;
+            }
           }
         }
       } else {
@@ -413,17 +429,22 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
           first = false;
         }
         else {
-          assertEquality(*eqc_i, rep, true);
+          if (!assertEquality(*eqc_i, rep, true))
+          {
+            return false;
+          }
         }
       }
     }
   }
+  return true;
 }
 
-void TheoryModel::assertRepresentative(TNode n )
+void TheoryModel::assertSkeleton(TNode n)
 {
-  Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
-  Trace("model-builder-reps") << "Rep eqc is : " << getRepresentative( n ) << std::endl;
+  Trace("model-builder-reps") << "Assert skeleton : " << n << std::endl;
+  Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n)
+                              << std::endl;
   d_reps[ n ] = n;
 }
 
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 600f511c8..ab844c6ec 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -55,19 +55,25 @@ namespace theory {
  *
  * These calls may modify the model object using the interface
  * functions below, including:
- * - assertEquality, assertPredicate, assertRepresentative,
+ * - assertEquality, assertPredicate, assertSkeleton,
  *   assertEqualityEngine.
  * - assignFunctionDefinition
  *
- * During and after this building process, these calls may use
- * interface functions below to guide the model construction:
+ * This class provides several interface functions:
  * - hasTerm, getRepresentative, areEqual, areDisequal
  * - getEqualityEngine
  * - getRepSet
  * - hasAssignedFunctionDefinition, getFunctionsToAssign
+ * - getValue
  *
- * After this building process, the function getValue can be
- * used to query the value of nodes.
+ * The above functions can be used for a model m after it has been
+ * successfully built, i.e. when m->isBuiltSuccess() returns true.
+ *
+ * Additionally, all of the above functions, with the exception of getValue,
+ * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
+ * documented in theory_model_builder.h. In particular, we make calls to the
+ * above functions such as getRepresentative() when assigning total
+ * interpretations for uninterpreted functions.
  */
 class TheoryModel : public Model
 {
@@ -80,7 +86,7 @@ public:
   virtual void reset();
   /** is built
    *
-   * Have we (attempted to) build this model since the last
+   * Have we attempted to build this model since the last
    * call to reset? Notice for model building techniques
    * that are not guaranteed to succeed (such as
    * when quantified formulas are enabled), a true return
@@ -88,22 +94,51 @@ public:
    * current assertions.
    */
   bool isBuilt() { return d_modelBuilt; }
+  /** is built success
+   *
+   * Was this model successfully built since the last call to reset?
+   */
+  bool isBuiltSuccess() { return d_modelBuiltSuccess; }
   //---------------------------- for building the model
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
-  /** assert equality holds in the model */
-  void assertEquality(TNode a, TNode b, bool polarity);
-  /** assert predicate holds in the model */
-  void assertPredicate(TNode a, bool polarity);
-  /** assert all equalities/predicates in equality engine hold in the model */
-  void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
-  /** assert representative
-    *  This function tells the model that n should be the representative of its equivalence class.
-    *  It should be called during model generation, before final representatives are chosen.  In the
-    *  case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
-    *  functions.
-    */
-  void assertRepresentative(TNode n);
+  /** assert equality holds in the model
+   *
+   * This method returns true if and only if the equality engine of this model
+   * is consistent after asserting the equality to this model.
+   */
+  bool assertEquality(TNode a, TNode b, bool polarity);
+  /** assert predicate holds in the model
+   *
+   * This method returns true if and only if the equality engine of this model
+   * is consistent after asserting the predicate to this model.
+   */
+  bool assertPredicate(TNode a, bool polarity);
+  /** assert all equalities/predicates in equality engine hold in the model
+   *
+   * This method returns true if and only if the equality engine of this model
+   * is consistent after asserting the equality engine to this model.
+   */
+  bool assertEqualityEngine(const eq::EqualityEngine* ee,
+                            std::set<Node>* termSet = NULL);
+  /** assert skeleton
+   *
+   * This method gives a "skeleton" for the model value of the equivalence
+   * class containing n. This should be an application of interpreted function
+   * (e.g. datatype constructor, array store, set union chain). The subterms of
+   * this term that are variables or terms that belong to other theories will
+   * be filled in with model values.
+   *
+   * For example, if we call assertSkeleton on (C x y) where C is a datatype
+   * constructor and x and y are variables, then the equivalence class of
+   * (C x y) will be interpreted in m as (C x^m y^m) where
+   * x^m = m->getValue( x ) and y^m = m->getValue( y ).
+   *
+   * It should be called during model generation, before final representatives
+   * are chosen. In the case of TheoryEngineModelBuilder, it should be called
+   * during Theory's collectModelInfo( ... ) functions.
+   */
+  void assertSkeleton(TNode n);
   //---------------------------- end building the model
 
   // ------------------- general equality queries
@@ -171,8 +206,10 @@ public:
  protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
-  /** whether this model has been built */
+  /** whether we have tried to build this model in the current context */
   bool d_modelBuilt;
+  /** whether this model has been built successfully */
+  bool d_modelBuiltSuccess;
   /** special local context for our equalityEngine so we can clear it
    * independently of search context */
   context::Context* d_eeContext;
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index ac12b37e3..e88d1e3be 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -286,11 +286,15 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
 
   // mark as built
   tm->d_modelBuilt = true;
+  tm->d_modelBuiltSuccess = false;
 
   // Collect model info from the theories
   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
                          << std::endl;
-  d_te->collectModelInfo(tm);
+  if (!d_te->collectModelInfo(tm))
+  {
+    return false;
+  }
 
   // model-builder specific initialization
   if (!preProcessBuildModel(tm))
@@ -799,6 +803,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   }
   else
   {
+    tm->d_modelBuiltSuccess = true;
     return true;
   }
 }
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index c24d50cbf..bb74569b7 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -58,7 +58,8 @@ class TheoryEngineModelBuilder : public ModelBuilder
    * (4) assign constants to all equivalence classes
    *     of m's equality engine, through alternating
    *     iterations of evaluation and enumeration,
-   * (5) builder-specific post-processing.
+   * (5) builder-specific processing, which includes assigning total
+   *     interpretations to uninterpreted functions.
    *
    * This function returns false if any of the above
    * steps results in a lemma sent on an output channel.
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f97a4b639..38ddb1246 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -330,14 +330,18 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
   return mkAnd(assumptions);
 }
 
-void TheoryUF::collectModelInfo( TheoryModel* m ){
+bool TheoryUF::collectModelInfo(TheoryModel* m)
+{
   Debug("uf") << "UF : collectModelInfo " << std::endl;
   set<Node> termSet;
 
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
 
-  m->assertEqualityEngine( &d_equalityEngine, &termSet );
+  if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+  {
+    return false;
+  }
 
   if( options::ufHo() ){
     for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
@@ -345,12 +349,16 @@ void TheoryUF::collectModelInfo( TheoryModel* m ){
       if( n.getKind()==kind::APPLY_UF ){
         // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY
         Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n );
-        m->assertEquality( n, hn, true );
+        if (!m->assertEquality(n, hn, true))
+        {
+          return false;
+        }
       }
     }
   }
 
   Debug("uf") << "UF : finish collectModelInfo " << std::endl;
+  return true;
 }
 
 void TheoryUF::presolve() {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 0665b8272..269aa63db 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -242,7 +242,7 @@ public:
   void preRegisterTerm(TNode term);
   Node explain(TNode n);
 
-  void collectModelInfo( TheoryModel* m );
+  bool collectModelInfo(TheoryModel* m) override;
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
   void presolve();