More work on inst propagate. Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.

9 files changed, 419 insertions, 271 deletions

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index d4be58636..1dc6f6d50 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -103,8 +103,7 @@ TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& arg
   if( !t.isNull() ){
     return t;
   }else{
-    //TODO?
-    return TNode::null();
+    return d_func_map_trie[f].existsTerm( args );
   }
 }
 
@@ -118,6 +117,7 @@ Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& e
   Node ar = getUfRepresentative( a, exp );
   if( !ar.isNull() ){
     if( engine_has_a || getEngine()->hasTerm( ar ) ){
+      Trace("qip-eq") << "getRepresentativeExp " << a << " returns " << ar << std::endl;
       Assert( getEngine()->hasTerm( ar ) );
       Assert( getEngine()->getRepresentative( ar )==ar );
       return ar;
@@ -252,7 +252,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
       }
     }
   }
-  
+
   if( swap ){
     //swap
     Node temp_r = ar;
@@ -262,7 +262,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
 
   Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
   Assert( ar!=br );
-  
+
   std::vector< Node > exp_d;
   if( areDisequalExp( ar, br, exp_d ) ){
     if( pol ){
@@ -290,7 +290,7 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
       Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
       a = ar;
       b = br;
-      
+
       //carry disequality list
       std::map< Node, std::map< Node, std::vector< Node > > >::iterator itd = d_diseq_list.find( ar );
       if( itd!=d_diseq_list.end() ){
@@ -302,13 +302,13 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
           }
         }
       }
-      
+
       return status;
     }else{
       Trace("qip-eq") << "EqualityQueryInstProp::setEqual : disequal " << ar << " <> " << br << std::endl;
       Assert( d_diseq_list[ar].find( br )==d_diseq_list[ar].end() );
       Assert( d_diseq_list[br].find( ar )==d_diseq_list[br].end() );
-      
+
       merge_exp( d_diseq_list[ar][br], reason );
       merge_exp( d_diseq_list[br][ar], reason );
       return STATUS_NONE;
@@ -316,187 +316,215 @@ int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< No
   }
 }
 
-void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
-  if( is_prop ){
-    if( isLiteral( n ) ){
-      props.push_back( pol ? n : n.negate() );
-      return;
-    }
+//void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
+void EqualityQueryInstProp::addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ) {
+  if( is_watch ){
+    watch.push_back( n );
   }
   args.push_back( n );
 }
 
-bool EqualityQueryInstProp::isLiteral( Node n ) {
-  Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
-  Assert( ak!=NOT );
-  return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+bool EqualityQueryInstProp::isPropagateLiteral( Node n ) {
+  if( n==d_true || n==d_false ){
+    return false;
+  }else{
+    Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
+    Assert( ak!=NOT );
+    return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+  }
+}
+
+void EqualityQueryInstProp::setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out ) {
+  if( watch.empty() ){
+    watch.push_back( n );
+  }
+  for( unsigned j=0; j<watch.size(); j++ ){
+    Trace("qip-eval") << "Watch : " << n << " -> " << watch[j] << std::endl;
+    watch_list_out[n].push_back( watch[j] );
+  }
+}
+
+void EqualityQueryInstProp::collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list ) {
+  std::map< Node, std::vector< Node > >::iterator it = watch_list_out.find( n );
+  if( it!=watch_list_out.end() && std::find( watch_list.begin(), watch_list.end(), n )==watch_list.end() ){
+    watch_list.push_back( n );
+    for( unsigned j=0; j<it->second.size(); j++ ){
+      collectWatchList( it->second[j], watch_list_out, watch_list );
+    }
+  }
 }
 
