diff options
| -rw-r--r-- | src/options/quantifiers_options.toml | 9 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
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); |