Optimizations for QCF to check relevant domain of variable argument positions eagerly, global ordering mechanism for quantified formulas within check. Refactoring of term database.

25 files changed, 432 insertions, 242 deletions

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d08f5f533..a2809bd67 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -576,8 +576,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
     return theory::quantifiers::QCF_PROP_EQ;
   } else if(optarg == "partial") {
     return theory::quantifiers::QCF_PARTIAL;
-  } else if(optarg == "mc" ) {
-    return theory::quantifiers::QCF_MC;
   } else if(optarg ==  "help") {
     puts(s_qcfModeHelp.c_str());
     exit(1);
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index a437cfc97..5749da972 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -83,8 +83,6 @@ enum QcfMode {
   QCF_PROP_EQ,
   /** use qcf for conflicts, propagations and heuristic instantiations */
   QCF_PARTIAL,
-  /** use qcf for model checking */
-  QCF_MC,
 };
 
 enum UserPatMode {
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index ed000427f..c8d18aced 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -82,7 +82,7 @@ QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule(
 void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     d_sqtc.clear();
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( d_quant_processed.find( q )==d_quant_processed.end() ){
         d_quant_processed[q] = true;
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 38d8c0d81..43f5ee2fd 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -298,7 +298,6 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     }
   }
   if( d_firstTime ){
-    Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
     //must return something
     d_firstTime = false;
     return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f8a9eefcb..27bbb0f5f 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -34,7 +34,7 @@ struct sortConjectureScore {
 };
 
 
-void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
+void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
   if( index==n.getNumChildren() ){
     Assert( n.hasOperator() );
     if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
@@ -42,7 +42,7 @@ void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
       d_op_terms.push_back( n );
     }
   }else{
-    d_child[s->getTermDatabase()->d_arg_reps[n][index]].addTerm( s, n, index+1 );
+    d_child[terms[index]].addTerm( terms, n, index+1 );
   }
 }
 
@@ -369,7 +369,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           TNode n = (*ieqc_i);
           if( getTermDatabase()->hasTermCurrent( n ) ){
             if( isHandledTerm( n ) ){
-              d_op_arg_index[r].addTerm( this, n );
+              d_op_arg_index[r].addTerm( getTermDatabase()->d_arg_reps[n], n );
             }
           }
           ++ieqc_i;
@@ -489,7 +489,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       d_thm_index.clear();
       std::vector< Node > provenConj;
       quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
-      for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<m->getNumAssertedQuantifiers(); i++ ){
         Node q = m->getAssertedQuantifier( i );
         Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
         Node conjEq;
@@ -1569,10 +1569,12 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         if( d_match_status_child_num==0 ){
           //initial binding
           TNode f = s->getTgFunc( d_typ, d_status_num );
-          std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
-          if( it!=s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.end() ){
-            d_match_children.push_back( it->second.d_data.begin() );
-            d_match_children_end.push_back( it->second.d_data.end() );
+          //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
+          Assert( !eqc.isNull() );
+          TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
+          if( tat ){
+            d_match_children.push_back( tat->d_data.begin() );
+            d_match_children_end.push_back( tat->d_data.end() );
           }else{
             d_match_status++;
             d_match_status_child_num--;
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b6e17e7a1..c89d0f2ee 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -39,7 +39,7 @@ public:
   std::map< TNode, OpArgIndex > d_child;
   std::vector< TNode > d_ops;
   std::vector< TNode > d_op_terms;
-  void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 );
+  void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 );
   Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
   void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
 };
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 59bd10493..a833f48d2 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -30,10 +30,23 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::quantifiers::fmcheck;
 
+struct sortQuantifierRelevance {
+  FirstOrderModel * d_fm;
+  bool operator() (Node i, Node j) {
+    int wi = d_fm->getRelevanceValue( i );
+    int wj = d_fm->getRelevanceValue( j );
+    if( wi==wj ){
+      return i<j;
+    }else{
+      return wi<wj;
+    }
+  }
+};
+
 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_rlv_count = 0;
 }
 
 void FirstOrderModel::assertQuantifier( Node n ){
@@ -44,6 +57,19 @@ void FirstOrderModel::assertQuantifier( Node n ){
   }
 }
 
