Merge branch 'master' into rmAliasesrmAliases

1 files changed, 0 insertions, 14 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 32a80a418..2c27c6054 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -266,7 +266,6 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
 }
 
 void TheoryEngine::finishInit() {
-
   //initialize the quantifiers engine, master equality engine, model, model builder
   if( d_logicInfo.isQuantified() ) {
     // initialize the quantifiers engine
@@ -350,7 +349,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_factsAsserted(context, false),
       d_preRegistrationVisitor(this, context),
       d_sharedTermsVisitor(d_sharedTerms),
-      d_theoryAlternatives(),
       d_attr_handle(),
       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 {
@@ -2374,18 +2372,6 @@ void TheoryEngine::spendResource(ResourceManager::Resource r)
   d_resourceManager->spendResource(r);
 }
 
-void TheoryEngine::enableTheoryAlternative(const std::string& name){
-  Debug("TheoryEngine::enableTheoryAlternative")
-      << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
-
-  d_theoryAlternatives.insert(name);
-}
-
-bool TheoryEngine::useTheoryAlternative(const std::string& name) {
-  return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
-}
-
-
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
     conflicts(getStatsPrefix(theory) + "::conflicts", 0),
     propagations(getStatsPrefix(theory) + "::propagations", 0),