Add --user-pat=interleave. Remove unused lte inst strategy.

1 files changed, 1 insertions, 8 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index e867aae1e..4fbf298f4 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
 
 }
 
 InstantiationEngine::~InstantiationEngine() {
   delete d_i_ag;
   delete d_isup;
-  delete d_i_lte;
   delete d_i_fs;
   delete d_i_splx;
   delete d_i_cegqi;
@@ -59,12 +58,6 @@ void InstantiationEngine::finishInit(){
     d_instStrategies.push_back( d_i_ag );
   }
 
-  //local theory extensions TODO?
-  //if( options::localTheoryExt() ){
-  //  d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
-  //  d_instStrategies.push_back( d_i_lte );
-  //}
-
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() ){
     d_i_fs = new InstStrategyFreeVariable( d_quantEngine );