+unsigned FirstOrderModel::getNumAssertedQuantifiers() { 
+  return d_forall_asserts.size(); 
+}
+
+Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { 
+  if( !ordered || d_forall_rlv_assert.empty() ){
+    return d_forall_asserts[i]; 
+  }else{
+    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+    return d_forall_rlv_assert[i];
+  }
+}
+
 Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
   std::vector< Node > children;
   if( n.getNumChildren()>0 ){
@@ -74,11 +100,11 @@ void FirstOrderModel::initialize() {
   processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
-  for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
     Node f = getAssertedQuantifier( i );
     if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
-      for(unsigned i=0; i<f[0].getNumChildren(); i++){
-        d_quant_var_id[f][f[0][i]] = i;
+      for(unsigned j=0; j<f[0].getNumChildren(); j++){
+        d_quant_var_id[f][f[0][j]] = j;
       }
     }
     processInitializeQuantifier( f );
@@ -120,6 +146,61 @@ bool FirstOrderModel::checkNeeded() {
 
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
+  
+  //order the quantified formulas
+  if( !d_forall_rlv_vec.empty() ){
+    Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
+    d_forall_rlv_assert.clear();
+    Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl;
+    std::map< Node, bool > qassert;
+    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+      qassert[d_forall_asserts[i]] = true;
+    }
+    Trace("fm-relevant-debug") << "Sort the relevant quantified formulas..." << std::endl;
+    sortQuantifierRelevance sqr;
+    sqr.d_fm = this;
+    std::sort( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), sqr );
+    Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
+    for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
+      Node q = d_forall_rlv_vec[i];
+      if( qassert.find( q )!=qassert.end() ){
+        Trace("fm-relevant") << "   " << d_forall_rlv[q] << " : " << q << std::endl;
+        d_forall_rlv_assert.push_back( q );
+      }
+    }
+    Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
+    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+      Node q = d_forall_asserts[i];
+      if( std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )==d_forall_rlv_assert.end() ){
+        d_forall_rlv_assert.push_back( q );
+      }else{
+        Trace("fm-relevant-debug") << "...already included " << q << std::endl;
+      }
+    }
+    Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
+    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+  }
+}
+
+void FirstOrderModel::markRelevant( Node q ) {
+  if( q!=d_last_forall_rlv ){
+    Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
+    if( std::find( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q )==d_forall_rlv_vec.end() ){
+      d_forall_rlv_vec.push_back( q );
+    }
+    d_forall_rlv[ q ] = d_rlv_count;
+    d_rlv_count++;
+    d_last_forall_rlv = q;
+  }
+}
+
+int FirstOrderModel::getRelevanceValue( Node q ) {
+  std::map< Node, unsigned >::iterator it = d_forall_rlv.find( q );
+  if( it==d_forall_rlv.end() ){
+    return -1;
+  }else{
+    return it->second;
+  }
 }
 
 //bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 4ab1dd1c3..cbe83cfa5 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -49,6 +49,12 @@ protected:
   QuantifiersEngine * d_qe;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
+  /** quantified formulas marked as relevant */
+  unsigned d_rlv_count;
+  std::map< Node, unsigned > d_forall_rlv;
+  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 */
@@ -59,9 +65,9 @@ public: //for Theory Quantifiers:
   /** assert quantifier */
   void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
-  int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+  unsigned getNumAssertedQuantifiers();
   /** get asserted quantifier */
-  Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+  Node getAssertedQuantifier( unsigned i, bool ordered = false );
   /** initialize model for term */
   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
   virtual void processInitializeModelForTerm( Node n ) = 0;
@@ -96,8 +102,10 @@ private:
 public:
   /** reset round */
   void reset_round();
