Remove local theory extension option (#4048)

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

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e104101efd00ba0b218e4fa2756fac5fb2419b16..6e0460ae9f725e39c5bebb83e56eb355a6cb7a16 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1925,15 +1925,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"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fbc5821ce232f107179640a53a993758afe8d6ae..5fc0189c33335be00f5715f24476401dd0cd3818 100644 (file)
--- 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);