-//this is identical to TermDb::evaluateTerm2, but tracks more information
-Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
-                                             std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) {
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  if( itv != visited.end() ){
+//this is similar to TermDb::evaluateTerm2, but tracks more information
+Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited,
+                                             bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props ) {
+  int polIndex = hasPol ? ( pol ? 1 : -1 ) : 0;
+  std::map< Node, Node >::iterator itv = visited[polIndex].find( n );
+  if( itv!=visited[polIndex].end() ){
     return itv->second;
   }else{
-    visited[n] = n;
-    Trace("qip-eval") << "evaluate term : " << n << std::endl;
-    std::vector< Node > exp_n;
-    Node ret = getRepresentativeExp( n, exp_n );
-    if( ret.isNull() ){
-      //term is not known to be equal to a representative in equality engine, evaluate it
-      Kind k = n.getKind();
-      if( k==FORALL ){
-        ret = Node::null();
-      }else{
-        std::map< Node, bool > watch_list_out_curr;
-        TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
-        std::vector< Node > args;
-        bool ret_set = false;
-        bool childChanged = false;
-        int abort_i = -1;
-        //get the child entailed polarity
-        Assert( n.getKind()!=IMPLIES );
-        bool newHasPol, newPol;
-        QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
-        //for each child
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );
-          if( c.isNull() ){
-            ret = Node::null();
-            ret_set = true;
-            break;
-          }else if( c==d_true || c==d_false ){
-            //short-circuiting
-            if( k==kind::AND || k==kind::OR ){
-              if( (k==kind::AND)==(c==d_false) ){
-                ret = c;
-                ret_set = true;
-                break;
-              }else{
-                //redundant
-                c = Node::null();
-                childChanged = true;
-              }
-            }else if( k==kind::ITE && i==0 ){
-              Assert( watch_list_out_curr.empty() );
-              ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );
-              ret_set = true;
-              break;
-            }else if( k==kind::NOT ){
-              ret = c==d_true ? d_false : d_true;
+    visited[polIndex][n] = n;
+    Node ret;
+    //check if it should be propagated in this context
+    if( hasPol && isPropagateLiteral( n ) ){
+      Assert( n.getType().isBoolean() );
+      //must be Boolean
+      ret = evaluateTermExp( n, exp, visited, false, pol, watch_list_out, props );
+      if( isPropagateLiteral( ret ) ){
+        Trace("qip-eval") << "-----> propagate : " << ret << std::endl;
+        props.push_back( pol ? ret : ret.negate() );
+        ret = pol ? d_true : d_false;
+      }
+    }else{
+      Trace("qip-eval") << "evaluate term : " << n << " [" << polIndex << "]" << std::endl;
+      std::vector< Node > exp_n;
+      ret = getRepresentativeExp( n, exp_n );
+      if( ret.isNull() ){
+        //term is not known to be equal to a representative in equality engine, evaluate it
+        Kind k = n.getKind();
+        if( k!=FORALL ){
+          TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+          std::vector< Node > args;
+          bool ret_set = false;
+          bool childChanged = false;
+          int abort_i = -1;
+          //get the child entailed polarity
+          Assert( n.getKind()!=IMPLIES );
+          bool newHasPol, newPol;
+          QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
+          std::vector< Node > watch;
+          //for each child
+          for( unsigned i=0; i<n.getNumChildren(); i++ ){
+            Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out, props );
+            if( c.isNull() ){
+              ret = Node::null();
               ret_set = true;
               break;
-            }
-          }
-          if( !c.isNull() ){
-            childChanged = childChanged || n[i]!=c;
-            if( !f.isNull() && !watch_list_out_curr.empty() ){
-              // we are done if this is an UF application and an argument is unevaluated
-              args.push_back( c );
-              abort_i = i;
-              break;
-            }else if( ( k==kind::AND || k==kind::OR ) ){
-              if( c.getKind()==k ){
-                //flatten
-                for( unsigned j=0; j<c.getNumChildren(); j++ ){
-                  addArgument( args, props, c[j], newHasPol, newPol );
+            }else if( c==d_true || c==d_false ){
+              //short-circuiting
+              if( k==kind::AND || k==kind::OR ){
+                if( (k==kind::AND)==(c==d_false) ){
+                  ret = c;
+                  ret_set = true;
+                  break;
+                }else{
+                  //redundant
+                  c = Node::null();
+                  childChanged = true;
                 }
-              }else{
-                addArgument( args, props, c, newHasPol, newPol );
+              }else if( k==kind::ITE && i==0 ){
+                ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out, props );
+                ret_set = true;
+                break;
+              }else if( k==kind::NOT ){
+                ret = c==d_true ? d_false : d_true;
+                ret_set = true;
+                break;
               }
-              //if we are in a branching position
-              if( hasPol && !newHasPol && args.size()>=2 ){
-                //we are done if at least two args are unevaluated
+            }
+            if( !c.isNull() ){
+              childChanged = childChanged || n[i]!=c;
+              bool is_watch = watch_list_out.find( c )!=watch_list_out.end();
+              if( !f.isNull() && is_watch ){
+                // we are done if this is an UF application and an argument is unevaluated
+                addArgument( c, args, watch, is_watch );
                 abort_i = i;
                 break;
+              }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){
+                Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl;
+                if( ( k==kind::AND || k==kind::OR  ) && c.getKind()==k ){
+                  //flatten
+                  for( unsigned j=0; j<c.getNumChildren(); j++ ){
+                    addArgument( c[j], args, watch, is_watch );
+                  }
+                }else{
+                  addArgument( c, args, watch, is_watch );
+                }
+                Trace("qip-eval-debug") << "props/args = " << props.size() << "/" << args.size() << std::endl;
+                //if we are in a branching position
+                if( hasPol && !newHasPol && args.size()>=2 ){
+                  //we are done if at least two args are unevaluated
+                  abort_i = i;
+                  break;
+                }
+              }else{
+                addArgument( c, args, watch, is_watch );
               }
-            }else if( k==kind::ITE ){
-              //we are done if we are ITE and condition is unevaluated
-              Assert( i==0 );
-              args.push_back( c );
-              abort_i = i;
-              break;
-            }else{
-              args.push_back( c );
             }
           }
-        }
-        //add remaining children if we aborted
-        if( abort_i!=-1 ){
-          for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
-            args.push_back( n[i] );
-          }
-        }
-        //copy over the watch list
-        for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){
-          watch_list_out[itc->first] = itc->second;
-        }
-
-        //if we have not short-circuited evaluation
-        if( !ret_set ){
-          //if it is an indexed term, return the congruent term
-          if( !f.isNull() && watch_list_out.empty() ){
-            std::vector< TNode > t_args;
-            for( unsigned i=0; i<args.size(); i++ ) {
-              t_args.push_back( args[i] );
-            }
-            Assert( args.size()==n.getNumChildren() );
-            //args contains terms known by the equality engine
-            TNode nn = getCongruentTerm( f, t_args );
-            Trace("qip-eval") << "  got congruent term " << nn << " from DB for " << n << std::endl;
-            if( !nn.isNull() ){
-              //successfully constructed representative in EE
-              Assert( exp_n.empty() );
-              ret = getRepresentativeExp( nn, exp_n );
-              Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
-              merge_exp( exp, exp_n );
-              ret_set = true;
-              Assert( !ret.isNull() );
+          //add remaining children if we aborted
+          if( abort_i!=-1 ){
+            Trace("qip-eval-debug") << "..." << n << " aborted at " << abort_i << std::endl;
+            for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
+              args.push_back( n[i] );
             }
           }
+          //if we have not short-circuited evaluation
           if( !ret_set ){
-            if( childChanged ){
-              Trace("qip-eval") << "return rewrite" << std::endl;
-              if( ( k==kind::AND || k==kind::OR ) ){
-                if( args.empty() ){
-                  ret = k==kind::AND ? d_true : d_false;
-                  ret_set = true;
-                }else if( args.size()==1 ){
-                  ret = args[0];
-                  ret_set = true;
-                }
+            //if it is an indexed term, return the congruent term
+            if( !f.isNull() && watch.empty() ){
+              std::vector< TNode > t_args;
+              for( unsigned i=0; i<args.size(); i++ ) {
+                Trace("qip-eval") << "arg " << i << " : " << args[i] << std::endl;
+                t_args.push_back( args[i] );
+              }
+              Assert( args.size()==n.getNumChildren() );
+              //args contains terms known by the equality engine
+              TNode nn = getCongruentTerm( f, t_args );
+              Trace("qip-eval") << "  got congruent term " << nn << " for " << n << std::endl;
+              if( !nn.isNull() ){
+                //successfully constructed representative in EE
+                Assert( exp_n.empty() );
+                ret = getRepresentativeExp( nn, exp_n );
+                Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
+                merge_exp( exp, exp_n );
+                ret_set = true;
+                Assert( !ret.isNull() );
+                Assert( ret!=n );
+                // we have that n == ret, check if the union find should be updated TODO?
               }else{
-                Assert( args.size()==n.getNumChildren() );
+                watch.push_back( ret );
               }
-              if( !ret_set ){
-                if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-                  args.insert( args.begin(), n.getOperator() );
+            }
+            if( !ret_set ){
+              if( childChanged || args.size()!=n.getNumChildren() ){
+                Trace("qip-eval") << "return rewrite" << std::endl;
+                if( k==kind::AND || k==kind::OR ){
+                  if( args.empty() ){
+                    ret = k==kind::AND ? d_true : d_false;
+                    ret_set = true;
+                  }else if( args.size()==1 ){
+                    //need to re-evaluate (may be new propagations)
+                    ret = evaluateTermExp( args[0], exp, visited, hasPol, pol, watch_list_out, props );
+                    ret_set = true;
+                  }
+                }else{
+                  Assert( args.size()==n.getNumChildren() );
                 }
-                ret = NodeManager::currentNM()->mkNode( k, args );
-                ret = Rewriter::rewrite( ret );
-                //re-evaluate
-                Node ret_eval = getRepresentativeExp( ret, exp_n );
-                if( !ret_eval.isNull() ){
-                  ret = ret_eval;
-                  watch_list_out.clear();
-                }else{            
-                  watch_list_out[ret] = true;
+                if( !ret_set ){
+                  if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+                    args.insert( args.begin(), n.getOperator() );
+                  }
+                  ret = NodeManager::currentNM()->mkNode( k, args );
+                  setWatchList( ret, watch, watch_list_out );
+                  ret = Rewriter::rewrite( ret );
+                  //need to re-evaluate
+                  ret = evaluateTermExp( ret, exp, visited, hasPol, pol, watch_list_out, props );
                 }
+              }else{
+                ret = n;
+                setWatchList( ret, watch, watch_list_out );
               }
-            }else{
-              ret = n;
-              watch_list_out[ret] = true;
             }
           }
         }
+      }else{
+        Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
+        merge_exp( exp, exp_n );
       }
-    }else{
-      Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
-      merge_exp( exp, exp_n );
     }
-    Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;
-    visited[n] = ret;
+
+    Trace("qip-eval") << "evaluated term : " << n << " [" << polIndex << "], got : " << ret << ", exp size = " << exp.size() << ", watch list size = " << watch_list_out.size() << std::endl;
+    visited[polIndex][n] = ret;
     return ret;
   }
 }
@@ -556,10 +584,7 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st
         Trace("qip-prop") << "  " << terms[i] << std::endl;
       }
     }
-    unsigned id = d_icount;
-    d_icount++;
-    Trace("qip-prop") << "...assign id=" << id << std::endl;
-    d_ii[id].init( q, lem, terms, body );
+    unsigned id = allocateInstantiation( q, lem, terms, body );
     //initialize the information
     if( cacheConclusion( id, body ) ){
       Assert( d_update_list.empty() );
@@ -586,31 +611,39 @@ bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, st
   }
 }
 
+unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) {
+  unsigned id = d_icount;
+  d_icount++;
+  Trace("qip-prop") << "...assign id=" << id << std::endl;
+  d_ii[id].init( q, lem, terms, body );
+  return id;
+}
+
 bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
   Assert( !d_conflict );
   Assert( ii.d_active );
   Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
   //update the evaluation of the current lemma
-  std::map< Node, Node > visited;
-  std::map< Node, bool > watch_list;
+  std::map< Node, std::vector< Node > > watch_list_out;
+  std::map< int, std::map< Node, Node > > visited;
+  std::vector< Node > exp;
   std::vector< Node > props;
-  Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );
+  Node eval = d_qy.evaluateTermExp( ii.d_curr, exp, visited, true, true, watch_list_out, props );
+  EqualityQueryInstProp::merge_exp( ii.d_curr_exp, exp );
   if( eval.isNull() ){
     ii.d_active = false;
   }else if( firstTime || eval!=ii.d_curr ){
-    if( EqualityQueryInstProp::isLiteral( eval ) ){
-      props.push_back( eval );
-      eval = d_qy.d_true;
-      watch_list.clear();
-    }
+    std::vector< Node > watch_list;
+    d_qy.collectWatchList( eval, watch_list_out, watch_list );
     if( Trace.isOn("qip-prop") ){
       Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
-      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";
+      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << std::endl; 
+      Trace("qip-prop") << "...explanation = ";
       debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
       Trace("qip-prop") << std::endl;
       Trace("qip-prop") << "...watch list: " << std::endl;
-      for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){
-        Trace("qip-prop") << "  " << itw->first << std::endl;
+      for( unsigned i=0; i<watch_list.size(); i++ ){
+        Trace("qip-prop") << "  " << watch_list[i] << std::endl;
       }
       Trace("qip-prop") << "...new propagations: " << std::endl;
       for( unsigned i=0; i<props.size(); i++ ){
@@ -627,8 +660,13 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
     }else{
       for( unsigned i=0; i<props.size(); i++ ){
         Trace("qip-prop-debug2")  << "Process propagation " << props[i] << std::endl;
+        Assert( d_qy.isPropagateLiteral( props[i] ) );
         //if we haven't propagated this literal yet
         if( cacheConclusion( id, props[i], 1 ) ){
+          //watch list for propagated literal: may not yet be purely EE representatives
+          std::vector< Node > prop_watch_list;
+          d_qy.collectWatchList( props[i], watch_list_out, prop_watch_list );
+        
           Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
           bool pol = props[i].getKind()!=NOT;
           if( lit.getKind()==EQUAL ){
@@ -647,10 +685,10 @@ bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
         ii.d_curr = eval;
         //update the watch list
         Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
-        //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.
-        //  Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.
-        for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){
-          d_watch_list[ itw->first ][ id ] = true;
+        //Here, we need to be notified of enough terms such that if we are not notified, then update( id, ii ) will return no propagations.
+        //  Similar to two-watched literals, but since we are taking into account UF, we need to watch all terms on a complete path of two terms.
+        for( unsigned i=0; i<watch_list.size(); i++ ){
+          d_watch_list[ watch_list[i] ][ id ] = true;
         }
       }else{
         Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl;
@@ -716,16 +754,18 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
   //now, inform quantifiers engine which instances should be retracted
   Trace("qip-prop-debug") << "...remove instantiation ids : ";
   for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
-    if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
-      if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
-        Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
-        Assert( false );
+    if( !it->second.d_q.isNull() ){
+      if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
+        if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+          Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
+          Assert( false );
+        }else{
+          Trace("qip-prop-debug") << it->first << " ";
+        }
       }else{
-        Trace("qip-prop-debug") << it->first << " ";
+        //mark the quantified formula as relevant
+        d_qe->markRelevant( it->second.d_q );
       }
-    }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_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 0c02c7f95..61aa8257f 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -74,7 +74,7 @@ private:
   /** disequality list, stores explanations */
   std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
   /** add arg */
-  void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol );
+  void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
 public:
   enum {
     STATUS_CONFLICT,
@@ -89,10 +89,13 @@ public:
 public:
   //for explanations
   static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
+  //for watch list
+  static void setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out );
+  static void collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list );
 
-  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
-                        std::map< Node, bool >& watch_list_out, std::vector< Node >& props );
-  static bool isLiteral( Node n );
+  Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited,
+                        bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props );
+  bool isPropagateLiteral( Node n );
 };
 
 class InstPropagator : public QuantifiersUtil {
@@ -104,13 +107,15 @@ private:
     InstPropagator& d_ip;
   public:
     InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
-    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { 
-      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); 
+    virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+      return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
     }
   };
   InstantiationNotifyInstPropagator d_notify;
   /** notify instantiation method */
   bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+  /** allocate instantiation */