-  /** is quantified formula asserted */
-  //bool isQuantifierAsserted( TNode q );
+  /** mark quantified formula relevant */
+  void markRelevant( Node q );
+  /** get relevance value */
+  int getRelevanceValue( Node q );
   /** set quantified formula active/inactive 
    * a quantified formula may be set inactive if for instance:
    *   - it is entailed by other quantified formulas
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0276cf7ab..6b06b9e5c 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -350,11 +350,11 @@ void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
     }
     //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( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node q = fm->getAssertedQuantifier( i );
         //make sure all types are set
-        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-          preInitializeType( fm, q[0][i].getType() );
+        for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+          preInitializeType( fm, q[0][j].getType() );
         }
       }
     }
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index c6f4affc5..d4be58636 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -723,6 +723,9 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
       }else{
         Trace("qip-prop-debug") << it->first << " ";
       }
+    }else{
+      //mark the quantified formula as relevant
+      d_qe->markRelevant( it->second.d_q );
     }
   }
   Trace("qip-prop-debug") << std::endl;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index cc9b56a7c..fe4867b4e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -46,7 +46,7 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
 }
 
 unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       return QuantifiersEngine::QEFFORT_STANDARD;
@@ -59,7 +59,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   d_cbqi_set_quant_inactive = false;
   d_incomplete_check = false;
   //check if any cbqi lemma has not been added yet
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
@@ -115,7 +115,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
     }
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     for( int ee=0; ee<=1; ee++ ){
-      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
         Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
         if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
           process( q, e, ee );
@@ -236,7 +236,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){
 
 Node InstStrategyCbqi::getNextDecisionRequest(){
   // all counterexample literals that are not asserted
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     if( hasAddedCbqiLemma( q ) ){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
@@ -316,8 +316,10 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
     }
   }
   //print debug
-  Debug("quant-arith-debug") << std::endl;
-  debugPrint( "quant-arith-debug" );
+  if( Debug.isOn("quant-arith-debug") ){
+    Debug("quant-arith-debug") << std::endl;
+    debugPrint( "quant-arith-debug" );
+  }
   d_counter++;
 }
 
@@ -355,10 +357,10 @@ void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
       bool m_point_valid = true;
       int lem = 0;
       //scan over all instantiation rows
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
         Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
         Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
-        for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+        for( unsigned j=0; j<d_instRows[ic].size(); j++ ){
           ArithVar x = d_instRows[ic][j];
           if( !d_ceTableaux[ic][x].empty() ){
             if( Debug.isOn("quant-arith-simplex") ){
@@ -474,25 +476,25 @@ void InstStrategySimplex::debugPrint( const char* c ){
   }
   Debug(c) << std::endl;
 
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Debug(c) << f << std::endl;
     Debug(c) << "   Inst constants: ";
-    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      if( i>0 ){
+    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      if( j>0 ){
         Debug( c ) << ", ";
       }
       Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
     }
     Debug(c) << std::endl;
-    for( int j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
       Debug(c) << "   Instantiation rows for " << ic << " : ";
-      for( int i=0; i<(int)d_instRows[ic].size(); i++ ){
-        if( i>0 ){
+      for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
+        if( k>0 ){
           Debug(c) << ", ";
         }
-        Debug(c) << d_instRows[ic][i];
+        Debug(c) << d_instRows[ic][k];
       }
       Debug(c) << std::endl;
     }
@@ -699,7 +701,7 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
   //must register with the instantiator
   //must explicitly remove ITEs so that we record dependencies
   std::vector< Node > ce_vars;
-  for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
     ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
   }
   std::vector< Node > lems;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 6d6991476..bb514f41b 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -573,8 +573,8 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
       Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
     }
     int addedLemmas = 0;
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         if( process( q, fullEffort ) ){
           //added lemma
@@ -627,7 +627,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
         if( r==0 ){
           ts = rd->getRDomain( f, i )->d_terms.size();
         }else{
-          ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+          ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() );
         }
         max_zero.push_back( fullEffort && ts==0 );
         ts = ( fullEffort && ts==0 ) ? 1 : ts;
@@ -643,6 +643,11 @@ bool FullSaturation::process( Node f, bool fullEffort ){
         }
       }
       if( !has_zero ){
+        std::vector< TypeNode > ftypes;
+        for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+          ftypes.push_back( f[0][i].getType() );
+        }
+      
         Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
         unsigned max_i = 0;
         bool success;
@@ -660,7 +665,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 if( options::cbqi() && r==1 && !max_zero[index] ){
                   //skip inst constant nodes
                   while( nv<maxs[index] && nv<=max_i &&
-                          quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+                          quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){
                     nv++;
                   }
                 }
@@ -689,7 +694,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 }else if( r==0 ){
                   terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
                 }else{
-                  terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+                  terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
                 }
               }
               if( d_quantEngine->addInstantiation( f, terms, false ) ){
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b59734720..955dc5d86 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -123,8 +123,8 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     //collect all active quantified formulas belonging to this
     bool quantActive = false;
     d_quants.clear();
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         quantActive = true;
         d_quants.push_back( q );
@@ -137,7 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
       doInstantiationRound( e );
       if( d_quantEngine->inConflict() ){
         Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
-        Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting();
+        Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound();
         if( lastWaiting>0 ){
           Trace("inst-engine") << " (prev " << lastWaiting << ")";
         }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index bdb416b6b..b0ca43cfe 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -54,10 +54,10 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
-    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
       std::vector< Node > vars;
-      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
       RepSetIterator riter( d_qe, &(fm->d_rep_set) );
@@ -65,8 +65,8 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
         while( !riter.isFinished() ){
           tests++;
           std::vector< Node > terms;
-          for( int i=0; i<riter.getNumTerms(); i++ ){
-            terms.push_back( riter.getTerm( i ) );
+          for( int k=0; k<riter.getNumTerms(); k++ ){
+            terms.push_back( riter.getTerm( k ) );
           }
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
@@ -149,7 +149,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
     if( optUseModel() ){
       Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
       //check if any quantifiers are un-initialized
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
         if( isQuantifierActive( f ) ){
           int lems = initializeQuantifier( f, f );
@@ -173,7 +173,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
         d_quant_sat.clear();
         d_uf_prefs.clear();
-        for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
           Node f = fm->getAssertedQuantifier( i );
           if( isQuantifierActive( f ) ){
             analyzeQuantifier( fm, f );
@@ -190,7 +190,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
           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( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+          for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
             Node f = fm->getAssertedQuantifier( i );
             if( isQuantifierActive( f ) ){
               int lems = doInstGen( fm, f );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a7e272be0..f94e947e5 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -83,8 +83,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine-debug") << "Check model..." << std::endl;
       d_incomplete_check = false;
       //print debug
-      Trace("fmf-model-complete") << std::endl;
-      debugPrint("fmf-model-complete");
+      if( Trace.isOn("fmf-model-complete") ){
+        Trace("fmf-model-complete") << std::endl;
+        debugPrint("fmf-model-complete");
+      }
       //successfully built an acceptable model, now check it
       addedLemmas += checkModel();
     }else{
@@ -99,8 +101,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
-      Trace("fmf-consistent") << std::endl;
-      debugPrint("fmf-consistent");
+      if( Trace.isOn("fmf-consistent") ){
+        Trace("fmf-consistent") << std::endl;
+        debugPrint("fmf-consistent");
+      }
     }
   }
 }
@@ -177,35 +181,30 @@ int ModelEngine::checkModel(){
   d_addedLemmas = 0;
   d_totalLemmas = 0;
   //for statistics
-  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-    Node f = fm->getAssertedQuantifier( i );
-    int totalInst = 1;
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      TypeNode tn = f[0][i].getType();
-      if( fm->d_rep_set.hasType( tn ) ){
-        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+  if( Trace.isOn("model-engine") ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      int totalInst = 1;
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+        TypeNode tn = f[0][j].getType();
+        if( fm->d_rep_set.hasType( tn ) ){
+          totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+        }
       }
+      d_totalLemmas += totalInst;
     }
-    d_totalLemmas += totalInst;
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
-    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node f = fm->getAssertedQuantifier( i );
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i, true );
       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
       if( considerQuantifiedFormula( f ) ){
         exhaustiveInstantiate( f, e );
-        if( Trace.isOn("model-engine-warn") ){
-          if( d_addedLemmas>10000 ){
-            Debug("fmf-exit") << std::endl;
-            debugPrint("fmf-exit");
-            exit( 0 );
-          }
-        }
         if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
           break;
         }
@@ -222,7 +221,7 @@ int ModelEngine::checkModel(){
 
   //print debug information
   if( d_quantEngine->inConflict() ){
-    Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl;
+    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
   }else{
     Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
     Trace("model-engine") << d_totalLemmas << std::endl;
@@ -320,15 +319,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
 
 void ModelEngine::debugPrint( const char* c ){
   Trace( c ) << "Quantifiers: " << std::endl;
-  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Trace( c ) << "   ";
-    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
+    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){
       Trace( c ) << "*Inactive* ";
     }else{
       Trace( c ) << "           ";
     }
-    Trace( c ) << f << std::endl;
+    Trace( c ) << q << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e5df41510..1cbfbd99b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -46,7 +47,7 @@ QuantInfo::~QuantInfo() {
 }
 
 
-void QuantInfo::initialize( Node q, Node qn ) {
+void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_q = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_match.push_back( TNode::null() );
@@ -107,6 +108,59 @@ void QuantInfo::initialize( Node q, Node qn ) {
     Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
   }
   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+  
+  if( d_mg->isValid() ){
+    //optimization : record variable argument positions for terms that must be matched
+    std::vector< TNode > vars;
+    //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
+    //if( options::qcfSkipRd() ){
+    //  for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+    //    vars.push_back( d_vars[j] );
+    //  }
+    //}
+    //get all variables that are always relevant
+    std::map< TNode, bool > visited;
+    getPropagateVars( vars, q[1], false, visited );
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Node v = vars[j];
+      TNode f = p->getTermDatabase()->getMatchOperator( v );
+      if( !f.isNull() ){
+        Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+        for( unsigned k=0; k<v.getNumChildren(); k++ ){
+          Node n = v[k];
+          std::map< TNode, int >::iterator itv = d_var_num.find( n );
+          if( itv!=d_var_num.end() ){
+            Trace("qcf-opt") << "  arg " << k << " is var #" << itv->second << std::endl;
+            if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
+              d_var_rel_dom[itv->second][f].push_back( k );
+            }
+          }
+        }
+      }
+    }    
+  }
+}
+
+void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+  std::map< TNode, bool >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    visited[n] = true;
+    bool rec = true;
+    bool newPol = pol;
+    if( d_var_num.find( n )!=d_var_num.end() ){
+      Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
+      vars.push_back( n );
+    }else if( MatchGen::isHandledBoolConnective( n ) ){
+      Assert( n.getKind()!=IMPLIES );
+      QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
+    }
+    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+    if( rec ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        getPropagateVars( vars, n[i], pol, visited );
+      }
+    }
+  }
 }
 
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
@@ -327,7 +381,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         return 1;
       }else{
         //std::map< int, TNode >::iterator itm = d_match.find( v );
-
+        bool isGroundRep = false;
         if( vn!=-1 ){
           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
           //std::map< int, TNode >::iterator itmn = d_match.find( vn );
@@ -373,13 +427,14 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         }else{
           Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
           if( d_match[v].isNull() ){
+            //isGroundRep = true;   ??
           }else{
             //compare ground values
             Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
             return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
           }
         }
-        if( setMatch( p, v, n ) ){
+        if( setMatch( p, v, n, isGroundRep ) ){
           Debug("qcf-match-debug") << "  -> success" << std::endl;
           return 1;
         }else{
@@ -445,8 +500,23 @@ bool QuantInfo::isConstrainedVar( int v ) {
   }
 }
 
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) {
   if( getCurrentCanBeEqual( p, v, n ) ){
+    if( isGroundRep ){
+      //fail if n does not exist in the relevant domain of each of the argument positions
+      std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
+      if( it!=d_var_rel_dom.end() ){
+        for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          for( unsigned j=0; j<it2->second.size(); j++ ){
+            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->second << "." << it2->second[j] << "?" << std::endl;
+            if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
+              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+              return false;
+            }
+          }
+        }
+      }
+    }
     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
     d_match[v] = n;
     return true;
@@ -566,7 +636,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 if( !z.isNull() ){
                   Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
                   assigned.push_back( vn );
-                  if( !setMatch( p, vn, z ) ){
+                  if( !setMatch( p, vn, z, false ) ){
                     success = false;
                     break;
                   }
@@ -608,7 +678,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
             if( !sum.isNull() ){
               assigned.push_back( slv_v );
               Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
-              if( !setMatch( p, slv_v, sum ) ){
+              if( !setMatch( p, slv_v, sum, false ) ){
                 success = false;
               }
               p->d_tempCache.push_back( sum );
@@ -694,7 +764,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 int currIndex = d_una_eqc_count[d_una_index];
                 d_una_eqc_count[d_una_index]++;
                 Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
-                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true ) ){
                   d_match_term[d_unassigned[d_una_index]] = TNode::null();
                   Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
                   d_una_index++;
@@ -1125,7 +1195,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }else{
       //unassigned, set match to true/false
       d_qni_bound[0] = vn;
-      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false );
       d_child_counter = 0;
     }
     if( d_child_counter==0 ){
@@ -1365,17 +1435,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           d_qni_bound_cons.clear();
         }
       }
-      /*
-      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
-        d_matched_basis = true;
-        Node f = getMatchOperator( d_n );
-        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
-        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
-          success = true;
-          d_qni_bound[0] = d_qni_var_num[0];
-        }
-      }
-      */
     }
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     d_wasSet = success;
@@ -1595,7 +1654,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {
                 d_qni.push_back( it );
                 //set the match
-                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true ) ){
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;
                   if( d_qn.size()<d_qni_size ){
                     d_qn.push_back( &it->second );
@@ -1640,7 +1699,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             d_qni[index]++;
             if( d_qni[index]!=d_qn[index]->d_data.end() ){
               success = true;
-              if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
+              if( qi->setMatch( p, itb->second, d_qni[index]->first, true ) ){
                 Debug("qcf-match-debug") << "       Bind next variable" << std::endl;
                 if( d_qn.size()<d_qni_size ){
                   d_qn.push_back( &d_qni[index]->second );
@@ -1756,8 +1815,7 @@ bool MatchGen::isHandled( TNode n ) {
 
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
 QuantifiersModule( qe ),
-d_conflict( c, false ),
-d_qassert( c ) {
+d_conflict( c, false ) {
   d_fid_count = 0;
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -1782,7 +1840,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
     Trace("qcf-qregister") << " : " << q << std::endl;
     //make QcfNode structure
     Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
-    d_qinfo[q].initialize( q, q[1] );
+    d_qinfo[q].initialize( this, q, q[1] );
 
     //debug print
     Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
@@ -1797,7 +1855,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
         Trace("qcf-qregister") << std::endl;
       }
     }
-
+    
     Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
   }
 }
@@ -1805,10 +1863,8 @@ void QuantConflictFind::registerQuantifier( Node q ) {
 short QuantConflictFind::getMaxQcfEffort() {
   if( options::qcfMode()==QCF_CONFLICT_ONLY ){
     return effort_conflict;
-  }else if( options::qcfMode()==QCF_PROP_EQ ){
+  }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){
     return effort_prop_eq;
-  }else if( options::qcfMode()==QCF_MC ){
-    return effort_mc;
   }else{
     return 0;
   }
@@ -1833,16 +1889,13 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc
 
 void QuantConflictFind::assertNode( Node q ) {
+  /*
   if( d_quantEngine->hasOwnership( q, this ) ){
     Trace("qcf-proc") << "QCF : assertQuantifier : ";
     debugPrintQuant("qcf-proc", q);
     Trace("qcf-proc") << std::endl;
-    d_qassert.push_back( q );
-    //set the eqRegistries that this depends on to true
-    //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
-    //  it->first->d_active.set( true );
-    //}
   }
+  */
 }
 
 /** new node */
@@ -1904,28 +1957,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
 
       //determine order for quantified formulas
       std::vector< Node > qorder;
-      std::map< Node, bool > qassert;
-      //mark which are asserted
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        qassert[d_qassert[i]] = true;
-      }
-      //add which ones are specified in the order
-      for( unsigned i=0; i<d_quant_order.size(); i++ ){
-        Node n = d_quant_order[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
-          qorder.push_back( n );
-        }
-      }
-      d_quant_order.clear();
-      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
-      //add remaining
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        Node n = d_qassert[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
-          qorder.push_back( n );
+      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+        if( d_quantEngine->hasOwnership( q, this ) ){
+          qorder.push_back( q );
         }
       }
-
       if( Trace.isOn("qcf-debug") ){
         Trace("qcf-debug") << std::endl;
         debugPrint("qcf-debug");
@@ -1974,7 +2011,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       Trace("qcf-inst") << std::endl;
                       ++addedLemmas;
                       if( e==effort_conflict ){
-                        d_quant_order.insert( d_quant_order.begin(), q );
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_conflict_inst);
                         if( options::qcfAllConflict() ){
                           isConflict = true;
@@ -1983,6 +2020,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                         }
                         break;
                       }else if( e==effort_prop_eq ){
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_prop_inst);
                       }
                     }else{
@@ -2040,60 +2078,24 @@ void QuantConflictFind::computeRelevantEqr() {
     //d_uf_terms.clear();
     //d_eqc_uf_terms.clear();
     d_eqcs.clear();
-    d_model_basis.clear();
     //d_arg_reps.clear();
     //double clSet = 0;
     //if( Trace.isOn("qcf-opt") ){
     //  clSet = double(clock())/double(CLOCKS_PER_SEC);
     //}
 
-    //long nTermst = 0;
-    //long nTerms = 0;
-    //long nEqc = 0;
-
-    //which nodes are irrelevant for disequality matches
-    std::map< TNode, bool > irrelevant_dnode;
     //now, store matches
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
     while( !eqcs_i.isFinished() ){
-      //nEqc++;
       Node r = (*eqcs_i);
       if( getTermDatabase()->hasTermCurrent( r ) ){
         TypeNode rtn = r.getType();
-        if( options::qcfMode()==QCF_MC ){
-          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
-          if( itt==d_eqcs.end() ){
-            Node mb = getTermDatabase()->getModelBasisTerm( rtn );
-            if( !getEqualityEngine()->hasTerm( mb ) ){
-              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
-              Assert( false );
-            }
-            Node mbr = getRepresentative( mb );
-            if( mbr!=r ){
-              d_eqcs[rtn].push_back( mbr );
-            }
-            d_eqcs[rtn].push_back( r );
-            d_model_basis[rtn] = mb;
-          }else{
-            itt->second.push_back( r );
-          }
-        }else{
-          if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
-            d_eqcs[rtn].push_back( r );
-          }
+        if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+          d_eqcs[rtn].push_back( r );
         }
       }
       ++eqcs_i;
     }
-    /*
-    if( Trace.isOn("qcf-opt") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
-      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
-      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
-      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
-    }
-    */
   }
 }
 
@@ -2120,21 +2122,6 @@ void QuantConflictFind::debugPrint( const char * c ) {
       ++eqc_i;
     }
     Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    /*
-    EqcInfo * eqcn = getEqcInfo( n, false );
-    if( eqcn ){
-      Trace(c) << "    DEQ : {";
-      pr = false;
-      for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
-        if( (*it).second ){
-          Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
-          pr = true;
-        }
-      }
-      Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    }
-    //}
-    */
     ++eqcs_i;
   }
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 36fcaddf5..8b42b0916 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -114,6 +114,9 @@ private: //for completing match
   int d_unassigned_nvar;
   int d_una_index;
   std::vector< int > d_una_eqc_count;
