Minor improvements for alpha equivalence and partial quantifier elimination in incremental mode. Change defaults to addInstantiation method.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index fe4867b4e..149330c61 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -648,12 +648,12 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true );
+    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
-    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ) ){
+    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
       //d_added_inst.insert( d_curr_quant );
       return true;
     }else{