Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.

27 files changed, 1104 insertions, 802 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 585ef3dc2..e5f2922a7 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -253,8 +253,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option cegqiUnifCondSol --cegqi-unif-csol bool :default false
-  enable approach which unifies conditional solutions
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -271,9 +269,13 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   
 option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
   template mode for sygus invariant synthesis
+option sygusUnifCondSol --sygus-unif-csol bool :default false
+  enable approach which unifies conditional solutions
 
 option sygusDirectEval --sygus-direct-eval bool :default true
   direct unfolding of evaluation functions
+option sygusCRefEval --sygus-cref-eval bool :default false
+  direct evaluation of refinement lemmas for conflict analysis
   
 # approach applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
diff --git a/src/smt/model.h b/src/smt/model.h
index fd31655f4..523751d9c 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -75,7 +75,7 @@ class ModelBuilder {
 public:
   ModelBuilder() { }
   virtual ~ModelBuilder() { }
-  virtual void buildModel(Model* m, bool fullModel) = 0;
+  virtual bool buildModel(Model* m) = 0;
 };/* class ModelBuilder */
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b9ef8f7c4..8e641aca1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1749,6 +1749,12 @@ void SmtEngine::setDefaults() {
       options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE );
     }
   }
+  if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+    if( !d_logic.isPure(THEORY_UF) ){
+      //MBQI_ABS is only supported in pure quantified UF
+      options::mbqiMode.set( quantifiers::MBQI_FMC );
+    }
+  } 
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 11903f863..4a47618f1 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1420,7 +1420,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 
   //combine the equality engine
   m->assertEqualityEngine( &d_equalityEngine, &termSet );
-  
 
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
@@ -1430,25 +1429,25 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
   while( !eqccs_i.isFinished() ){
     Node eqc = (*eqccs_i);
     //for all equivalence classes that are datatypes
-    if( termSet.find( eqc )==termSet.end() ){
-      Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
-    }else{
-      if( eqc.getType().isDatatype() ){
-        EqcInfo* ei = getOrMakeEqcInfo( eqc );
-        if( ei && !ei->d_constructor.get().isNull() ){
-          Node c = ei->d_constructor.get();
-          cons.push_back( c );
-          eqc_cons[ eqc ] = c;
-        }else{
-          //if eqc contains a symbol known to datatypes (a selector), then we must assign
-          //should assign constructors to EQC if they have a selector or a tester
-          bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
-          if( shouldConsider ){
-            nodes.push_back( eqc );
-          }
+    //if( termSet.find( eqc )==termSet.end() ){
+    //  Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl;
+    //}
+    if( eqc.getType().isDatatype() ){
+      EqcInfo* ei = getOrMakeEqcInfo( eqc );
+      if( ei && !ei->d_constructor.get().isNull() ){
+        Node c = ei->d_constructor.get();
+        cons.push_back( c );
+        eqc_cons[ eqc ] = c;
+      }else{
+        //if eqc contains a symbol known to datatypes (a selector), then we must assign
+        //should assign constructors to EQC if they have a selector or a tester
+        bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc );
+        if( shouldConsider ){
+          nodes.push_back( eqc );
         }
       }
     }
+    //}
     ++eqccs_i;
   }
 
@@ -2165,7 +2164,7 @@ void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
   // Compute terms appearing in assertions and shared terms
   computeRelevantTerms(termSet);
   
-  //also include non-singleton equivalence classes
+  //also include non-singleton equivalence classes  TODO : revisit this
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
@@ -2176,6 +2175,11 @@ void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
       TNode n = (*eqc_i);
       if( first.isNull() ){
         first = n;
+        //always include all datatypes
+        if( n.getType().isDatatype() ){
+          addedFirst = true;
+          termSet.insert( n );
+        }
       }else{
         if( !addedFirst ){
           addedFirst = true;
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 2ccc17e55..de55ecdba 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -586,7 +586,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
     //  exit( 10 );
     //}
     return true;
-  }else if( varChCount==1 && n.getKind()==EQUAL ){
+  }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
     Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;
     //expand the variable based on its finite domain
     AbsDef a;
@@ -598,7 +598,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
     Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;
     construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
     return true;
-  }else if( varChCount==2 && n.getKind()==EQUAL ){
+  }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
     Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;
     //efficient expansion of the equality
     construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none );
@@ -721,115 +721,112 @@ QModelBuilder( c, qe ){
 
 //------------------------model construction----------------------------
 
-void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
-  Trace("ambqi-debug") << "process build model " << fullModel << std::endl;
+bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
+  Trace("ambqi-debug") << "process build model " << std::endl;
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
-  if( fullModel ){
-    Trace("ambqi-model") << "Construct model representation..." << std::endl;
-    //make function values
-    for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      if( it->first.getType().getNumChildren()>1 ){
-        Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
-        m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
-      }
-    }
-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
-    //mark that the model has been set
-    fm->markModelSet();
-    //debug the model
-    debugModel( fm );
-  }else{
-    fm->initialize();
-    //process representatives
-    fm->d_rep_id.clear();
-    fm->d_domain.clear();
-
-    //initialize boolean sort
-    TypeNode b = d_true.getType();
-    fm->d_rep_set.d_type_reps[b].clear();
-    fm->d_rep_set.d_type_reps[b].push_back( d_false );
-    fm->d_rep_set.d_type_reps[b].push_back( d_true );
-    fm->d_rep_id[d_false] = 0;
-    fm->d_rep_id[d_true] = 1;
-
-    //initialize unintpreted sorts
-    Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Assert( !it->second.empty() );
-        //set the domain
-        fm->d_domain[it->first] = 0;
-        Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
-        for( unsigned i=0; i<it->second.size(); i++ ){
-          if( i<32 ){
-            fm->d_domain[it->first] |= ( 1 << i );
-          }
-          Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
-          fm->d_rep_id[it->second[i]] = i;
-        }
-        if( it->second.size()>=32 ){
-          fm->d_domain.erase( it->first );
+  fm->initialize();
+  //process representatives
+  fm->d_rep_id.clear();
+  fm->d_domain.clear();
+
+  //initialize boolean sort
+  TypeNode b = d_true.getType();
+  fm->d_rep_set.d_type_reps[b].clear();
+  fm->d_rep_set.d_type_reps[b].push_back( d_false );
+  fm->d_rep_set.d_type_reps[b].push_back( d_true );
+  fm->d_rep_id[d_false] = 0;
+  fm->d_rep_id[d_true] = 1;
+
+  //initialize unintpreted sorts
+  Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      Assert( !it->second.empty() );
+      //set the domain
+      fm->d_domain[it->first] = 0;
+      Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        if( i<32 ){
+          fm->d_domain[it->first] |= ( 1 << i );
         }
+        Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
+        fm->d_rep_id[it->second[i]] = i;
+      }
+      if( it->second.size()>=32 ){
+        fm->d_domain.erase( it->first );
       }
     }
+  }
 
-    Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
-    //construct the models for functions
-    for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      Node f = it->first;
-      Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
-      //reset the model
-      it->second->clear();
-      //get all (non-redundant) f-applications
-      std::vector< TNode > fapps;
-      Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
-      for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
-        Node n = fm->d_uf_terms[f][i];
+  Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
+  //construct the models for functions
+  for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+    Node f = it->first;
+    Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
+    //reset the model
+    it->second->clear();
+    //get all (non-redundant) f-applications
+    std::vector< TNode > fapps;
+    Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
+    std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f );
+    if( itut!=fm->d_uf_terms.end() ){
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = itut->second[i];
         if( d_qe->getTermDatabase()->isTermActive( n ) ){
           Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
           fapps.push_back( n );
         }
       }
-      if( fapps.empty() ){
-        //choose arbitrary value
-        Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
-        Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
-        fapps.push_back( mbt );
-      }
-      bool fValid = true;
-      for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
-        if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
-          Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
-          Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
-          fValid = false;
-          break;
-        }
+    }
+    if( fapps.empty() ){
+      //choose arbitrary value
+      Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+      Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+      fapps.push_back( mbt );
+    }
+    bool fValid = true;
+    for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
+      if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
+        Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
+        Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
+        fValid = false;
+        break;
       }
-      fm->d_models_valid[f] = fValid;
-      if( fValid ){
-        //construct the ambqi model
-        it->second->construct_func( fm, fapps );
-        Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
-        it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
-        Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
-        it->second->simplify( fm, TNode::null(), fapps[0] );
-        Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
-        it->second->debugPrint("ambqi-model", fm, fapps[0] );
+    }
+    fm->d_models_valid[f] = fValid;
+    if( fValid ){
+      //construct the ambqi model
+      it->second->construct_func( fm, fapps );
+      Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
+      it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
+      Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
+      it->second->simplify( fm, TNode::null(), fapps[0] );
+      Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
+      it->second->debugPrint("ambqi-model", fm, fapps[0] );
 
 /*
-        if( Debug.isOn("ambqi-model-debug") ){
-          for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
-            Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
-            Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
-            Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
-          }
+      if( Debug.isOn("ambqi-model-debug") ){
+        for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+          Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+          Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+          Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
         }
-*/
       }
+*/
+    }
+  }
+  Trace("ambqi-model") << "Construct model representation..." << std::endl;
+  //make function values
+  for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+    if( it->first.getType().getNumChildren()>1 ){
+      Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
+      m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
     }
   }
+  Assert( d_addedLemmas==0 );
+  return TheoryEngineModelBuilder::processBuildModel( m );
 }
 
 
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 0adaef638..68cb27038 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -91,7 +91,7 @@ public:
   AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
   ~AbsMbqiBuilder() throw() {}
   //process build model
-  void processBuildModel(TheoryModel* m, bool fullModel);
+  bool processBuildModel(TheoryModel* m);
   //do exhaustive instantiation
   int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
 };
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 3d5066c08..41face8f7 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -615,10 +615,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
   getBounds( f, v, rsi, l, u );
   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
   if( !l.isNull() ){
-    l = d_quantEngine->getModel()->getCurrentModelValue( l );
+    l = d_quantEngine->getModel()->getValue( l );
   }
   if( !u.isNull() ){
-    u = d_quantEngine->getModel()->getCurrentModelValue( u );
+    u = d_quantEngine->getModel()->getValue( u );
   }
   Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
   return;