+  unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body );
   /** equality query */
   EqualityQueryInstProp d_qy;
   class InstInfo {
@@ -143,7 +148,6 @@ private:
   void conflict( std::vector< Node >& exp );
   bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
   void addRelevantInstances( std::vector< Node >& exp, const char * c );
-
   void debugPrintExplanation( std::vector< Node >& exp, const char * c );
 public:
   InstPropagator( QuantifiersEngine* qe );
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ca87a607d..52563978f 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -49,6 +49,7 @@ QuantInfo::~QuantInfo() {
 
 void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_q = q;
+  d_extra_var = 0;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_match.push_back( TNode::null() );
     d_match_term.push_back( TNode::null() );
@@ -77,32 +78,30 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
       }
     }
     */
-    if( d_mg->isValid() ){
-      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
-        if( d_vars[j].getKind()!=BOUND_VARIABLE ){
-          d_var_mg[j] = NULL;
-          bool is_tsym = false;
-          if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
-            is_tsym = true;
-            d_tsym_vars.push_back( j );
-          }
-          if( !is_tsym || options::qcfTConstraint() ){
-            d_var_mg[j] = new MatchGen( this, d_vars[j], true );
-          }
-          if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
-            Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
-            d_mg->setInvalid();
-            break;
-          }else{
-            std::vector< int > bvars;
-            d_var_mg[j]->determineVariableOrder( this, bvars );
-          }
+    for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+      if( d_vars[j].getKind()!=BOUND_VARIABLE ){
+        d_var_mg[j] = NULL;
+        bool is_tsym = false;
+        if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
+          is_tsym = true;
+          d_tsym_vars.push_back( j );
+        }
+        if( !is_tsym || options::qcfTConstraint() ){
+          d_var_mg[j] = new MatchGen( this, d_vars[j], true );
+        }
+        if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
+          Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
+          d_mg->setInvalid();
+          break;
+        }else{
+          std::vector< int > bvars;
+          d_var_mg[j]->determineVariableOrder( this, bvars );
         }
       }