+  //optimization: track which arguments variables appear under UF terms in
+  std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
+  void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
 public:
   QuantInfo();
   ~QuantInfo();
@@ -138,7 +141,7 @@ public:
   bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); }
 
   bool matchGeneratorIsValid() const { return d_mg->isValid(); }
-  bool getNextMatch( QuantConflictFind * p) {
+  bool getNextMatch( QuantConflictFind * p ) {
     return d_mg->getNextMatch(p, this);
   }
 
@@ -146,7 +149,7 @@ public:
   void reset_round( QuantConflictFind * p );
 public:
   //initialize
-  void initialize( Node q, Node qn );
+  void initialize( QuantConflictFind * p, Node q, Node qn );
   //current constraints
   std::vector< TNode > d_match;
   std::vector< TNode > d_match_term;
@@ -158,7 +161,7 @@ public:
   bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
   int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
-  bool setMatch( QuantConflictFind * p, int v, TNode n );
+  bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep );
   bool isMatchSpurious( QuantConflictFind * p );
   bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
   bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
@@ -178,7 +181,6 @@ class QuantConflictFind : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   context::CDO< bool > d_conflict;
-  std::vector< Node > d_quant_order;
   std::map< Kind, Node > d_zero;
   //for storing nodes created during t-constraint solving (prevents memory leaks)
   std::vector< Node > d_tempCache;
