1 files changed, 17 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4b4316db1..cd3b34879 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,12 +42,26 @@
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 
+#include "theory/uf/equality_engine.h"
 
 using namespace std;
 
 using namespace CVC4;
 using namespace CVC4::theory;
 
+void TheoryEngine::finishInit() {
+  if (d_logicInfo.isQuantified()) {
+    Assert(d_masterEqualityEngine == 0);
+    d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master");
+
+    for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
+      if (d_theoryTable[theoryId]) {
+        d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
+      }
+    }
+  }
+}
+
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveITE& iteRemover,
@@ -58,6 +72,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_userContext(userContext),
   d_logicInfo(logicInfo),
   d_sharedTerms(this, context),
+  d_masterEqualityEngine(NULL),
   d_quantEngine(NULL),
   d_curr_model(NULL),
   d_curr_model_builder(NULL),
@@ -114,6 +129,8 @@ TheoryEngine::~TheoryEngine() {
 
   delete d_quantEngine;
 
+  delete d_masterEqualityEngine;
+
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
@@ -229,21 +246,6 @@ void TheoryEngine::dumpAssertions(const char* tag) {
   }
 }
 
-
-template<typename T, bool doAssert>
-class scoped_vector_clear {
-  vector<T>& d_v;
-public:
-  scoped_vector_clear(vector<T>& v)
-  : d_v(v) {
-    Assert(!doAssert || d_v.empty());
-  }
-  ~scoped_vector_clear() {
-    d_v.clear();
-  }
-
-};
-
 /**
  * Check all (currently-active) theories for conflicts.
  * @param effort the effort level to use