diff options
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 4 |
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;
|