1 files changed, 13 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 75294621a..34704181c 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -133,7 +133,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
     : ContextNotifyObj(context),
-      d_masterEqualityEngine(0),
+      d_masterEqualityEngine(nullptr),
+      d_proofEqualityEngine(nullptr),
       d_context(context),
       d_done(context, false),
       d_notify(&s_notifyNone),
@@ -161,10 +162,20 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
 }
 
 void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
-  Assert(d_masterEqualityEngine == 0);
+  Assert(d_masterEqualityEngine == nullptr);
   d_masterEqualityEngine = master;
 }
 
+void EqualityEngine::setProofEqualityEngine(ProofEqEngine* pfee)
+{
+  Assert(d_proofEqualityEngine == nullptr);
+  d_proofEqualityEngine = pfee;
+}
+ProofEqEngine* EqualityEngine::getProofEqualityEngine()
+{
+  return d_proofEqualityEngine;
+}
+
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
   Debug("equality") << d_name << "::eq::enqueue({" << candidate.d_t1Id << "} "
                     << d_nodes[candidate.d_t1Id] << ", {" << candidate.d_t2Id