@@ -656,7 +656,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
   Node sr = getSetRange( q, v, rsi );
   if( !sr.isNull() ){
     Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
-    sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
+    sr = d_quantEngine->getModel()->getValue( sr );
     //if non-constant, then sr does not occur in the model, we fail
     if( !sr.isConst() ){
       return Node::null();
@@ -679,7 +679,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
         for( unsigned i = 0; it != it_end; ++ it, ++i ){
           Node lit = (*it).assertion;
           if( lit.getKind()==kind::MEMBER ){
-            Node vr = d_quantEngine->getModel()->getCurrentModelValue( lit[0] );
+            Node vr = d_quantEngine->getModel()->getValue( lit[0] );
             Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl;
             Trace("bound-int-rsi-debug") << "  " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl;
             if( val_to_term.find( vr )!=val_to_term.end() ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 999c554b5..713b9ed6f 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -81,7 +81,7 @@ void CegConjecture::assign( Node q ) {
         }
       }
     }
-    if( options::cegqiUnifCondSol() ){
+    if( options::sygusUnifCondSol() ){
       // for each variable, determine whether we can do conditional counterexamples
       for( unsigned i=0; i<d_candidates.size(); i++ ){
         registerCandidateConditional( d_candidates[i] );
@@ -295,7 +295,7 @@ bool CegConjecture::needsRefinement() {
 }
 
 void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){
-  Assert( options::cegqiUnifCondSol() );
+  Assert( options::sygusUnifCondSol() );
   std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
   if( it!=d_cinfo.end() ){
     if( !it->second.d_csol_cond.isNull() ){
@@ -323,7 +323,7 @@ void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Nod
 }
 
 void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
-  if( options::cegqiUnifCondSol() && !forceOrig ){
+  if( options::sygusUnifCondSol() && !forceOrig ){
     for( unsigned i=0; i<d_candidates.size(); i++ ){
       getConditionalCandidateList( clist, d_candidates[i], true );
     }
@@ -333,7 +333,7 @@ void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig
 }
 
 Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ) {
-  Assert( options::cegqiUnifCondSol() );
+  Assert( options::sygusUnifCondSol() );
   std::map< Node, Node >::iterator itc = cmv.find( curr );
   if( itc!=cmv.end() ){
     return itc->second;
@@ -366,7 +366,7 @@ Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv,
 
 bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values ) {
   Assert( clist.size()==model_values.size() );
-  if( options::cegqiUnifCondSol() ){
+  if( options::sygusUnifCondSol() ){
     std::map< Node, Node > cmv;
     for( unsigned i=0; i<clist.size(); i++ ){
       cmv[ clist[i] ] = model_values[i];
@@ -403,7 +403,7 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector<
     //must get a counterexample to the value of the current candidate
     Node inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
     bool hasActiveConditionalNode = false;
-    if( options::cegqiUnifCondSol() ){
+    if( options::sygusUnifCondSol() ){
       //TODO
       hasActiveConditionalNode = true;
     }
@@ -446,7 +446,7 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector<
 }
 
 Node CegConjecture::getActiveConditional( Node curr ) {
-  Assert( options::cegqiUnifCondSol() );
+  Assert( options::sygusUnifCondSol() );
   std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
   Assert( it!=d_cinfo.end() );
   if( !it->second.d_csol_cond.isNull() ){
@@ -541,9 +541,9 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
   std::map< Node, std::vector< Node > > csol_ccond_ret;
   std::map< Node, std::map< Node, bool > > csol_cpol;
   std::vector< Node > csol_vals;
-  if( options::cegqiUnifCondSol() ){
+  if( options::sygusUnifCondSol() ){
     std::vector< Node > new_active_measure_sum;
-    Trace("cegqi-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl;
+    Trace("sygus-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl;
     for( unsigned i=0; i<d_candidates.size(); i++ ){
       Node v = d_candidates[i];
       Node ac = getActiveConditional( v );
@@ -557,11 +557,11 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
       //if it is a conditional
       if( !d_cinfo[ac].d_csol_cond.isNull() ){
         //activate
-        Trace("cegqi-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
+        Trace("sygus-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
         d_cinfo[ac].d_csol_status = 0;  //TODO
-        Trace("cegqi-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
-        Trace("cegqi-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
-        Trace("cegqi-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl;
+        Trace("sygus-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
+        Trace("sygus-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
+        Trace("sygus-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl;
         registerCandidateConditional( d_cinfo[ac].d_csol_var[1-d_cinfo[ac].d_csol_status] );
         //add to measure sum
         Node acfc = getMeasureTermFactor( d_cinfo[ac].d_csol_cond );
@@ -575,7 +575,7 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
         csol_cond[v] = d_cinfo[ac].d_csol_cond;
         csol_vals.push_back( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] );
       }else{
-        Trace("cegqi-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl;
+        Trace("sygus-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl;
         //if we have not already included this in the measure, do so
         if( d_cinfo[ac].d_csol_status==0 ){
           Node acf = getMeasureTermFactor( ac );
@@ -587,11 +587,23 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
         csol_vals.push_back( ac );
       }
       if( !csol_ccond[v].empty() ){
-        Trace("cegqi-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl;
+        Trace("sygus-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl;
       }
     }
     // must add to active measure
     if( !new_active_measure_sum.empty() ){
+      Node mcsum = new_active_measure_sum.size()==1 ? new_active_measure_sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, new_active_measure_sum );
+      Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, mcsum, d_active_measure_term );
+      Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
+      d_qe->getOutputChannel().lemma( mclem );
+/*
+      for( unsigned i=0; i<new_active_measure_sum.size(); i++ ){
+        Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, new_active_measure_sum[i], d_active_measure_term );
+        Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
+        d_qe->getOutputChannel().lemma( mclem );
+      }
+      */
+      /*
       Node new_active_measure = NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() );
       new_active_measure_sum.push_back( new_active_measure );
       Node namlem = NodeManager::currentNM()->mkNode( kind::GEQ, new_active_measure, NodeManager::currentNM()->mkConst(Rational(0)));
@@ -600,6 +612,7 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
       Trace("cegqi-lemma") << "Cegqi::Lemma : Measure expansion : " << namlem << std::endl;
       d_qe->getOutputChannel().lemma( namlem );
       d_active_measure_term = new_active_measure;
+      */
     }
   }
   Trace("cegqi-refine") << "Refine " << d_ce_sk.size() << " points." << std::endl;
@@ -635,11 +648,11 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
         }
       }
       //compute the body, inst_cond
-      if( options::cegqiUnifCondSol() && !c_disj.isNull() ){
-        Trace("cegqi-unif") << "Process " << c_disj << std::endl;
+      if( options::sygusUnifCondSol() && !c_disj.isNull() ){
+        Trace("sygus-unif") << "Process " << c_disj << std::endl;
         c_disj = purifyConditionalEvaluations( c_disj, csol_cond, psubs, psubs_visited );
-        Trace("cegqi-unif") << "Purified to : " << c_disj << std::endl;
-        Trace("cegqi-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
+        Trace("sygus-unif") << "Purified to : " << c_disj << std::endl;
+        Trace("sygus-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
       }else{
         //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
       }
@@ -662,9 +675,10 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
       }
     }
     if( success ){
-      Trace("cegqi-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl;
+      Assert( sk_vars.size()==sk_subs.size() );
+      Trace("sygus-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl;
       //add conditional correctness assumptions
-      std::map< Node, Node > psubs_condc;
+      std::vector< Node > psubs_condc;
       std::map< Node, std::vector< Node > > psubs_apply;
       std::vector< Node > paux_vars;
       for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){
@@ -676,8 +690,8 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
         }
         Node c = csol_cond[itp->first[0]];
         psubs_apply[ c ].push_back( itp->first );
-        Trace("cegqi-unif") << "   process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
-        Trace("cegqi-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl;
+        Trace("sygus-unif") << "   process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
+        Trace("sygus-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl;
         std::vector< Node> assm;
         if( !c.isNull() ){
           assm.push_back( mkConditional( c, args ) );
@@ -688,53 +702,29 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
         }
         Assert( !assm.empty() );
         Node condn = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm );
-        Node cond = NodeManager::currentNM()->mkNode( kind::IMPLIES, condn, itp->first.eqNode( itp->second ) );
-        psubs_condc[itp->first] = cond;
-        Trace("cegqi-unif") << "   ...made conditional correctness assumption : " << cond << std::endl;
-      }
-      for( std::map< Node, Node >::iterator itp = psubs_condc.begin(); itp != psubs_condc.end(); ++itp ){
-        lem_c.push_back( itp->second );
+        Node cond = NodeManager::currentNM()->mkNode( kind::OR, condn.negate(), itp->first.eqNode( itp->second ) );
+        cond = cond.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+        cond = cond.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+        psubs_condc.push_back( cond );
+        Trace("sygus-unif") << "   ...made conditional correctness assumption : " << cond << std::endl;
       }
       
-      Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
-      //substitute the actual return values
-      if( options::cegqiUnifCondSol() ){
-        Assert( d_candidates.size()==csol_vals.size() );
-        lem = lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
-      }
+      Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
       
-      //previous non-ground conditional refinement lemmas must satisfy the current point
-      for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){
-        Node prev_lem = d_refinement_lemmas[i];
-        prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-        //do auxiliary variable substitution
-        std::vector< Node > subs;
-        for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){
-          subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), 
-                                                              "purification variable for non-ground sygus conditional solution" ) );
-        }
-        prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() );
-        prev_lem = Rewriter::rewrite( prev_lem );
-        prev_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prev_lem );
-        Trace("cegqi-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
-        lems.push_back( prev_lem );
-      }
-      if( !isGround() && !csol_cond.empty() ){
-        Trace("cegqi-unif") << "Lemma " << lem << " is a non-ground conditional refinement lemma, store it for future instantiation." << std::endl;
-        d_refinement_lemmas.push_back( lem );
-        d_refinement_lemmas_aux_vars.push_back( paux_vars );
-      }
-      
-      if( options::cegqiUnifCondSol() ){
-        Trace("cegqi-unif") << "We have lemma : " << lem << std::endl;
-        Trace("cegqi-unif") << "Now add progress assertions..." << std::endl;
+      if( options::sygusUnifCondSol() ){
+        //substitute the actual return values
+        Assert( d_candidates.size()==csol_vals.size() );
+        base_lem = base_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+        Trace("sygus-unif") << "We have base lemma : " << base_lem << std::endl;
+        //progress lemmas
+        Trace("sygus-unif") << "Now add progress assertions..." << std::endl;
         std::vector< Node > prgr_conj;
         std::map< Node, bool > cprocessed;
         for( std::map< Node, Node >::iterator itc = csol_cond.begin(); itc !=csol_cond.end(); ++itc ){
           Node x = itc->first;
           Node c = itc->second;          
           if( !c.isNull() ){
-            Trace("cegqi-unif") << "  process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl;
+            Trace("sygus-unif") << "  process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl;
             //make the progress point
             Assert( x.getType().isDatatype() );
             const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype();
@@ -764,31 +754,69 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
               }
             }
             //the condition holds for the point
-            prgr_conj.push_back( mkConditional( c, prgr_pt ) );
+            Node cplem = mkConditional( c, prgr_pt );
             // ...and not for its context, if this return point is different from them
             //for( unsigned j=0; j<csol_ccond[x].size(); j++ ){
             //  Node cc = csol_ccond[x][j];
             //  prgr_conj.push_back( mkConditional( cc, prgr_pt, csol_cpol[x][cc] ) );
             //}
             //FIXME
+            d_refinement_lemmas_cprogress.push_back( cplem );
+            d_refinement_lemmas_cprogress_pts.push_back( prgr_pt );
+            prgr_conj.push_back( cplem );
           }
         }
         if( !prgr_conj.empty() ){
           Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj );
           prgr_lem = prgr_lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
-          Trace("cegqi-unif") << "Progress lemma is " << prgr_lem << std::endl;
-          lem = NodeManager::currentNM()->mkNode( kind::AND, lem, prgr_lem );
+          prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+          prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem );
+          Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl;
+          lems.push_back( prgr_lem );
+        }
+        
+        //previous non-ground conditional refinement lemmas must satisfy the current point
+        if( !isGround() ){
+          for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){
+            Node prev_lem = d_refinement_lemmas[i];
+            prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+            //do auxiliary variable substitution
+            std::vector< Node > subs;
+            for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){
+              subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), 
+                                                                  "purification variable for non-ground sygus conditional solution" ) );
+            }
+            prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() );
+            prev_lem = Rewriter::rewrite( prev_lem );
+            Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
+            lems.push_back( prev_lem );
+          }
         }
-        //make in terms of new values
-        Assert( csol_vals.size()==d_candidates.size() );
-        Trace("cegqi-unif") << "Now rewrite in terms of new evaluation branches...got " << lem << std::endl;
       }
-      //apply the substitution
-      Assert( sk_vars.size()==sk_subs.size() );
-      lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+      
+      //make the base lemma
+      base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+      d_refinement_lemmas_base.push_back( base_lem );
+      
+      Node lem = base_lem;
+      
+      if( options::sygusUnifCondSol() ){
+        d_refinement_lemmas_ceval.push_back( psubs_condc );
+        //add the conditional evaluation
+        if( !psubs_condc.empty() ){
+          std::vector< Node > children;
+          children.push_back( base_lem );
+          children.insert( children.end(), psubs_condc.begin(), psubs_condc.end() );
+          lem = NodeManager::currentNM()->mkNode( AND, children );
+        }
+      }
+
       lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
       lem = Rewriter::rewrite( lem );
       lems.push_back( lem );
+      
+      d_refinement_lemmas.push_back( lem );
+      d_refinement_lemmas_aux_vars.push_back( paux_vars );
     }
   }
   d_ce_sk.clear();
@@ -932,7 +960,7 @@ void CegInstantiation::registerQuantifier( Node q ) {
       //fairness
       if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
         std::vector< Node > mc;
-        if( options::cegqiUnifCondSol() || 
+        if( options::sygusUnifCondSol() || 
             d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED  ){
           //measure term is a fresh constant
           mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
@@ -1049,24 +1077,50 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       std::vector< Node > model_values;
       if( conj->getModelValues( clist, model_values ) ){
         if( options::sygusDirectEval() ){
+          bool addedEvalLemmas = false;
+          if( options::sygusCRefEval() ){
+            Trace("cegqi-debug") << "Do cref evaluation..." << std::endl;
+            // see if any refinement lemma is refuted by evaluation
+            std::vector< Node > cre_lems;
+            getCRefEvaluationLemmas( conj, clist, model_values, cre_lems );
+            if( !cre_lems.empty() ){
+              Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..." << std::endl;
+              for( unsigned j=0; j<cre_lems.size(); j++ ){
+                Node lem = cre_lems[j];
+                Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
+                if( d_quantEngine->addLemma( lem ) ){
+                  addedEvalLemmas = true;
+                }
+              }
+              if( addedEvalLemmas ){
+                return;
+              }
+            }
+          }
           Trace("cegqi-debug") << "Do direct evaluation..." << std::endl;
-          std::vector< Node > eager_eval_lem;
+          std::vector< Node > eager_terms; 
+          std::vector< Node > eager_vals; 
+          std::vector< Node > eager_exps;
           for( unsigned j=0; j<clist.size(); j++ ){
-          Trace("cegqi-debug") << "  register " << clist[j] << " -> " << model_values[j] << std::endl;
-            d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_eval_lem );
+            Trace("cegqi-debug") << "  register " << clist[j] << " -> " << model_values[j] << std::endl;
+            d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_terms, eager_vals, eager_exps );
           }
-          Trace("cegqi-debug") << "...produced " << eager_eval_lem.size()  << " eager evaluation lemmas." << std::endl;
-          if( !eager_eval_lem.empty() ){
+          Trace("cegqi-debug") << "...produced " << eager_terms.size()  << " eager evaluation lemmas." << std::endl;
+          if( !eager_terms.empty() ){
             Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
-            for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
-              Node lem = eager_eval_lem[j];
+            for( unsigned j=0; j<eager_terms.size(); j++ ){
+              Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) );
               if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
                 //FIXME: hack to incorporate hacks from BV for division by zero
                 lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
               }
               Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
-              d_quantEngine->addLemma( lem );
+              if( d_quantEngine->addLemma( lem ) ){
+                addedEvalLemmas = true;
+              }
             }
+          }
+          if( addedEvalLemmas ){
             return;
           }
         }
@@ -1160,6 +1214,171 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   }
 }
 
+void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
+  if( conj->getNumRefinementLemmas()>0 ){
+    Assert( vs.size()==ms.size() );
+    std::map< Node, Node > vtm;
+    for( unsigned i=0; i<vs.size(); i++ ){
+      vtm[vs[i]] = ms[i];
+    }
+    std::map< Node, Node > visited;
+    std::map< Node, std::vector< Node > > exp;
+    for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){
+      Node lem;
+      std::vector< Node > cvars;
+      if( options::sygusUnifCondSol() ){
+        //TODO : progress lemma
+        std::map< Node, Node > visitedc;
+        std::map< Node, std::vector< Node > > expc;
+        for( unsigned j=0; j<conj->getNumConditionalEvaluations( i ); j++ ){
+          Node ce = conj->getConditionalEvaluation( i, j );
+          Node cee = crefEvaluate( ce, vtm, visitedc, expc );
+          Trace("sygus-cref-eval") << "Check conditional evaluation : " << ce << ", evaluates to " << cee << std::endl;
+          if( !cee.isNull() && cee.getKind()==kind::EQUAL ){
+            // the conditional holds, we will apply this as a substitution
+            for( unsigned r=0; r<2; r++ ){
+              if( cee[r].isVar() && cee[1-r].isConst() ){
+                Node v = cee[r];
+                Node c = cee[1-r];
+                cvars.push_back( v );
+                Assert( exp.find( v )==exp.end() );
+                //TODO : should also carry symbolic solution (do not eagerly unfold conclusion of ce)
+                visited[v] = c;
+                exp[v].insert( exp[v].end(), expc[ce].begin(), expc[ce].end() );
+                Trace("sygus-cref-eval") << "   consider " << v << " -> " << c << std::endl;
+                break;
+              }
+            }
+          }
+        }
+        if( !cvars.empty() ){
+          lem = conj->getRefinementBaseLemma( i );
+        }
+      }else{
+        lem = conj->getRefinementBaseLemma( i );
+      }
+      if( !lem.isNull() ){
+        Trace("sygus-cref-eval") << "Check refinement lemma " << lem << " against current model." << std::endl;
+        Node elem = crefEvaluate( lem, vtm, visited, exp );
+        Trace("sygus-cref-eval") << "...evaluated to " << elem << ", exp size = " << exp[lem].size() << std::endl;
+        if( !elem.isNull() ){
+          bool success = false;
+          success = elem==d_quantEngine->getTermDatabase()->d_false;
+          if( success ){
+            elem = conj->getGuard().negate();
+            Node cre_lem;
+            if( !exp[lem].empty() ){
+              Node en = exp[lem].size()==1 ? exp[lem][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[lem] );
+              cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), elem );
+            }else{
+              cre_lem = elem;
+            }
+            if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
+              Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
+              lems.push_back( cre_lem );
+            }
+          }
+        }
+      }
+      // clean up caches
+      for( unsigned j=0; j<cvars.size(); j++ ){
+        visited.erase( cvars[j] );
+        exp.erase( cvars[j] );
+      }
+    }
+  }
+}
+
+Node CegInstantiation::crefEvaluate( Node n, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp ){
+  std::map< Node, Node >::iterator itv = visited.find( n );
+  if( itv!=visited.end() ){
+    return itv->second;
+  }else{
+    std::vector< Node > exp_c;
+    Node ret;
+    if( n.getKind()==kind::APPLY_UF ){
+      //it is an evaluation function
+      Trace("sygus-cref-eval-debug") << "Compute evaluation for : " << n << std::endl;
+      //unfold by one step 
+      Node nn = d_quantEngine->getTermDatabaseSygus()->unfold( n, vtm, exp[n] );
+      Trace("sygus-cref-eval-debug") << "...unfolded once to " << nn << std::endl;
+      Assert( nn!=n );
+      //it is the result of evaluating the unfolding
+      ret = crefEvaluate( nn, vtm, visited, exp );
+      //carry explanation
+      exp_c.push_back( nn );
+    }
+    if( ret.isNull() ){
+      if( n.getNumChildren()>0 ){
+        std::vector< Node > children;
+        bool childChanged = false;
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.push_back( n.getOperator() );
+        }
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          Node nc = crefEvaluate( n[i], vtm, visited, exp );
+          childChanged = nc!=n[i] || childChanged;
+          children.push_back( nc );
+          //Boolean short circuiting
+          if( n.getKind()==kind::AND ){
+            if( nc==d_quantEngine->getTermDatabase()->d_false ){
+              ret = nc;
+              exp_c.clear();
+            }
+          }else if( n.getKind()==kind::OR ){
+            if( nc==d_quantEngine->getTermDatabase()->d_true ){
+              ret = nc;
+              exp_c.clear();
+            }
+          }else if( n.getKind()==kind::ITE && i==0 ){
+            int index = -1;
+            if( nc==d_quantEngine->getTermDatabase()->d_true ){
+              index = 1;
+            }else if( nc==d_quantEngine->getTermDatabase()->d_false ){
+              index = 2;
+            }
+            if( index!=-1 ){
+              ret = crefEvaluate( n[index], vtm, visited, exp );
+              exp_c.push_back( n[index] );
+            }
+          }
+          //carry explanation
+          exp_c.push_back( n[i] );
+          if( !ret.isNull() ){
+            break;
+          }
+        }
+        if( ret.isNull() ){
+          if( childChanged ){
+            ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+            ret = Rewriter::rewrite( ret );
+          }else{
+            ret = n;
+          }
+        }
+      }else{
+        ret = n;
+      }
+    }
+    //carry explanation from children
+    for( unsigned i=0; i<exp_c.size(); i++ ){
+      Node nn = exp_c[i];
+      std::map< Node, std::vector< Node > >::iterator itx = exp.find( nn );
+      if( itx!=exp.end() ){
+        for( unsigned j=0; j<itx->second.size(); j++ ){
+          if( std::find( exp[n].begin(), exp[n].end(), itx->second[j] )==exp[n].end() ){
+            exp[n].push_back( itx->second[j] );
+          }
+        }
+      }
+    }
+    Trace("sygus-cref-eval-debug") << "... evaluation of " << n << " is (" << ret.getKind() << ") " << ret << std::endl;
+    Trace("sygus-cref-eval-debug") << "...... exp size = " << exp[n].size() << std::endl;
+    visited[n] = ret;
+    return ret;
+  }
+}
+
 void CegInstantiation::registerMeasuredType( TypeNode tn ) {
   std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
   if( it==d_uf_measure.end() ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index f49298411..2200baf55 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -51,6 +51,10 @@ private:
   /** refinement lemmas */
   std::vector< Node > d_refinement_lemmas;
   std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars;
+  std::vector< Node > d_refinement_lemmas_base;
+  std::vector< std::vector< Node > > d_refinement_lemmas_ceval;
+  std::vector< Node > d_refinement_lemmas_cprogress;
+  std::vector< std::vector< Node > > d_refinement_lemmas_cprogress_pts;
 private: //for condition solutions
   /** get candidate list recursively for conditional solutions */
   void getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd );
@@ -173,6 +177,18 @@ public:
   bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
   /** get model value */
   Node getModelValue( Node n );
+  /** get number of refinement lemmas */
+  unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
+  /** get refinement lemma */
+  Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
+  /** get refinement lemma */
+  Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+  /** get num conditional evaluations */
+  unsigned getNumConditionalEvaluations( unsigned i ) { return d_refinement_lemmas_ceval[i].size(); }
+  /** get conditional evaluation */
+  Node getConditionalEvaluation( unsigned i, unsigned j ) { return d_refinement_lemmas_ceval[i][j]; }
+  /** get progress lemma */
+  Node getConditionalProgressLemma( unsigned i ) { return d_refinement_lemmas_cprogress[i]; }
 };
 
 
@@ -199,6 +215,10 @@ private: //for enforcing fairness
   std::map< Node, std::map< int, Node > > d_size_term_lemma;
   /** get measure lemmas */
   void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
+private: //for direct evaluation
+  /** get refinement evaluation */
+  void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems );
+  Node crefEvaluate( Node lem, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp );
   /** get eager unfolding */
   Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
 private:
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b1cc9ed19..16fc4d4b8 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -45,7 +45,7 @@ struct sortQuantifierRelevance {
 
 FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
 TheoryModel( c, name, true ),
-d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
+d_qe( qe ), d_forall_asserts( c ){
   d_rlv_count = 0;
 }
 
@@ -70,34 +70,6 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
   }
 }
 