@@ -192,18 +194,14 @@ public:  //for ground terms
   Node d_false;
   TNode getZero( Kind k );
 private:
-  //currently asserted quantifiers
-  NodeList d_qassert;
   std::map< Node, QuantInfo > d_qinfo;
 private:  //for equivalence classes
   // type -> list(eqc)
   std::map< TypeNode, std::vector< TNode > > d_eqcs;
-  std::map< TypeNode, Node > d_model_basis;
 public:
   enum {
     effort_conflict,
     effort_prop_eq,
-    effort_mc,
   };
   short d_effort;
   void setEffort( int e ) { d_effort = e; }
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9181677ee..b353fce2f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -95,7 +95,7 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    for( int i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
       Node q = d_model->getAssertedQuantifier( i );
       Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 5bf8d8a8d..07b1462c6 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -285,7 +285,7 @@ void RewriteEngine::registerQuantifier( Node f ) {
       //make the quantified formula
       d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
       Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
-      d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] );
+      d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] );
     }
   }
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3d3646d7d..ef301c2cf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -78,8 +78,8 @@ TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argInd
 
 void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-    for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
-    Debug(c) << it->first << std::endl;
+    for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  "; }
+    Trace(c) << it->first << std::endl;
     it->second.debugPrint( c, n, depth+1 );
   }
 }