-      if( d_mg->isValid() ){
-        std::vector< int > bvars;
-        d_mg->determineVariableOrder( this, bvars );
-      }
+    }
+    if( d_mg->isValid() ){
+      std::vector< int > bvars;
+      d_mg->determineVariableOrder( this, bvars );
     }
   }else{
     Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
@@ -163,6 +162,10 @@ void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol,
   }
 }
 
+bool QuantInfo::isBaseMatchComplete() {
+  return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var);
+}
+
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
   Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
   if( n.getKind()==FORALL ){
@@ -219,6 +222,8 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
       d_match_term.push_back( TNode::null() );
       if( n.getKind()==ITE ){
         registerNode( n, false, false );
+      }else if( n.getKind()==BOUND_VARIABLE ){
+        d_extra_var++;
       }else{
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           flatten( n[i], beneathQuant );
@@ -238,6 +243,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) {
     d_match[i] = TNode::null();
     d_match_term[i] = TNode::null();
   }
+  d_vars_set.clear();
   d_curr_var_deq.clear();
   d_tconstraints.clear();
   //add built-in variable constraints
@@ -377,11 +383,12 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
             }
           }
         }
-        d_match[v] = TNode::null();
+        unsetMatch( p, v );
         return 1;
       }else{
         //std::map< int, TNode >::iterator itm = d_match.find( v );
         bool isGroundRep = false;
+        bool isGround = false;
         if( vn!=-1 ){
           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
           //std::map< int, TNode >::iterator itmn = d_match.find( vn );
@@ -428,13 +435,14 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
           Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
           if( d_match[v].isNull() ){
             //isGroundRep = true;   ??
+            isGround = 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, isGroundRep ) ){
+        if( setMatch( p, v, n, isGroundRep, isGround ) ){
           Debug("qcf-match-debug") << "  -> success" << std::endl;
           return 1;
         }else{
@@ -500,7 +508,7 @@ bool QuantInfo::isConstrainedVar( int v ) {
   }
 }
 
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround ) {
   if( getCurrentCanBeEqual( p, v, n ) ){
     if( isGroundRep ){
       //fail if n does not exist in the relevant domain of each of the argument positions
@@ -518,6 +526,12 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe
       }
     }
     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
+    if( isGround ){
+      if( d_vars[v].getKind()==BOUND_VARIABLE ){
+        d_vars_set[v] = true;
+        Debug("qcf-match-debug") << "---- now bound " << d_vars_set.size() << " / " << d_q[0].getNumChildren() << " base variables." << std::endl;
+      }
+    }
     d_match[v] = n;
     return true;
   }else{
@@ -525,6 +539,14 @@ bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRe
   }
 }
 