-//AJR : FIXME : this function is only used by bounded integers, can likely be removed.
-Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
-  std::vector< Node > children;
-  if( n.getNumChildren()>0 ){
-    if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( n.getOperator() );
-    }
-    for (unsigned i=0; i<n.getNumChildren(); i++) {
-      Node nc = getCurrentModelValue( n[i], partial );
-      if (nc.isNull()) {
-        return Node::null();
-      }else{
-        children.push_back( nc );
-      }
-    }
-    if( n.getKind()==APPLY_UF ){
-      return getCurrentUfModelValue( n, children, partial );
-    }else{
-      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      nn = Rewriter::rewrite( nn );
-      return nn;
-    }
-  }else{
-    //return getRepresentative(n);
-    return getValue(n);
-  }
-}
-
 void FirstOrderModel::initialize() {
   processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
@@ -613,6 +585,7 @@ void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
   }
 }
 
+/*
 Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
   std::vector< Node > children;
   children.push_back(n.getOperator());
@@ -627,7 +600,7 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar
     return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
   }
 }
-
+*/
 
 
 
@@ -659,6 +632,7 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
   }
 }
 
+/*
 Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
   Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
   for(unsigned i=0; i<args.size(); i++) {
@@ -667,6 +641,7 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a
   Assert( n.getKind()==APPLY_UF );
   return d_models[n.getOperator()]->evaluate(this, args);
 }
+*/
 
 void FirstOrderModelFmc::processInitialize( bool ispre ) {
   if( ispre ){
@@ -900,6 +875,7 @@ Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) {
   return Node::null();
 }
 
+/*
 Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
   Debug("qint-debug") << "get curr uf value " << n << std::endl;
   if( d_models_valid[n] ){
@@ -912,6 +888,7 @@ Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & a
     return Node::null();
   }
 }
+*/
 
 void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
   if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 7ded1b05d..05771d1a2 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -55,12 +55,10 @@ protected:
   std::vector< Node > d_forall_rlv_vec;
   Node d_last_forall_rlv;
   std::vector< Node > d_forall_rlv_assert;
-  /** is model set */
-  context::CDO< bool > d_isModelSet;
   /** get variable id */
   std::map< Node, std::map< Node, int > > d_quant_var_id;
-  /** get current model value */
-  virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
+  /** get current model value (deprecated) */
+  //virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0;
 public: //for Theory Quantifiers:
   /** assert quantifier */
   void assertQuantifier( Node n );
@@ -82,12 +80,6 @@ public:
   // initialize the model
   void initialize();
   virtual void processInitialize( bool ispre ) = 0;
-  /** mark model set */
-  void markModelSet() { d_isModelSet = true; }
-  /** is model set */
-  bool isModelSet() { return d_isModelSet; }
-  /** get current model value */
-  Node getCurrentModelValue( Node n, bool partial = false );
   /** get variable id */
   int getVariableId(TNode q, TNode n) {
     return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1;
@@ -133,8 +125,6 @@ private:
   //index ordering to use for each term
   std::map< Node, std::vector< int > > d_eval_term_index_order;
   void makeEvalUfIndexOrder( Node n );
-  /** get current model value */
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
 //the following functions are for evaluating quantifier bodies
 public:
   FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
@@ -179,7 +169,6 @@ private:
   Node intervalOp;
   Node getUsedRepresentative(Node n, bool strict = false);
   /** get current model value */
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
   void processInitializeModelForTerm(Node n);
 public:
   FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
@@ -214,7 +203,6 @@ public:
   std::map< Node, std::map< int, int > > d_var_index;
 private:
   /** get current model value */
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
   void processInitializeModelForTerm(Node n);
   void processInitializeQuantifier( Node q );
   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 7e528fef3..ac23dae29 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -257,7 +257,9 @@ void Def::basic_simplify( FirstOrderModelFmc * m ) {
 }
 
 void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
+  Trace("fmc-simplify") << "Simplify definition, #cond = " << d_cond.size() << std::endl;
   basic_simplify( m );
+  Trace("fmc-simplify") << "post-basic simplify, #cond = " << d_cond.size() << std::endl;
 
   //check if the last entry is not all star, if so, we can make the last entry all stars
   if( !d_cond.empty() ){
@@ -300,6 +302,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
       Trace("fmc-cover-simplify") << std::endl;
     }
   }
+  Trace("fmc-simplify") << "finish simplify, #cond = " << d_cond.size() << std::endl;
 }
 
 void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
