Remove local theory extension option (#4048)

This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.

2 files changed, 0 insertions, 15 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e104101ef..6e0460ae9 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1926,15 +1926,6 @@ header = "options/quantifiers_options.h"
 ### Local theory extensions options
 
 [[option]]
-  name       = "localTheoryExt"
-  category   = "regular"
-  long       = "local-t-ext"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "do instantiation based on local theory extensions"
-
-[[option]]
   name       = "lteRestrictInstClosure"
   category   = "regular"
   long       = "lte-restrict-inst-closure"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fbc5821ce..5fc0189c3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1814,12 +1814,6 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  //local theory extensions
-  if( options::localTheoryExt() ){
-    if( !options::instMaxLevel.wasSetByUser() ){
-      options::instMaxLevel.set( 0 );
-    }
-  }
   if( options::instMaxLevel()!=-1 ){
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
     options::cbqi.set(false);