+void QuantInfo::unsetMatch( QuantConflictFind * p, int v ) {
+  Debug("qcf-match-debug") << "-- unbind : " << v << std::endl;
+  if( d_vars[v].getKind()==BOUND_VARIABLE && d_vars_set.find( v )!=d_vars_set.end() ){
+    d_vars_set.erase( v );
+  }
+  d_match[ v ] = TNode::null();
+}
+
 bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   for( int i=0; i<getNumVars(); i++ ){
     //std::map< int, TNode >::iterator it = d_match.find( i );
@@ -538,6 +560,37 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
 }
 
 bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
+  if( options::qcfEagerTest() ){
+    //check whether the instantiation evaluates as expected
+    if( p->d_effort==QuantConflictFind::effort_conflict ){
+      Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
+      std::map< TNode, TNode > subs;
+      for( unsigned i=0; i<terms.size(); i++ ){
+        Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
+        subs[d_q[0][i]] = terms[i];
+      }
+      if( !p->getTermDatabase()->isEntailed( d_q[1], subs, false, false ) ){
+        Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
+        return true;
+      }
+    }else{
+      Node inst = p->d_quantEngine->getInstantiation( d_q, terms );
+      Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() );
+      if( Trace.isOn("qcf-instance-check") ){
+        Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
+        for( unsigned i=0; i<terms.size(); i++ ){
+          Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
+        }
+        Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
+      }
+      if( inst_eval.isNull() || inst_eval==p->getTermDatabase()->d_true || !isPropagatingInstance( p, inst_eval ) ){
+        Trace("qcf-instance-check") << "...spurious." << std::endl;
+        return true;
+      }else{
+        Trace("qcf-instance-check") << "...not spurious." << std::endl;
+      }
+    }
+  }
   if( !d_tconstraints.empty() ){
     //check constraints
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
@@ -552,6 +605,25 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
   return false;
 }
 
+bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) {
+  if( n.getKind()==FORALL ){
+    return true;
+  }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !isPropagatingInstance( p, n[i] ) ){
+        return false;
+      }
+    }
+    return true;
+  }else{
+    if( p->getEqualityEngine()->hasTerm( n ) || isGroundSubterm( n ) ){
+      return true;
+    }
+  }
+  Trace("qcf-instance-check-debug") << "...not propagating instance because of " << n << std::endl;
+  return false;
+}
+
 bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
   Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
   Node rew = Rewriter::rewrite( lit );
@@ -606,6 +678,9 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     doFail = true;
     success = false;
   }else{
+    if( isBaseMatchComplete() && options::qcfEagerTest() ){
+      return true;
+    }
     //solve for interpreted symbol matches
     //   this breaks the invariant that all introduced constraints are over existing terms
     for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
@@ -636,7 +711,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, false ) ){
+                  if( !setMatch( p, vn, z, false, true ) ){
                     success = false;
                     break;
                   }
@@ -678,7 +753,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, false ) ){
+              if( !setMatch( p, slv_v, sum, false, true ) ){
                 success = false;
               }
               p->d_tempCache.push_back( sum );
@@ -764,7 +839,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], true ) ){
+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true, 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++;
@@ -813,9 +888,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
     }
     return true;
   }else{
-    for( unsigned i=0; i<assigned.size(); i++ ){
-      d_match[ assigned[i] ] = TNode::null();
-    }
+    revertMatch( p, assigned );
     assigned.clear();
     return false;
   }
@@ -837,9 +910,9 @@ void QuantInfo::getMatch( std::vector< Node >& terms ){
   }
 }
 
-void QuantInfo::revertMatch( std::vector< int >& assigned ) {
+void QuantInfo::revertMatch( QuantConflictFind * p, std::vector< int >& assigned ) {
   for( unsigned i=0; i<assigned.size(); i++ ){
-    d_match[ assigned[i] ] = TNode::null();
+    unsetMatch( p, assigned[i] );
   }
 }
 
@@ -1003,6 +1076,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
               }
             }else{
               d_qni_gterm[i] = d_n[i];
+              qi->setGroundSubterm( d_n[i] );
             }
           }
           d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
@@ -1013,6 +1087,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
       //we will just evaluate
       d_n = n;
       d_type = typ_ground;
+      qi->setGroundSubterm( d_n );
     }
     //if( d_type!=typ_invalid ){
       //determine an efficient children ordering
@@ -1169,15 +1244,20 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
   d_qni.clear();
   d_qni_bound.clear();
   d_child_counter = -1;