@@ -325,94 +328,96 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   //standard pre-process
-  preProcessBuildModelStd( m, fullModel );
+  if( !preProcessBuildModelStd( m ) ){
+    return false;
+  }
   
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
-  if( !fullModel ){
-    Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
-    d_preinitialized_types.clear();
-    //traverse equality engine
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
-    while( !eqcs_i.isFinished() ){
-      TypeNode tr = (*eqcs_i).getType();
-      d_preinitialized_types[tr] = true;
-      ++eqcs_i;
-    }
+  Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+  d_preinitialized_types.clear();
+  //traverse equality engine
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    TypeNode tr = (*eqcs_i).getType();
+    d_preinitialized_types[tr] = true;
+    ++eqcs_i;
+  }
 
-    //must ensure model basis terms exists in model for each relevant type
-    fm->initialize();
-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      Node op = it->first;
-      TypeNode tno = op.getType();
-      for( unsigned i=0; i<tno.getNumChildren(); i++) {
-        preInitializeType( fm, tno[i] );
-      }
+  //must ensure model basis terms exists in model for each relevant type
+  fm->initialize();
+  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+    Node op = it->first;
+    TypeNode tno = op.getType();
+    for( unsigned i=0; i<tno.getNumChildren(); i++) {
+      preInitializeType( fm, tno[i] );
     }
-    //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
-    if( !options::fmfEmptySorts() ){
-      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node q = fm->getAssertedQuantifier( i );
-        //make sure all types are set
-        for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-          preInitializeType( fm, q[0][j].getType() );
-        }
+  }
+  //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
+  if( !options::fmfEmptySorts() ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i );
+      //make sure all types are set
+      for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+        preInitializeType( fm, q[0][j].getType() );
       }
     }
   }
+  return true;
 }
 
-void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+bool FullModelChecker::processBuildModel(TheoryModel* m){
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
-  if( !fullModel ){
-    Trace("fmc") << "---Full Model Check reset() " << std::endl;
-    d_quant_models.clear();
-    d_rep_ids.clear();
-    d_star_insts.clear();
-    //process representatives
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        for( size_t a=0; a<it->second.size(); a++ ){
-          Node r = fm->getUsedRepresentative( it->second[a] );
-          if( Trace.isOn("fmc-model-debug") ){
-            std::vector< Node > eqc;
-            ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
-            Trace("fmc-model-debug") << "   " << (it->second[a]==r);
-            Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
-            //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
-            Trace("fmc-model-debug") << " {";
-            for( size_t i=0; i<eqc.size(); i++ ){
-              Trace("fmc-model-debug") << eqc[i] << ", ";
-            }
-            Trace("fmc-model-debug") << "}" << std::endl;
+  Trace("fmc") << "---Full Model Check reset() " << std::endl;
+  d_quant_models.clear();
+  d_rep_ids.clear();
+  d_star_insts.clear();
+  //process representatives
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      for( size_t a=0; a<it->second.size(); a++ ){
+        Node r = fm->getUsedRepresentative( it->second[a] );
+        if( Trace.isOn("fmc-model-debug") ){
+          std::vector< Node > eqc;
+          ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+          Trace("fmc-model-debug") << "   " << (it->second[a]==r);
+          Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+          Trace("fmc-model-debug") << " {";
+          for( size_t i=0; i<eqc.size(); i++ ){
+            Trace("fmc-model-debug") << eqc[i] << ", ";
           }
-          d_rep_ids[it->first][r] = (int)a;
+          Trace("fmc-model-debug") << "}" << std::endl;
         }
-        Trace("fmc-model-debug") << std::endl;
+        d_rep_ids[it->first][r] = (int)a;
       }
+      Trace("fmc-model-debug") << std::endl;
     }
+  }
 
-    //now, make models
-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
-      Node op = it->first;
-      //reset the model
-      fm->d_models[op]->reset();
-
-      Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
-      std::vector< Node > add_conds;
-      std::vector< Node > add_values;
-      bool needsDefault = true;
-      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-        Node n = fm->d_uf_terms[op][i];
+  //now, make models
+  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+    Node op = it->first;
+    //reset the model
+    fm->d_models[op]->reset();
+
+    std::vector< Node > add_conds;
+    std::vector< Node > add_values;      
+    bool needsDefault = true;
+    std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
+    if( itut!=fm->d_uf_terms.end() ){
+      Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = itut->second[i];
         if( d_qe->getTermDatabase()->isTermActive( n ) ){
           add_conds.push_back( n );
           add_values.push_back( n );
           Node r = fm->getUsedRepresentative(n);
           Trace("fmc-model-debug") << n << " -> " << r << std::endl;
-          //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) );
+          //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
         }else{
           if( Trace.isOn("fmc-model-debug") ){
             Node r = fm->getUsedRepresentative(n);
@@ -420,127 +425,126 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           }
         }
       }
-      Trace("fmc-model-debug") << std::endl;
-      //possibly get default
-      if( needsDefault ){
-        Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
-        //add default value if necessary
-        if( fm->hasTerm( nmb ) ){
-          Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
-          add_conds.push_back( nmb );
-          add_values.push_back( nmb );
-        }else{
-          Node vmb = getSomeDomainElement(fm, nmb.getType());
-          Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
-          Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
-          add_conds.push_back( nmb );
-          add_values.push_back( vmb );
-        }
+    }else{
+      Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
+    }
+    Trace("fmc-model-debug") << std::endl;
+    //possibly get default
+    if( needsDefault ){
+      Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+      //add default value if necessary
+      if( fm->hasTerm( nmb ) ){
+        Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+        add_conds.push_back( nmb );
+        add_values.push_back( nmb );
+      }else{
+        Node vmb = getSomeDomainElement(fm, nmb.getType());
+        Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+        Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+        add_conds.push_back( nmb );
+        add_values.push_back( vmb );
       }
+    }
 
-      std::vector< Node > conds;
-      std::vector< Node > values;
-      std::vector< Node > entry_conds;
-      //get the entries for the mdoel
-      for( size_t i=0; i<add_conds.size(); i++ ){
-        Node c = add_conds[i];
-        Node v = add_values[i];
-        std::vector< Node > children;
-        std::vector< Node > entry_children;
-        children.push_back(op);
-        entry_children.push_back(op);
-        bool hasNonStar = false;
-        for( unsigned i=0; i<c.getNumChildren(); i++) {
-          Node ri = fm->getUsedRepresentative( c[i] );
-          children.push_back(ri);
-          bool isStar = false;
-          if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
-            if (fm->isModelBasisTerm(ri) ) {
-              ri = fm->getStar( ri.getType() );
-              isStar = true;
-            }else{
-              hasNonStar = true;
-            }
-          }
-          if( !isStar && !ri.isConst() ){
-            Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
-            Assert( false );
+    std::vector< Node > conds;
+    std::vector< Node > values;
+    std::vector< Node > entry_conds;
+    //get the entries for the mdoel
+    for( size_t i=0; i<add_conds.size(); i++ ){
+      Node c = add_conds[i];
+      Node v = add_values[i];
+      std::vector< Node > children;
+      std::vector< Node > entry_children;
+      children.push_back(op);
+      entry_children.push_back(op);
+      bool hasNonStar = false;
+      for( unsigned i=0; i<c.getNumChildren(); i++) {
+        Node ri = fm->getUsedRepresentative( c[i] );
+        children.push_back(ri);
+        bool isStar = false;
+        if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
+          if (fm->isModelBasisTerm(ri) ) {
+            ri = fm->getStar( ri.getType() );
+            isStar = true;
+          }else{
+            hasNonStar = true;
           }
-          entry_children.push_back(ri);
         }
-        Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-        Node nv = fm->getUsedRepresentative( v );
-        if( !nv.isConst() ){
-          Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+        if( !isStar && !ri.isConst() ){
+          Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
           Assert( false );
         }
-        Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
-        if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
-          Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
-          conds.push_back(n);
-          values.push_back(nv);
-          entry_conds.push_back(en);
-        }
-        else {
-          Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
-        }
+        entry_children.push_back(ri);
+      }
+      Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+      Node nv = fm->getUsedRepresentative( v );
+      if( !nv.isConst() ){
+        Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+        Assert( false );
+      }
+      Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+      if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+        Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+        conds.push_back(n);
+        values.push_back(nv);
+        entry_conds.push_back(en);
       }
+      else {
+        Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+      }
+    }
 
 
-      //sort based on # default arguments
-      std::vector< int > indices;
-      ModelBasisArgSort mbas;
-      for (int i=0; i<(int)conds.size(); i++) {
-        d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
-        mbas.d_terms.push_back(conds[i]);
-        indices.push_back(i);
-      }
-      std::sort( indices.begin(), indices.end(), mbas );
+    //sort based on # default arguments
+    std::vector< int > indices;
+    ModelBasisArgSort mbas;
+    for (int i=0; i<(int)conds.size(); i++) {
+      d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+      mbas.d_terms.push_back(conds[i]);
+      indices.push_back(i);
+    }
+    std::sort( indices.begin(), indices.end(), mbas );
 
-      for (int i=0; i<(int)indices.size(); i++) {
-        fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
-      }
+    for (int i=0; i<(int)indices.size(); i++) {
+      fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+    }
 
 
-      if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
-        convertIntervalModel( fm, op );
-      }
+    if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
+      convertIntervalModel( fm, op );
+    }
 
