Better combination of UF with cbqi, refactor quantifiers intialization.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index a1af1313d..26b598413 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -624,7 +624,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
   }
 
   if( !d_unassigned.empty() && ( success || doContinue ) ){
-    Trace("qcf-check") << "Assign to unassigned..." << std::endl;
+    Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
     do {
       if( doFail ){
         Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
@@ -702,6 +702,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
         }
       }
     }while( success && isMatchSpurious( p ) );
+    Trace("qcf-check") << "done assigning." << std::endl;
   }
   if( success ){
     for( unsigned i=0; i<d_unassigned.size(); i++ ){
@@ -2113,7 +2114,9 @@ void QuantConflictFind::computeRelevantEqr() {
             itt->second.push_back( r );
           }
         }else{
-          d_eqcs[rtn].push_back( r );
+          if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+            d_eqcs[rtn].push_back( r );
+          }
         }
       }
       ++eqcs_i;