+  d_use_children = true;
   d_tgt_orig = d_tgt;
 
   //set up processing matches
   if( d_type==typ_invalid ){
-    //do nothing
+    d_use_children = false;
   }else if( d_type==typ_ground ){
+    d_use_children = false;
     if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
       d_child_counter = 0;
     }
+  }else if( qi->isBaseMatchComplete() && options::qcfEagerTest() ){
+    d_use_children = false;
+    d_child_counter = 0;
   }else if( d_type==typ_bool_var ){
     //get current value of the variable
     TNode n = qi->getCurrentValue( d_n );
@@ -1195,7 +1275,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, false );
+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false, true );
       d_child_counter = 0;
     }
     if( d_child_counter==0 ){
@@ -1309,7 +1389,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
   Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";
   debugPrintType( "qcf-match", d_type );
   Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
-  if( d_type==typ_invalid || d_type==typ_ground ){
+  if( !d_use_children ){
     if( d_child_counter==0 ){
       d_child_counter = -1;
       return true;
@@ -1423,7 +1503,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
         for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
           Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;
           Assert( it->second<qi->getNumVars() );
-          qi->d_match[ it->second ] = TNode::null();
+          qi->unsetMatch( p, it->second );
           qi->d_match_term[ it->second ] = TNode::null();
         }
         d_qni_bound.clear();
@@ -1654,7 +1734,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, true ) ){
+                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true, true ) ){
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;
                   if( d_qn.size()<d_qni_size ){
                     d_qn.push_back( &it->second );
@@ -1699,7 +1779,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, true ) ){
+              if( qi->setMatch( p, itb->second, d_qni[index]->first, true, 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 );
@@ -1709,7 +1789,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
                 invalidMatch = true;
               }
             }else{
-              qi->d_match[ itb->second ] = TNode::null();
+              qi->unsetMatch( p, itb->second );
               qi->d_match_term[ itb->second ] = TNode::null();
               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
             }
@@ -1991,12 +2071,13 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
               Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
               qi->debugPrintMatch("qcf-inst");
               Trace("qcf-inst") << std::endl;
-              std::vector< int > assigned;
               if( !qi->isMatchSpurious( this ) ){
+                std::vector< int > assigned;
                 if( qi->completeMatch( this, assigned ) ){
                   std::vector< Node > terms;
                   qi->getMatch( terms );
-                  if( !qi->isTConstraintSpurious( this, terms ) ){
+                  bool tcs = qi->isTConstraintSpurious( this, terms );
+                  if( !tcs ){
                     //for debugging
                     if( Debug.isOn("qcf-check-inst") ){
                       Node inst = d_quantEngine->getInstantiation( q, terms );
@@ -2029,9 +2110,11 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       //in this case, break to avoid exponential behavior
                       break;
                     }
+                  }else{
+                    Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
                   }
                   //clean up assigned
-                  qi->revertMatch( assigned );
+                  qi->revertMatch( this, assigned );
                   d_tempCache.clear();
                 }else{
                   Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 8b42b0916..16f6b6a1b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -35,6 +35,7 @@ class MatchGen {
 private:
   //current children information
   int d_child_counter;
+  bool d_use_children;
   //children of this object
   std::vector< int > d_children_order;
   unsigned getNumChildren() { return d_children.size(); }
@@ -117,6 +118,15 @@ private: //for completing match
   //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 );
+  //optimization: number of variables set, to track when we can stop
+  std::map< int, bool > d_vars_set;
+  std::map< Node, bool > d_ground_terms;
+  unsigned d_extra_var;
+public:
+  void setGroundSubterm( Node t ) { d_ground_terms[t] = true; }
+  bool isGroundSubterm( Node t ) { return d_ground_terms.find( t )!=d_ground_terms.end(); }
+  bool isBaseMatchComplete();
+  bool isPropagatingInstance( QuantConflictFind * p, Node n );
 public:
   QuantInfo();
   ~QuantInfo();
@@ -161,12 +171,13 @@ 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 isGroundRep );
+  bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround );
+  void unsetMatch( QuantConflictFind * p, int v );
   bool isMatchSpurious( QuantConflictFind * p );
   bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
   bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
-  void revertMatch( std::vector< int >& assigned );
+  void revertMatch( QuantConflictFind * p, std::vector< int >& assigned );
   void debugPrintMatch( const char * c );
   bool isConstrainedVar( int v );
 public:
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 3b7787a20..437f1bddf 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -33,22 +33,15 @@ eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
 }
 
 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
+  return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
 }
 
 bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
+  return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
 }
 
 TNode QuantifiersModule::getRepresentative( TNode n ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  if( ee->hasTerm( n ) ){
-    return ee->getRepresentative( n );
-  }else{
-    return n;
-  }
+  return d_quantEngine->getEqualityQuery()->getRepresentative( n );
 }
 
 quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8b09d8e5d..4dcf0e248 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -237,25 +237,23 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
 
 //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 ) {
+Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) {
   std::map< TNode, Node >::iterator itv = visited.find( n );
   if( itv != visited.end() ){
     return itv->second;
   }
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  Node ret;
-  if( n.getKind()==BOUND_VARIABLE ){
-    return n;
+  Node ret = n;
+  if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
+    //do nothing
   }else if( !qy->hasTerm( n ) ){
     //term is not known to be equal to a representative in equality engine, evaluate it
-    if( n.getKind()==FORALL ){
-      ret = Node::null();
-    }else if( n.hasOperator() ){
+    if( n.hasOperator() ){
       TNode f = getMatchOperator( n );
       std::vector< TNode > args;
       bool ret_set = false;
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        TNode c = evaluateTerm2( n[i], visited, qy );
+        TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests );
         if( c.isNull() ){
           ret = Node::null();
           ret_set = true;
@@ -267,7 +265,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ
             ret_set = true;
             break;
           }else if( n.getKind()==kind::ITE && i==0 ){
-            ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy ); 
+            ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); 
             ret_set = true;
             break;
           }
@@ -295,6 +293,22 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ
           }
           ret = NodeManager::currentNM()->mkNode( n.getKind(), args );
           ret = Rewriter::rewrite( ret );
+          if( ret.getKind()==kind::EQUAL ){
+            if( qy->areDisequal( ret[0], ret[1] ) ){
+              ret = d_false;
+            }
+          }
+          if( useEntailmentTests ){
+            if( ret.getKind()==kind::EQUAL || ret.getKind()==kind::GEQ ){
+              for( unsigned j=0; j<2; j++ ){
+                std::pair<bool, Node> et = d_quantEngine->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, j==0 ? ret : ret.negate() );
+                if( et.first ){
+                  ret = j==0 ? d_true : d_false;
+                  break;
+                }
+              }
+            }
+          }
         }
       }
     }
@@ -355,12 +369,12 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
   return TNode::null();
 }
 
-Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) {
+Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) {
   if( qy==NULL ){
     qy = d_quantEngine->getEqualityQuery();
   }
   std::map< TNode, Node > visited;
-  return evaluateTerm2( n, visited, qy );
+  return evaluateTerm2( n, visited, qy, useEntailmentTests );
 }
 
 TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index a62b343a2..266d9b8fa 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -228,7 +228,7 @@ private:
   /** set has term */
   void setHasTerm( Node n );
   /** evaluate term */
-  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
+  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
   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:
@@ -259,7 +259,7 @@ public:
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
-  Node evaluateTerm( TNode n, EqualityQuery * qy = NULL );
+  Node evaluateTerm( TNode n, EqualityQuery * qy = NULL, bool useEntailmentTests = false );
   /** get entailed term, does not construct new terms, less aggressive */
   TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL );
   TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6d3b17254..2451036f1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -57,6 +57,7 @@ using namespace CVC4::theory::inst;
 
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
     d_te( te ),
+    d_conflict_c(c, false),
     //d_quants(u),
     d_quants_red(u),
     d_lemmas_produced_c(u),
@@ -380,6 +381,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
+    //this will fail if a set of instances is marked as a conflict, but is not
+    Assert( !d_conflict_c.get() );
     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
     flushLemmas();
     if( d_hasAddedLemma ){
@@ -1122,6 +1125,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
         if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
           Trace("inst-add-debug") << "...we are in conflict." << std::endl;
           d_conflict = true;
+          d_conflict_c = true;
           Assert( !d_lemmas_waiting.empty() );
           break;
         }
@@ -1403,7 +1407,7 @@ bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
       Trace("quant-engine-ee-proc") << "      explanation : " << eq_exp << std::endl;
       Assert( ee->hasTerm( eq[0] ) );
       Assert( ee->hasTerm( eq[1] ) );
-      if( ee->areDisequal( eq[0], eq[1], false ) ){
+      if( areDisequal( eq[0], eq[1] ) ){
         Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
         if( Trace.isOn("term-db-lemma") ){
           Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
@@ -1445,11 +1449,10 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
   }else{
     eq::EqualityEngine* ee = getEngine();
     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areEqual( a, b ) ){
-        return true;
-      }
+      return ee->areEqual( a, b );
+    }else{
+      return false;
     }
-    return false;
   }
 }
 
@@ -1459,11 +1462,10 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
   }else{
     eq::EqualityEngine* ee = getEngine();
     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-      if( ee->areDisequal( a, b, false ) ){
-        return true;
-      }
+      return ee->areDisequal( a, b, false );
+    }else{
+      return a.isConst() && b.isConst();
     }
-    return false;
   }
 }
 
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4ee66f9e7..4c7cb4a2f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -156,6 +156,7 @@ private:  //this information is reset during check
   unsigned d_curr_effort_level;
   /** are we in conflict */
   bool d_conflict;
+  context::CDO< bool > d_conflict_c;
   /** number of lemmas we actually added this round (for debugging) */
   unsigned d_num_added_lemmas_round;
   /** has added lemma this round */