-      Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
-      fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
-      Trace("fmc-model-simplify") << std::endl;
+    Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+    fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+    Trace("fmc-model-simplify") << std::endl;
 
-      Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
-      fm->d_models[op]->simplify( this, fm );
+    Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
+    fm->d_models[op]->simplify( this, fm );
 
-      fm->d_models[op]->debugPrint("fmc-model", op, this);
-      Trace("fmc-model") << std::endl;
+    fm->d_models[op]->debugPrint("fmc-model", op, this);
+    Trace("fmc-model") << std::endl;
 
-      //for debugging
-      /*
-      for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
-        std::vector< Node > inst;
-        for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
-          Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
-          inst.push_back( r );
-        }
-        Node ev = fm->d_models[op]->evaluate( fm, inst );
-        Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
-        AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
+    //for debugging
+    /*
+    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+      std::vector< Node > inst;
+      for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
+        Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
+        inst.push_back( r );
       }
-      */
-    }
-  }else{
-    //make function values
-    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
-      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+      Node ev = fm->d_models[op]->evaluate( fm, inst );
+      Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
+      AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
     }
-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
-    //mark that the model has been set
-    fm->markModelSet();
-    //debug the model
-    debugModel( fm );
+    */
+  }
+  Assert( d_addedLemmas==0 );
+  
+  //make function values
+  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
+    m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
   }
+  return TheoryEngineModelBuilder::processBuildModel( m );
 }
 
 void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
@@ -617,6 +621,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         //model check the quantifier
         doCheck(fmfmc, f, d_quant_models[f], f[1]);
         Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
+        Assert( !d_quant_models[f].d_cond.empty() );
         d_quant_models[f].debugPrint("fmc", Node::null(), this);
         Trace("fmc") << std::endl;
 