@@ -111,6 +111,20 @@ Node TermDb::getGroundTerm( Node f, unsigned i ) {
   return d_op_map[f][i];
 }
 
+unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
+  std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn );
+  if( it!=d_type_map.end() ){
+    return it->second.size();
+  }else{
+    return 0;
+  }
+}
+
+Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
+  Assert( i<d_type_map[tn].size() );
+  return d_type_map[tn][i];
+}
+
 Node TermDb::getMatchOperator( Node n ) {
   //return n.getOperator();
   Kind k = n.getKind();
@@ -205,6 +219,21 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   }
 }
 
+bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+  Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
+  std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
+  if( it != d_func_map_rel_dom.end() ){
+    std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
+    if( it2!=it->second.end() ){
+      return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
+    }else{
+      return false;
+    }
+  }else{
+    return false;
+  }
+}
+
 //return a term n' equivalent to n
 //  maximal subterms of n' are representatives in the equality engine qy
 Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
@@ -533,6 +562,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_arg_reps.clear();
   d_func_map_trie.clear();
   d_func_map_eqc_trie.clear();
+  d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
@@ -596,16 +626,18 @@ bool TermDb::reset( Theory::Effort effort ){
           }
           computeArgReps( n );
 
-          if( Trace.isOn("term-db-debug") ){
-            Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
-            for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
-              Trace("term-db-debug") << d_arg_reps[n][i] << " ";
-            }
-            Trace("term-db-debug") << std::endl;
-            if( ee->hasTerm( n ) ){
-              Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+          Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+          for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+            Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+            if( std::find( d_func_map_rel_dom[it->first][i].begin(), 
+                           d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){
+              d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] );
             }
           }
