1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 1a47b3a02..ced4e1997 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1277,6 +1277,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
                 invalidMatch = true;
               }
             }else{
+              qi->d_match[ itb->second ] = TNode::null();
+              qi->d_match_term[ itb->second ] = TNode::null();
               Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
             }
           }else{
@@ -1898,6 +1900,7 @@ void QuantConflictFind::computeRelevantEqr() {
     }else{
       d_eqcs[rtn].push_back( r );
     }
+    /*
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
     while( !eqc_i.isFinished() ){
       TNode n = (*eqc_i);
@@ -1907,6 +1910,7 @@ void QuantConflictFind::computeRelevantEqr() {
       }
       ++eqc_i;
     }
+    */
 
     //if( r.getType().isInteger() ){
     //  Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;