@@ -890,7 +895,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       */
     } else {
       if( !var_ch.empty() ){
-        if( n.getKind()==EQUAL ){
+        if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
           if( var_ch.size()==2 ){
             Trace("fmc-debug") << "Do variable equality " << n << std::endl;
             doVariableEquality( fm, f, d, n );
@@ -1273,7 +1278,7 @@ Node FullModelChecker::mkArrayCond( Node a ) {
 }
 
 Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
-  if( n.getKind()==EQUAL ){
+  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
     if (!vals[0].isNull() && !vals[1].isNull()) {
       return vals[0]==vals[1] ? d_true : d_false;
     }else{
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 7d21b4185..3e7c9918e 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -144,10 +144,8 @@ public:
   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
 
   /** process build model */  
-  void preProcessBuildModel(TheoryModel* m, bool fullModel); 
-  void processBuildModel(TheoryModel* m, bool fullModel);
-  /** get current model value */
-  Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
+  bool preProcessBuildModel(TheoryModel* m); 
+  bool processBuildModel(TheoryModel* m);
 
   bool useSimpleModels();
 };/* class FullModelChecker */
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 41099552d..28b92cc5e 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -367,7 +367,7 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
   }else{
     Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
     if( ak==EQUAL ){
-      Node atom = n.getKind() ? n[0] : n;
+      Node atom = n.getKind()==NOT ? n[0] : n;
       return !atom[0].getType().isBoolean();
     }else{
       Assert( ak!=NOT );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index f2ed81d8c..a197e057e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -670,6 +670,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
       }else{
         Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
       }
+      Assert( rd!=NULL );
       rd->compute();
       unsigned final_max_i = 0;
       std::vector< unsigned > maxs;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 090f2735a..7f342c633 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -35,7 +35,7 @@ using namespace CVC4::theory::quantifiers;
 
 
 QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
+TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_qe( qe ){
 
 }
 
@@ -43,46 +43,46 @@ bool QModelBuilder::optUseModel() {
   return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
 }
 
-void QModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
-  preProcessBuildModelStd( m, fullModel );
+bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
+  return preProcessBuildModelStd( m );
 }
 
-void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) {
-  if( !fullModel ){
-    if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
-      FirstOrderModel * fm = (FirstOrderModel*)m;
-      //traverse equality engine
-      std::map< TypeNode, bool > eqc_usort;
-      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
-      while( !eqcs_i.isFinished() ){
-        TypeNode tr = (*eqcs_i).getType();
-        eqc_usort[tr] = true;
-        ++eqcs_i;
-      }
-      //look at quantified formulas
-      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node q = fm->getAssertedQuantifier( i, true );
-        if( fm->isQuantifierActive( q ) ){
-          //check if any of these quantified formulas can be set inactive
-          if( options::fmfEmptySorts() ){
-            for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-              TypeNode tn = q[0][i].getType();
-              //we are allowed to assume the type is empty
-              if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
-                Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
-                fm->setQuantifierActive( q, false );
-              }
+bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
+  d_addedLemmas = 0;
+  d_triedLemmas = 0;
+  if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
+    FirstOrderModel * fm = (FirstOrderModel*)m;
+    //traverse equality engine
+    std::map< TypeNode, bool > eqc_usort;
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+    while( !eqcs_i.isFinished() ){
+      TypeNode tr = (*eqcs_i).getType();
+      eqc_usort[tr] = true;
+      ++eqcs_i;
+    }
+    //look at quantified formulas
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i, true );
+      if( fm->isQuantifierActive( q ) ){
+        //check if any of these quantified formulas can be set inactive
+        if( options::fmfEmptySorts() ){
+          for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+            TypeNode tn = q[0][i].getType();
+            //we are allowed to assume the type is empty
+            if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
+              Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
+              fm->setQuantifierActive( q, false );
             }
-          }else if( options::fmfFunWellDefinedRelevant() ){
-            if( q[0].getNumChildren()==1 ){
-              TypeNode tn = q[0][0].getType();
-              if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
-                //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
-                //we are allowed to assume the introduced type is empty
-                if( eqc_usort.find( tn )==eqc_usort.end() ){
-                  Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
-                  fm->setQuantifierActive( q, false );
-                }
+          }
+        }else if( options::fmfFunWellDefinedRelevant() ){
+          if( q[0].getNumChildren()==1 ){
+            TypeNode tn = q[0][0].getType();
+            if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
+              //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
+              //we are allowed to assume the introduced type is empty
+              if( eqc_usort.find( tn )==eqc_usort.end() ){
+                Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
+                fm->setQuantifierActive( q, false );
               }
             }
           }
@@ -90,11 +90,13 @@ void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) {
       }
     }
   }
+  return true;
 }
 
-void QModelBuilder::debugModel( FirstOrderModel* fm ){
+void QModelBuilder::debugModel( TheoryModel* m ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
   if( Trace.isOn("quant-check-model") ){
+    FirstOrderModel* fm = (FirstOrderModel*)m;
     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
@@ -164,122 +166,119 @@ QModelBuilder( c, qe ), d_basisNoMatch( c ) {
 
 }
 
+/*
 Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
   return n;
 }
+*/
 
-void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
+bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
-  Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl;
-  if( fullModel ){
-    Assert( d_curr_model==fm );
-    //update models
-    for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-      it->second.update( fm );
-      Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
-      //construct function values
-      fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+  Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
+  d_didInstGen = false;
+  //reset the internal information
+  reset( fm );
+  //only construct first order model if optUseModel() is true
+  if( optUseModel() ){
+    Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
+    //check if any quantifiers are un-initialized
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i );
+      if( d_qe->getModel()->isQuantifierActive( q ) ){
+        int lems = initializeQuantifier( q, q );
+        d_statistics.d_init_inst_gen_lemmas += lems;
+        d_addedLemmas += lems;
+        if( d_qe->inConflict() ){
+          break;
+        }
+      }
     }
-    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
-    //mark that the model has been set
-    fm->markModelSet();
-    //debug the model
-    debugModel( fm );
-  }else{
-    d_curr_model = fm;
-    d_didInstGen = false;
-    //reset the internal information
-    reset( fm );
-    //only construct first order model if optUseModel() is true
-    if( optUseModel() ){
-      Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
-      //check if any quantifiers are un-initialized
+    if( d_addedLemmas>0 ){
+      Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
+      return false;
+    }else{
+      Assert( !d_qe->inConflict() );
+      //initialize model
+      fm->initialize();
+      //analyze the functions
+      Trace("model-engine-debug") << "Analyzing model..." << std::endl;
+      analyzeModel( fm );
+      //analyze the quantifiers
+      Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
+      d_uf_prefs.clear();
       for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node q = fm->getAssertedQuantifier( i );
-        if( d_qe->getModel()->isQuantifierActive( q ) ){
-          int lems = initializeQuantifier( q, q );
-          d_statistics.d_init_inst_gen_lemmas += lems;
-          d_addedLemmas += lems;
-          if( d_qe->inConflict() ){
-            break;
-          }
-        }
+        analyzeQuantifier( fm, q );
       }
-      if( d_addedLemmas>0 ){
-        Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
-      }else{
-        Assert( !d_qe->inConflict() );
-        //initialize model
-        fm->initialize();
-        //analyze the functions
-        Trace("model-engine-debug") << "Analyzing model..." << std::endl;
-        analyzeModel( fm );
-        //analyze the quantifiers
-        Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
-        d_uf_prefs.clear();
-        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-          Node q = fm->getAssertedQuantifier( i );
-          analyzeQuantifier( fm, q );
-        }
 
-        //if applicable, find exceptions to model via inst-gen
-        if( options::fmfInstGen() ){
-          d_didInstGen = true;
-          d_instGenMatches = 0;
-          d_numQuantSat = 0;
-          d_numQuantInstGen = 0;
-          d_numQuantNoInstGen = 0;
-          d_numQuantNoSelForm = 0;
-          //now, see if we know that any exceptions via InstGen exist
-          Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
-          for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-            Node f = fm->getAssertedQuantifier( i );
-            if( d_qe->getModel()->isQuantifierActive( f ) ){
-              int lems = doInstGen( fm, f );
-              d_statistics.d_inst_gen_lemmas += lems;
-              d_addedLemmas += lems;
-              //temporary
-              if( lems>0 ){
-                d_numQuantInstGen++;
-              }else if( hasInstGen( f ) ){
-                d_numQuantNoInstGen++;
-              }else{
-                d_numQuantNoSelForm++;
-              }
-              if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
-                break;
-              }
+      //if applicable, find exceptions to model via inst-gen
+      if( options::fmfInstGen() ){
+        d_didInstGen = true;
+        d_instGenMatches = 0;
+        d_numQuantSat = 0;
+        d_numQuantInstGen = 0;
+        d_numQuantNoInstGen = 0;
+        d_numQuantNoSelForm = 0;
+        //now, see if we know that any exceptions via InstGen exist
+        Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+          Node f = fm->getAssertedQuantifier( i );
+          if( d_qe->getModel()->isQuantifierActive( f ) ){
+            int lems = doInstGen( fm, f );
+            d_statistics.d_inst_gen_lemmas += lems;
+            d_addedLemmas += lems;
+            //temporary
+            if( lems>0 ){
+              d_numQuantInstGen++;
+            }else if( hasInstGen( f ) ){
+              d_numQuantNoInstGen++;
             }else{
-              d_numQuantSat++;
+              d_numQuantNoSelForm++;
             }
-          }
-          Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
-          Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
-          Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
-          if( Trace.isOn("model-engine") ){
-            if( d_addedLemmas>0 ){
-              Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
-            }else{
-              Trace("model-engine") << "No InstGen lemmas..." << std::endl;
+            if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
+              break;
             }
+          }else{
+            d_numQuantSat++;
           }
         }
-        //construct the model if necessary
-        if( d_addedLemmas==0 ){
-          //if no immediate exceptions, build the model
-          //  this model will be an approximation that will need to be tested via exhaustive instantiation
-          Trace("model-engine-debug") << "Building model..." << std::endl;
-          //build model for UF
-          for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-            Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
-            constructModelUf( fm, it->first );
+        Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
+        Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
+        Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
+        if( Trace.isOn("model-engine") ){
+          if( d_addedLemmas>0 ){
+            Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+          }else{
+            Trace("model-engine") << "No InstGen lemmas..." << std::endl;
           }
-          Trace("model-engine-debug") << "Done building models." << std::endl;
         }
       }
+      //construct the model if necessary
+      if( d_addedLemmas==0 ){
+        //if no immediate exceptions, build the model
+        //  this model will be an approximation that will need to be tested via exhaustive instantiation
+        Trace("model-engine-debug") << "Building model..." << std::endl;
+        //build model for UF
+        for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+          Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
+          constructModelUf( fm, it->first );
+        }
+        Trace("model-engine-debug") << "Done building models." << std::endl;
+      }else{
+        return false;
+      }
     }
   }
+  //update models
+  for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+    it->second.update( fm );
+    Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
+    //construct function values
+    fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+  }
+  Assert( d_addedLemmas==0 );
+  return TheoryEngineModelBuilder::processBuildModel( m );
 }
 
 int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
@@ -330,24 +329,27 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
   for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
     Node op = it->first;
     TermArgBasisTrie tabt;
-    for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
-      Node n = fmig->d_uf_terms[op][i];
-      //for calculating if op is constant
-      if( d_qe->getTermDatabase()->isTermActive( n ) ){
-        Node v = fmig->getRepresentative( n );
-        if( i==0 ){
-          d_uf_prefs[op].d_const_val = v;
-        }else if( v!=d_uf_prefs[op].d_const_val ){
-          d_uf_prefs[op].d_const_val = Node::null();
-          break;
+    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+    if( itut!=fmig->d_uf_terms.end() ){
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = fmig->d_uf_terms[op][i];
+        //for calculating if op is constant
+        if( d_qe->getTermDatabase()->isTermActive( n ) ){
+          Node v = fmig->getRepresentative( n );
+          if( i==0 ){
+            d_uf_prefs[op].d_const_val = v;
+          }else if( v!=d_uf_prefs[op].d_const_val ){
+            d_uf_prefs[op].d_const_val = Node::null();
+            break;
+          }
         }
-      }
-      //for calculating terms that we don't need to consider
-      if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
-        if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
-          //need to consider if it is not congruent modulo model basis
-          if( !tabt.addTerm( fmig, n ) ){
-            d_basisNoMatch[n] = true;
+        //for calculating terms that we don't need to consider
+        if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+          if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
+            //need to consider if it is not congruent modulo model basis
+            if( !tabt.addTerm( fmig, n ) ){
+              d_basisNoMatch[n] = true;
+            }
           }
         }
       }
@@ -733,31 +735,34 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
     Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
     Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
     //set the values in the model
-    for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){
-      Node n = fmig->d_uf_terms[op][i];
-      if( isTermActive( n ) ){
-        Node v = fmig->getRepresentative( n );
-        Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
-        //if this assertion did not help the model, just consider it ground
-        //set n = v in the model tree
-        //set it as ground value
-        fmig->d_uf_model_gen[op].setValue( fm, n, v );
-        if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
-          //also set as default value if necessary
-          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
-            Trace("fmf-model-cons") << "  Set as default." << std::endl;
-            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+    std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
+    if( itut!=fmig->d_uf_terms.end() ){
+      for( size_t i=0; i<itut->second.size(); i++ ){
+        Node n = itut->second[i];
+        if( isTermActive( n ) ){
+          Node v = fmig->getRepresentative( n );
+          Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+          //if this assertion did not help the model, just consider it ground
+          //set n = v in the model tree
+          //set it as ground value
+          fmig->d_uf_model_gen[op].setValue( fm, n, v );
+          if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
+            //also set as default value if necessary
+            if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
+              Trace("fmf-model-cons") << "  Set as default." << std::endl;
+              fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+              if( n==defaultTerm ){
+                //incidentally already set, we will not need to find a default value
+                setDefaultVal = false;
+              }
+            }
+          }else{
             if( n==defaultTerm ){
+              fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
               //incidentally already set, we will not need to find a default value
               setDefaultVal = false;
             }
           }
-        }else{
-          if( n==defaultTerm ){
-            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
-            //incidentally already set, we will not need to find a default value
-            setDefaultVal = false;
-          }
         }
       }
     }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index e1f586585..eedd850d6 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -29,12 +29,13 @@ namespace quantifiers {
 class QModelBuilder : public TheoryEngineModelBuilder
 {
 protected:
-  //the model we are working with
-  context::CDO< FirstOrderModel* > d_curr_model;
   //quantifiers engine
   QuantifiersEngine* d_qe;
-  void preProcessBuildModel(TheoryModel* m, bool fullModel);
-  void preProcessBuildModelStd(TheoryModel* m, bool fullModel);
+  bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
+  bool preProcessBuildModelStd(TheoryModel* m);
+  /** number of lemmas generated while building model */
+  unsigned d_addedLemmas;
+  unsigned d_triedLemmas;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilder() throw() {}
@@ -45,13 +46,13 @@ public:
   virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
-  /** number of lemmas generated while building model */
-  int d_addedLemmas;
-  int d_triedLemmas;
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
   //debug model
-  void debugModel( FirstOrderModel* fm );
+  virtual void debugModel( TheoryModel* m );
+  //statistics 
+  unsigned getNumAddedLemmas() { return d_addedLemmas; }
+  unsigned getNumTriedLemmas() { return d_triedLemmas; }
 };
 
 
@@ -87,9 +88,7 @@ protected:
   //whether inst gen was done
   bool d_didInstGen;
   /** process build model */
-  virtual void processBuildModel( TheoryModel* m, bool fullModel );
-  /** get current model value */
-  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
+  virtual bool processBuildModel( TheoryModel* m );
 protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 9496f630d..f529a9a27 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -237,8 +237,8 @@ int ModelEngine::checkModel(){
 void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   //first check if the builder can do the exhaustive instantiation
   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
-  mb->d_triedLemmas = 0;
-  mb->d_addedLemmas = 0;
+  unsigned prev_alem = mb->getNumAddedLemmas();
+  unsigned prev_tlem = mb->getNumTriedLemmas();
   int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
   if( retEi!=0 ){
     if( retEi<0 ){
@@ -247,9 +247,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }else{
       Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
     }
-    d_triedLemmas += mb->d_triedLemmas;
-    d_addedLemmas += mb->d_addedLemmas;
-    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas;
+    d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
+    d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
+    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas();
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 8166925c6..f7bac23e2 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -69,7 +69,7 @@ void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) {
 
 
 
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){
+RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){
    d_is_computed = false;
 }
 
@@ -105,8 +105,9 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_model->getAssertedQuantifier( i );
+    FirstOrderModel* fm = d_qe->getModel();
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node q = fm->getAssertedQuantifier( i );
       Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
       computeRelevantDomain( q, icf, true, true );
@@ -171,7 +172,7 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
     }
   }
 
-  if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
+  if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
     //compute the information for what this literal does
     computeRelevantDomainLit( q, hasPol, pol, n );
     if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 1d6a2af19..be6ebcd9d 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -43,7 +43,6 @@ private:
   std::map< RDomain *, Node > d_rn_map;
   std::map< RDomain *, int > d_ri_map;
   QuantifiersEngine* d_qe;
-  FirstOrderModel* d_model;
   void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol );
   void computeRelevantDomainOpCh( RDomain * rf, Node n );
   bool d_is_computed;
@@ -63,7 +62,7 @@ private:
   std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit;
   void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n );
 public:
-  RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
+  RelevantDomain( QuantifiersEngine* qe );
   virtual ~RelevantDomain();
   /* reset */
   bool reset( Theory::Effort e );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d394c8fef..fb123f5b0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -3274,7 +3274,7 @@ void TermDbSygus::registerEvalTerm( Node n ) {
   }
 }
 
-void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) {
+void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms, std::vector< Node >& vals, std::vector< Node >& exps ) {
   std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
   if( its!=d_subterms.end() ){
     Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
@@ -3288,7 +3288,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
         Node vn = n.substitute( at, vt );
         vn = Rewriter::rewrite( vn );
         unsigned start = d_node_mv_args_proc[n][vn];
-        Node antec = n.eqNode( vn ).negate();
+        Node antec = n.eqNode( vn );
         TypeNode tn = n.getType();
         Assert( tn.isDatatype() );
         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
@@ -3306,10 +3306,16 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
         for( unsigned i=start; i<it->second.size(); i++ ){
           Assert( vars.size()==it->second[i].size() );
           Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
-          Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); 
-          lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
-          Trace("sygus-eager") << "Lemma : " << lem << std::endl;
-          lems.push_back( lem );
+          sBTerm = Rewriter::rewrite( sBTerm );
+          //Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); 
+          //lem = NodeManager::currentNM()->mkNode( OR, antec.negate(), lem );
+          terms.push_back( d_evals[n][i] );
+          vals.push_back( sBTerm );
+          exps.push_back( antec );
+          Trace("sygus-eager") << "Conclude : " << d_evals[n][i] << " == " << sBTerm << std::endl;
+          Trace("sygus-eager") << "   from " << antec << std::endl;
+          //Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+          //lems.push_back( lem );
         }
         d_node_mv_args_proc[n][vn] = it->second.size();
       }