+          Trace("term-db-debug") << std::endl;
+          if( ee->hasTerm( n ) ){
+            Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+          }
           Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
           if( at!=n && ee->areEqual( at, n ) ){
             NoMatchAttribute nma;
@@ -650,12 +682,12 @@ bool TermDb::reset( Theory::Effort effort ){
   Trace("term-db-stats") << "TermDb: Reset" << std::endl;
   Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
   Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
-  if( Debug.isOn("term-db") ){
-    Debug("term-db") << "functions : " << std::endl;
+  if( Trace.isOn("term-db-index") ){
+    Trace("term-db-index") << "functions : " << std::endl;
     for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
       if( it->second.size()>0 ){
-        Debug("term-db") << "- " << it->first << std::endl;
-        d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+        Trace("term-db-index") << "- " << it->first << std::endl;
+        d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
       }
     }
   }
@@ -929,10 +961,10 @@ Node TermDb::getInstantiationConstant( Node q, int i ) const {
 }
 
 /** get number of instantiation constants for q */
-int TermDb::getNumInstantiationConstants( Node q ) const {
+unsigned TermDb::getNumInstantiationConstants( Node q ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
   if( it!=d_inst_constants.end() ){
-    return (int)it->second.size();
+    return it->second.size();
   }else{
     return 0;
   }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 76bd623a8..a62b343a2 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -163,11 +163,21 @@ namespace fmcheck {
 }
 
 class TermDbSygus;
+class QuantConflictFind;
+class RelevantDomain;
+class ConjectureGenerator;
+class TermGenerator;
+class TermGenEnv;
 
 class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
+  //TODO: eliminate most of these
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
+  friend class ::CVC4::theory::quantifiers::QuantConflictFind;
+  friend class ::CVC4::theory::quantifiers::RelevantDomain;
+  friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
+  friend class ::CVC4::theory::quantifiers::TermGenEnv;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
 private:
   /** reference to the quantifiers engine */
@@ -180,12 +190,6 @@ private:
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
   bool d_consistent_ee;
-  /** set has term */
-  void setHasTerm( Node n );
-  /** evaluate term */
-  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
-  TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
-  bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -195,7 +199,14 @@ public:
   /** constants */
   Node d_zero;
   Node d_one;
-
+public:
+  /** presolve (called once per user check-sat) */
+  void presolve();
+  /** reset (calculate which terms are active) */
+  bool reset( Theory::Effort effort );
+  /** identify */
+  std::string identify() const { return "TermDb"; }  
+private:
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
@@ -208,24 +219,29 @@ public:
   /** map from operators to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
+  /** mapping from operators to their representative relevant domains */
+  std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
-  std::map< Node, Node > d_term_elig_eqc;
-
+  std::map< Node, Node > d_term_elig_eqc;  
+  /** set has term */
+  void setHasTerm( Node n );
+  /** evaluate term */
+  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
+  TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+  bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 public:
   /** ground terms for operator */
   unsigned getNumGroundTerms( Node f );
   /** get ground term for operator */
   Node getGroundTerm( Node f, unsigned i );
+  /** get num type terms */
+  unsigned getNumTypeGroundTerms( TypeNode tn );
+  /** get type ground term */
+  Node getTypeGroundTerm( TypeNode tn, unsigned i );
   /** add a term to the database */
   void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
-  /** presolve (called once per user check-sat) */
-  void presolve();
-  /** reset (calculate which terms are active) */
-  bool reset( Theory::Effort effort );
-  /** identify */
-  std::string identify() const { return "TermDb"; }
   /** get match operator */
   Node getMatchOperator( Node n );
   /** get term arg index */
@@ -238,6 +254,8 @@ public:
   void computeArgReps( TNode n );
   /** compute uf eqc terms */
   void computeUfEqcTerms( TNode f );
+  /** in relevant domain */
+  bool inRelevantDomain( TNode f, unsigned i, TNode r );
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
@@ -297,7 +315,7 @@ public:
   /** get the i^th instantiation constant of q */
   Node getInstantiationConstant( Node q, int i ) const;
   /** get number of instantiation constants for q */
-  int getNumInstantiationConstants( Node q ) const;
+  unsigned getNumInstantiationConstants( Node q ) const;
   /** get the ce body q[e/x] */
   Node getInstConstantBody( Node q );
   /** get counterexample literal (for cbqi) */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4b95c75ed..1008d7d49 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QEFFORT_NONE;
   d_conflict = false;
+  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_db->d_true] = true;
@@ -365,6 +366,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 
   d_conflict = false;
+  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -398,7 +400,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
-      Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
@@ -410,6 +411,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset utilities
+    Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
     for( unsigned i=0; i<d_util.size(); i++ ){
       Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
       if( !d_util[i]->reset( e ) ){
@@ -429,9 +431,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset the model
+    Trace("quant-engine-debug") << "Reset model..." << std::endl;
     d_model->reset_round();
 
     //reset the modules
+    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     for( unsigned i=0; i<d_modules.size(); i++ ){
       Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
       d_modules[i]->reset_round( e );
@@ -936,6 +940,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
       Trace("inst-add-debug") << "Added lemma" << std::endl;
+      d_num_added_lemmas_round++;
       return true;
     }else{
       Trace("inst-add-debug") << "Duplicate." << std::endl;
@@ -944,6 +949,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   }else{
     //do not need to rewrite, will be rewritten after sending
     d_lemmas_waiting.push_back( lem );
+    d_num_added_lemmas_round++;
     return true;
   }
 }
@@ -1115,6 +1121,14 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   }
 }
 
+bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
+  //lem must occur in d_waiting_lemmas
+  if( removeLemma( lem ) ){
+    return removeInstantiationInternal( q, terms );
+  }else{
+    return false;
+  }
+}
 
 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
   n = Rewriter::rewrite( n );
@@ -1134,16 +1148,10 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
-bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
-  //lem must occur in d_waiting_lemmas
-  if( removeLemma( lem ) ){
-    return removeInstantiationInternal( q, terms );
-  }else{
-    return false;
-  }
+void QuantifiersEngine::markRelevant( Node q ) {
+  d_model->markRelevant( q );
 }
 
-
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bad9c0169..a088dfec6 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -156,6 +156,8 @@ private:  //this information is reset during check
   unsigned d_curr_effort_level;
   /** are we in conflict */
   bool d_conflict;
+  /** number of lemmas we actually added this round (for debugging) */
+  unsigned d_num_added_lemmas_round;
   /** has added lemma this round */
   bool d_hasAddedLemma;
 private:
@@ -317,12 +319,16 @@ public:
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
+  /** mark relevant quantified formula, this will indicate it should be checked before the others */
+  void markRelevant( Node q );
   /** has added lemma */
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** is in conflict */
   bool inConflict() { return d_conflict; }
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
+  /** get number of waiting lemmas */
+  unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 784eaf677..b51313deb 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -77,7 +77,8 @@ TESTS =	\
 	anti-sk-simp.smt2 \
 	pure_dt_cbqi.smt2 \
 	florian-case-ax.smt2 \
-	double-pattern.smt2
+	double-pattern.smt2 \
+	qcf-rel-dom-opt.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
new file mode 100644
index 000000000..539f181af
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
@@ -0,0 +1,45 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+
+(assert (P 0))
+(assert (P 1))
+(assert (P 2))
+(assert (P 3))
+(assert (P 4))
+(assert (P 5))
+(assert (P 6))
+(assert (P 7))
+(assert (P 8))
+(assert (P 9))
+
+(assert (P 10))
+(assert (P 11))
+(assert (P 12))
+(assert (P 13))
+(assert (P 14))
+(assert (P 15))
+(assert (P 16))
+(assert (P 17))
+(assert (P 18))
+(assert (P 19))
+
+(assert (P 20))
+(assert (P 21))
+(assert (P 22))
+(assert (P 23))
+(assert (P 24))
+(assert (P 25))
+(assert (P 26))
+(assert (P 27))
+(assert (P 28))
+(assert (P 29))
+
+(declare-fun Q (Int Int Int Int Int) Bool)
+(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q))))
+
+(declare-fun R (Int) Bool)
+(assert (R 0))
+(assert (forall ((x Int)) (not (R x))))
+
+(check-sat)