@@ -3317,6 +3323,66 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
   }
 }
 
+
+Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp ) {
+  if( en.getKind()==kind::APPLY_UF ){
+    std::map< Node, Node >::iterator itv = vtm.find( en[0] );
+    if( itv!=vtm.end() ){
+      Node ev = itv->second;
+      Assert( en[0].getType()==ev.getType() );
+      Assert( ev.isConst() && ev.getKind()==kind::APPLY_CONSTRUCTOR );
+      std::vector< Node > args;
+      for( unsigned i=1; i<en.getNumChildren(); i++ ){
+        args.push_back( en[i] );
+      }
+      const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype();
+      unsigned i = Datatype::indexOf( ev.getOperator().toExpr() );
+      //explanation
+      Node ee = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), en[0] );
+      if( std::find( exp.begin(), exp.end(), ee )==exp.end() ){
+        exp.push_back( ee );
+      }
+      std::map< int, Node > pre;
+      for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+        std::vector< Node > cc;
+        //get the evaluation argument for the selector
+        const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype();
+        cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) );
+        Node s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][j].getSelector() ), en[0] );
+        cc.push_back( s );
+        //update vtm map
+        vtm[s] = ev[j];
+        cc.insert( cc.end(), args.begin(), args.end() );
+        pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
+      }
+      std::map< TypeNode, int > var_count; 
+      Node ret = mkGeneric( dt, i, var_count, pre );
+      // if it is a variable, apply the substitution
+      if( ret.getKind()==kind::BOUND_VARIABLE ){
+        //replace by argument
+        Node var_list = Node::fromExpr( dt.getSygusVarList() );
+        //TODO : set argument # on sygus variables
+        for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+          if( var_list[j]==ret ){
+            ret = args[j];
+            break;
+          }
+        }
+        Assert( ret.isConst() );
+      }else if( ret.getKind()==APPLY ){
+        //must expand definitions to account for defined functions in sygus grammars
+        ret = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( ret.toExpr() ) );
+      }
+      return ret;
+    }else{
+      Assert( false );
+    }
+  }else{
+    Assert( en.isConst() );
+  }
+  return en;
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9f43c1d35..fa27f0160 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -672,7 +672,8 @@ private:
   std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
 public:
   void registerEvalTerm( Node n );
-  void registerModelValue( Node n, Node v, std::vector< Node >& lems );
+  void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals );
+  Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp );
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ba50f9ead..bdf2de7f7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -97,16 +97,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
-  //the model object
-  if( options::mbqiMode()==quantifiers::MBQI_FMC ||
-      options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() ||
-      options::mbqiMode()==quantifiers::MBQI_TRUST ){
-    d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
-  }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
-    d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
-  }else{
-    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
-  }
   if( options::relevantTriggers() ){
     d_quant_rel = new QuantRelevance( false );
   }else{
@@ -127,6 +117,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_i_cbqi = NULL;
   d_qsplit = NULL;
   d_anti_skolem = NULL;
+  d_model = NULL;
   d_model_engine = NULL;
   d_bint = NULL;
   d_rr_engine = NULL;
@@ -224,14 +215,14 @@ void QuantifiersEngine::finishInit(){
   if( options::cbqi() ){
     d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
     d_modules.push_back( d_i_cbqi );
-    if( options::cbqiModel() ){
-      needsBuilder = true;
-    }
+    //if( options::cbqiModel() ){
+    //  needsBuilder = true;
+    //}
   }
   if( options::ceGuidedInst() ){
     d_ceg_inst = new quantifiers::CegInstantiation( this, c );
     d_modules.push_back( d_ceg_inst );
-    needsBuilder = true;
+    //needsBuilder = true;
   }  
   //finite model finding
   if( options::finiteModelFind() ){
@@ -241,6 +232,7 @@ void QuantifiersEngine::finishInit(){
     }
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
+    //finite model finder has special ways of building the model
     needsBuilder = true;
   }
   if( options::quantRewriteRules() ){
@@ -276,27 +268,32 @@ void QuantifiersEngine::finishInit(){
     d_modules.push_back( d_fs );
     needsRelDom = true;
   }
- 
+  
   if( needsRelDom ){
-    d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+    d_rel_dom = new quantifiers::RelevantDomain( this );
     d_util.push_back( d_rel_dom );
   }
-
+  
+  // if we require specialized ways of building the model
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
         options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
+      d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
+      d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
       d_builder = new quantifiers::AbsMbqiBuilder( c, this );
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
+      d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
       d_builder = new quantifiers::QModelBuilderDefault( c, this );
     }
+  }else{
+    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
-
 }
 
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
@@ -405,7 +402,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   d_conflict = false;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
-  bool usedModelBuilder = false;
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
@@ -505,14 +501,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
       d_curr_effort_level = quant_e;
       bool success = true;
       //build the model if any module requested it
-      if( needsModelE==quant_e ){
-        Assert( d_builder!=NULL );
+      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;
-        usedModelBuilder = true;
-        d_builder->d_addedLemmas = 0;
-        d_builder->buildModel( d_model, false );
-        //we are done if model building was unsuccessful
-        if( d_builder->d_addedLemmas>0 ){
+        if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+          //we are done if model building was unsuccessful
+          Trace("quant-engine-debug") << "...failed." << std::endl;
           success = false;
         }
       }
@@ -625,13 +620,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
     if( options::produceModels() ){
-      if( usedModelBuilder ){
-        Trace("quant-engine-debug") << "Build completed model..." << std::endl;
-        d_builder->buildModel( d_model, true );
-      }else if( !d_model->isModelSet() ){
+      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 model..." << std::endl;
-        d_te->getModelBuilder()->buildModel( d_model, true );
+        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;
       }
     }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 58f3e4f74..8014a8f22 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -212,16 +212,9 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
 void TheoryEngine::finishInit() {
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
-
-  //initialize the model
+  
+  //initialize the quantifiers engine, master equality engine, model, model builder
   if( d_logicInfo.isQuantified() ) {
-    d_curr_model = d_quantEngine->getModel();
-  } else {
-    d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
-    d_aloc_curr_model = true;
-  }
-
-  if (d_logicInfo.isQuantified()) {
     d_quantEngine->finishInit();
     Assert(d_masterEqualityEngine == 0);
     d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
@@ -232,6 +225,17 @@ void TheoryEngine::finishInit() {
         d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
       }
     }
+  
+    d_curr_model_builder = d_quantEngine->getModelBuilder();
+    d_curr_model = d_quantEngine->getModel();
+  } else {
+    d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
+    d_aloc_curr_model = true;
+  }
+  //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
+  if( d_curr_model_builder==NULL ){
+    d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
+    d_aloc_curr_model_builder = true;
   }
 
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
@@ -283,6 +287,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_curr_model(NULL),
   d_aloc_curr_model(false),
   d_curr_model_builder(NULL),
+  d_aloc_curr_model_builder(false),
   d_ppCache(),
   d_possiblePropagations(context),
   d_hasPropagated(context),
@@ -317,10 +322,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_theoryTable[theoryId] = NULL;
     d_theoryOut[theoryId] = NULL;
   }
-
-  // build model information if applicable
-  d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
-
+  
   smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -344,7 +346,9 @@ TheoryEngine::~TheoryEngine() {
     }
   }
 
-  delete d_curr_model_builder;
+  if( d_aloc_curr_model_builder ){
+    delete d_curr_model_builder;
+  }
   if( d_aloc_curr_model ){
     delete d_curr_model;
   }
@@ -583,21 +587,24 @@ void TheoryEngine::check(Theory::Effort effort) {
     }
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
-    if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+    if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
       Trace("theory::assertions-model") << endl;
       if (Trace.isOn("theory::assertions-model")) {
         printAssertions("theory::assertions-model");
       }
       //checks for theories requiring the model go at last call
-      bool builtModel = false;
+      d_curr_model->setNeedsBuild();
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
         if( theoryId!=THEORY_QUANTIFIERS ){
           Theory* theory = d_theoryTable[theoryId];
           if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
             if( theory->needsCheckLastEffort() ){
-              if( !builtModel ){
-                builtModel = true;
-                d_curr_model_builder->buildModel(d_curr_model, false);
+              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;
+                }
               }
               theory->check(Theory::EFFORT_LAST_CALL);
             }
@@ -609,9 +616,9 @@ void TheoryEngine::check(Theory::Effort effort) {
           // quantifiers engine must pass effort last call check
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
           // if returning incomplete or SAT, we have ensured that d_curr_model has been built with fullModel=true
-        } else if(options::produceModels()) {
+        } else if(options::produceModels() && !d_curr_model->isBuilt()) {
           // must build model at this point
-          d_curr_model_builder->buildModel(d_curr_model, true);
+          d_curr_model_builder->buildModel(d_curr_model);
         }
       }
     }
@@ -619,8 +626,16 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
-    if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
-      AlwaysAssert(d_masterEqualityEngine->consistent());
+    if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
+      //we will 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);
+      }
     }
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
@@ -828,6 +843,7 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
 }
 
 void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
+  Assert( fullModel ); // AJR : FIXME : remove/simplify fullModel argument everywhere
   //have shared term engine collectModelInfo
   //  d_sharedTerms.collectModelInfo( m, fullModel );
   // Consult each active theory to get all relevant information
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d8ddf7ffc..f623748cf 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -187,6 +187,7 @@ class TheoryEngine {
    * Model builder object
    */
   theory::TheoryEngineModelBuilder* d_curr_model_builder;
+  bool d_aloc_curr_model_builder;
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
   typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8579ad55f..de48c956a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -30,7 +30,7 @@ namespace CVC4 {
 namespace theory {
 
 TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
-  d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
+  d_substitutions(c, false), d_modelBuilt(false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -495,12 +495,10 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac
   cache.insert(n);
 }
 
-void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) {
-  constantReps[eqc] = const_rep;
+void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) {
+  d_constantReps[eqc] = const_rep;
   Trace("model-builder") << "    Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
-  if( !fullModel ){
-    tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
-  }
+  tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
 }
 
 bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
@@ -583,24 +581,26 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigne
   return false;
 }
 
-void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
+bool TheoryEngineModelBuilder::buildModel(Model* m)
 {
-  Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
+  Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
   TheoryModel* tm = (TheoryModel*)m;
 
   // buildModel with fullModel = true should only be called once in any context
   Assert(!tm->isBuilt());
-  tm->d_modelBuilt = fullModel;
+  tm->d_modelBuilt = true;
 
   // Reset model
   tm->reset();
 
   // Collect model info from the theories
   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
-  d_te->collectModelInfo(tm, fullModel);
+  d_te->collectModelInfo(tm, true);
 
   // model-builder specific initialization
-  preProcessBuildModel(tm, fullModel);
+  if( !preProcessBuildModel(tm) ){
+    return false;
+  }
 
   // Loop through all terms and make sure that assignable sub-terms are in the equality engine
   // Also, record #eqc per type (for finite model finding)
@@ -627,7 +627,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   Trace("model-builder") << "Collect representatives..." << std::endl;
 
   // Process all terms in the equality engine, store representatives for each EC
-  std::map< Node, Node > assertedReps, constantReps;
+  d_constantReps.clear();
+  std::map< Node, Node > assertedReps;
   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
   TypeEnumeratorProperties tep;
   if( options::finiteModelFind() ){
@@ -648,7 +649,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
     TypeNode eqct = eqc.getType();
     Assert(assertedReps.find(eqc) == assertedReps.end());
-    Assert(constantReps.find(eqc) == constantReps.end());
+    Assert(d_constantReps.find(eqc) == d_constantReps.end());
 
     // Loop through terms in this EC
     Node rep, const_rep;
@@ -680,7 +681,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       // Theories should not specify a rep if there is already a constant in the EC
       //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
       //Assert(rep.isNull() || rep == const_rep);
-      assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
+      assignConstantRep( tm, eqc, const_rep );
       typeConstSet.add(eqct.getBaseType(), const_rep);
     }
     else if (!rep.isNull()) {
@@ -741,10 +742,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
               }
               else {
                 evaluable = true;
-                Node normalized = normalize(tm, n, constantReps, true);
+                Node normalized = normalize(tm, n, true);
                 if (normalized.isConst()) {
                   typeConstSet.add(tb, normalized);
-                  assignConstantRep( tm, constantReps, *i2, normalized, fullModel );
+                  assignConstantRep( tm, *i2, normalized);
                   Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                   changed = true;
                   evaluated = true;
@@ -772,12 +773,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           for (i = repSet->begin(); i != repSet->end(); ) {
             Assert(assertedReps.find(*i) != assertedReps.end());
             Node rep = assertedReps[*i];
-            Node normalized = normalize(tm, rep, constantReps, false);
+            Node normalized = normalize(tm, rep, false);
             Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
             if (normalized.isConst()) {
               changed = true;
               typeConstSet.add(tb, normalized);
-              assignConstantRep( tm, constantReps, *i, normalized, fullModel );
+              assignConstantRep( tm, *i, normalized);
               assertedReps.erase(*i);
               i2 = i;
               ++i;
@@ -901,7 +902,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             n = *te;
           }
           Assert(!n.isNull());
-          assignConstantRep( tm, constantReps, *i2, n, fullModel );
+          assignConstantRep( tm, *i2, n);
           changed = true;
           noRepSet.erase(i2);
           if (assignOne) {
@@ -924,14 +925,12 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   }
 
 #ifdef CVC4_ASSERTIONS
-  if (fullModel) {
-    // Assert that all representatives have been converted to constants
-    for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
-      set<Node>& repSet = TypeSet::getSet(it);
-      if (!repSet.empty()) {
-        Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
-        Assert(false);
-      }
+  // Assert that all representatives have been converted to constants
+  for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
+    set<Node>& repSet = TypeSet::getSet(it);
+    if (!repSet.empty()) {
+      Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
+      Assert(false);
     }
   }
 #endif /* CVC4_ASSERTIONS */
@@ -939,76 +938,76 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   Trace("model-builder") << "Copy representatives to model..." << std::endl;
   tm->d_reps.clear();
   std::map< Node, Node >::iterator itMap;
-  for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
+  for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap) {
     tm->d_reps[itMap->first] = itMap->second;
     tm->d_rep_set.add(itMap->second.getType(), itMap->second);
   }
 
-  if (!fullModel) {
-    Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
-    // Make sure every EC has a rep
-    for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
-      tm->d_reps[itMap->first] = itMap->second;
-      tm->d_rep_set.add(itMap->second.getType(), itMap->second);
-    }
-    for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
-      set<Node>& noRepSet = TypeSet::getSet(it);
-      set<Node>::iterator i;
-      for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
-        tm->d_reps[*i] = *i;
-        tm->d_rep_set.add((*i).getType(), *i);
-      }
+  Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
+  // Make sure every EC has a rep
+  for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
+    tm->d_reps[itMap->first] = itMap->second;
+    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+  }
+  for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+    set<Node>& noRepSet = TypeSet::getSet(it);
+    set<Node>::iterator i;
+    for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
+      tm->d_reps[*i] = *i;
+      tm->d_rep_set.add((*i).getType(), *i);
     }
   }
 
   //modelBuilder-specific initialization
-  processBuildModel( tm, fullModel );
-
-  // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model)
-  if( fullModel ){
-    Trace("model-builder") << "TheoryEngineModelBuilder: Post-process model..." << std::endl;
-    d_te->postProcessModel(tm);
+  if( !processBuildModel( tm ) ){
+    return false;
+  }else{
+    return true;
   }
-  
+}
+
+void TheoryEngineModelBuilder::debugCheckModel(Model* m){
+  TheoryModel* tm = (TheoryModel*)m;
 #ifdef CVC4_ASSERTIONS
-  if (fullModel) {
-    // Check that every term evaluates to its representative in the model
-    for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
-      // eqc is the equivalence class representative
-      Node eqc = (*eqcs_i);
-      Node rep;
-      itMap = constantReps.find(eqc);
-      if (itMap == constantReps.end() && eqc.getType().isBoolean()) {
-        rep = tm->getValue(eqc);
-        Assert(rep.isConst());
-      }
-      else {
-        Assert(itMap != constantReps.end());
-        rep = itMap->second;
-      }
-      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
-      for ( ; !eqc_i.isFinished(); ++eqc_i) {
-        Node n = *eqc_i;
-        static int repCheckInstance = 0;
-        ++repCheckInstance;
-
-        Debug("check-model::rep-checking")
-          << "( " << repCheckInstance <<") "
-          << "n: " << n << endl
-          << "getValue(n): " << tm->getValue(n) << endl
-          << "rep: " << rep << endl;
-        Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
-      }
+  Assert(tm->isBuilt());
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
+  std::map< Node, Node >::iterator itMap;
+  // Check that every term evaluates to its representative in the model
+  for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
+    // eqc is the equivalence class representative
+    Node eqc = (*eqcs_i);
+    Node rep;
+    itMap = d_constantReps.find(eqc);
+    if (itMap == d_constantReps.end() && eqc.getType().isBoolean()) {
+      rep = tm->getValue(eqc);
+      Assert(rep.isConst());
+    }
+    else {
+      Assert(itMap != d_constantReps.end());
+      rep = itMap->second;
+    }
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+    for ( ; !eqc_i.isFinished(); ++eqc_i) {
+      Node n = *eqc_i;
+      static int repCheckInstance = 0;
+      ++repCheckInstance;
+
+      Debug("check-model::rep-checking")
+        << "( " << repCheckInstance <<") "
+        << "n: " << n << endl
+        << "getValue(n): " << tm->getValue(n) << endl
+        << "rep: " << rep << endl;
+      Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
     }
   }
 #endif /* CVC4_ASSERTIONS */
+  debugModel( tm );
 }
 
-
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly)
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
 {
-  std::map<Node, Node>::iterator itMap = constantReps.find(r);
-  if (itMap != constantReps.end()) {
+  std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
+  if (itMap != d_constantReps.end()) {
     return (*itMap).second;
   }
   NodeMap::iterator it = d_normalizedCache.find(r);
@@ -1027,8 +1026,8 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
       bool recurse = true;
       if (!ri.isConst()) {
         if (m->d_equalityEngine->hasTerm(ri)) {
-          itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
-          if (itMap != constantReps.end()) {
+          itMap = d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
+          if (itMap != d_constantReps.end()) {
             ri = (*itMap).second;
             recurse = false;
           }
@@ -1037,7 +1036,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
           }
         }
         if (recurse) {
-          ri = normalize(m, ri, constantReps, evalOnly);
+          ri = normalize(m, ri, evalOnly);
         }
         if (!ri.isConst()) {
           childrenConst = false;
@@ -1055,50 +1054,49 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
   return retNode;
 }
 
-void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
-  
+bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) {
+  return true;
 }
 
-void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
-{
-  if (fullModel) {
-    Trace("model-builder") << "Assigning function values..." << endl;
-    //construct function values
-    for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
-      Node n = it->first;
-      if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
-        TypeNode type = n.getType();
-        uf::UfModelTree ufmt( n );
-        Node default_v, un, simp, v;
-        for( size_t i=0; i<it->second.size(); i++ ){
-          un = it->second[i];
-          vector<TNode> children;
-          children.push_back(n);
-          for (size_t j = 0; j < un.getNumChildren(); ++j) {
-            children.push_back(m->getRepresentative(un[j]));
-          }
-          simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
-          v = m->getRepresentative(un);
-          Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")" << endl;
-          ufmt.setValue(m, simp, v);
-          default_v = v;
-        }
-        if( default_v.isNull() ){
-          //choose default value from model if none exists
-          TypeEnumerator te(type.getRangeType());
-          default_v = (*te);
-        }
-        ufmt.setDefaultValue( m, default_v );
-        if(options::condenseFunctionValues()) {
-          ufmt.simplify();
+bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){
+  Trace("model-builder") << "Assigning function values..." << endl;
+  //construct function values
+  for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+    Node n = it->first;
+    if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
+      TypeNode type = n.getType();
+      Trace("model-builder") << "  Assign function value for " << n << " " << type << std::endl;
+      uf::UfModelTree ufmt( n );
+      Node default_v, un, simp, v;
+      for( size_t i=0; i<it->second.size(); i++ ){
+        un = it->second[i];
+        vector<TNode> children;
+        children.push_back(n);
+        for (size_t j = 0; j < un.getNumChildren(); ++j) {
+          children.push_back(m->getRepresentative(un[j]));
         }
-        Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
-        Trace("model-builder") << "  Assigning (" << n << ") to (" << val << ")" << endl;
-        m->d_uf_models[n] = val;
-        //ufmt.debugPrint( std::cout, m );
+        simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+        v = m->getRepresentative(un);
+        Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")" << endl;
+        ufmt.setValue(m, simp, v);
+        default_v = v;
+      }
+      if( default_v.isNull() ){
+        //choose default value from model if none exists
+        TypeEnumerator te(type.getRangeType());
+        default_v = (*te);
+      }
+      ufmt.setDefaultValue( m, default_v );
+      if(options::condenseFunctionValues()) {
+        ufmt.simplify();
       }
+      Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
+      Trace("model-builder") << "  Assigning (" << n << ") to (" << val << ")" << endl;
+      m->d_uf_models[n] = val;
+      //ufmt.debugPrint( std::cout, m );
     }
   }
+  return true;
 }
 
 } /* namespace CVC4::theory */
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index c30d1eabc..82341c377 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -36,7 +36,7 @@ class TheoryModel : public Model
 protected:
   /** substitution map for this model */
   SubstitutionMap d_substitutions;
-  context::CDO<bool> d_modelBuilt;
+  bool d_modelBuilt;
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel() throw();
@@ -74,7 +74,9 @@ protected:
   Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
 public:
   /** is built */
-  bool isBuilt() { return d_modelBuilt.get(); }
+  bool isBuilt() { return d_modelBuilt; }
+  /** set need build */
+  void setNeedsBuild() { d_modelBuilt = false; }
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
    * on this model.
@@ -266,15 +268,17 @@ protected:
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_normalizedCache;
   typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+  std::map< Node, Node > d_constantReps;
 
   /** process build model */
-  virtual void preProcessBuildModel(TheoryModel* m, bool fullModel);
-  virtual void processBuildModel(TheoryModel* m, bool fullModel);
+  virtual bool preProcessBuildModel(TheoryModel* m);
+  virtual bool processBuildModel(TheoryModel* m);
+  virtual void debugModel( TheoryModel* m ) {}
   /** normalize representative */
-  Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
+  Node normalize(TheoryModel* m, TNode r, bool evalOnly);
   bool isAssignable(TNode n);
   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-  void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
+  void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
   /** is v an excluded codatatype value */
   bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
   bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
@@ -287,7 +291,8 @@ public:
   /** Build model function.
    *    Should be called only on TheoryModels m
    */
-  void buildModel(Model* m, bool fullModel);
+  bool buildModel(Model* m);
+  void debugCheckModel(Model* m);
 };/* class TheoryEngineModelBuilder */
 
 }/* CVC4::theory namespace */