Refactor array-proofs and uf-proofs (#1655)

This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.

10 files changed, 1005 insertions, 850 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 89221dc69..3da7efd2e 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -643,6 +643,7 @@ ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
   : TheoryProof(arith, pe), d_realMode(false)
 {}
 
+theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; }
 void ArithProof::registerTerm(Expr term) {
   Debug("pf::arith") << "Arith register term: " << term << ". Kind: " << term.getKind()
                             << ". Type: " << term.getType() << std::endl;
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 677952bf7..2052adeac 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -63,8 +63,9 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
 
   bool d_realMode;
+  theory::TheoryId getTheoryId();
 
-public:
+ public:
   ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);
 
   void registerTerm(Expr term) override;
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index b0290fb3e..96197bb00 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -59,61 +59,7 @@ std::string ArrayProofPrinter::printTag(unsigned tag) {
 
 }  // namespace
 
-inline static Node eqNode(TNode n1, TNode n2) {
-  return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
-}
-
-// congrence matching term helper
-inline static bool match(TNode n1, TNode n2) {
-  Debug("mgd") << "match " << n1 << " " << n2 << std::endl;
-  if(ProofManager::currentPM()->hasOp(n1)) {
-    n1 = ProofManager::currentPM()->lookupOp(n1);
-  }
-  if(ProofManager::currentPM()->hasOp(n2)) {
-    n2 = ProofManager::currentPM()->lookupOp(n2);
-  }
-  Debug("mgd") << "+ match " << n1 << " " << n2 << std::endl;
-  Debug("pf::array") << "+ match: step 1" << std::endl;
-  if(n1 == n2) {
-    return true;
-  }
-
-  if(n1.getType().isFunction() && n2.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
-      return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator());
-    } else {
-      return n1 == n2.getOperator();
-    }
-  }
-
-  if(n2.getType().isFunction() && n1.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
-      return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator());
-    } else {
-      return n2 == n1.getOperator();
-    }
-  }
-
-  if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) {
-    if (!((n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_0) ||
-          (n1.getKind() == kind::SELECT && n2.getKind() == kind::PARTIAL_SELECT_1) ||
-          (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::SELECT) ||
-          (n1.getKind() == kind::PARTIAL_SELECT_1 && n2.getKind() == kind::PARTIAL_SELECT_0) ||
-          (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::SELECT) ||
-          (n1.getKind() == kind::PARTIAL_SELECT_0 && n2.getKind() == kind::PARTIAL_SELECT_1)
-          )) {
-      return false;
-    }
-  }
-
-  for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) {
-    if(n1[i] != n2[i]) {
-      return false;
-    }
-  }
 
-  return true;
-}
 
 ProofArray::ProofArray(std::shared_ptr<theory::eq::EqProof> pf,
                        unsigned row,
@@ -160,131 +106,19 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                      << "toStreamRecLFSC called. tb = " << tb
                      << " . proof:" << std::endl;
   ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt);
-  pf.debug_print("pf::array", 0, &proofPrinter);
-  Debug("pf::array") << std::endl;
-
   if(tb == 0) {
-    Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.size() >= 2);
-
-    int neg = -1;
     std::shared_ptr<theory::eq::EqProof> subTrans =
         std::make_shared<theory::eq::EqProof>();
-    subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
-    subTrans->d_node = pf.d_node;
 
-    size_t i = 0;
-    while (i < pf.d_children.size()) {
-      if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
-        pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
-
-      // Look for the negative clause, with which we will form a contradiction.
-      if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) {
-        Assert(neg < 0);
-        neg = i;
-        ++i;
-      }
-
-      // Handle congruence closures over equalities.
-      else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) {
-        Debug("pf::array") << "Handling congruence over equalities" << std::endl;
-
-        // Gather the sequence of consecutive congruence closures.
-        std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures;
-        unsigned count;
-        Debug("pf::array") << "Collecting congruence sequence" << std::endl;
-        for (count = 0;
-             i + count < pf.d_children.size() &&
-               pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-               pf.d_children[i + count]->d_node.isNull();
-             ++count) {
-          Debug("pf::array") << "Found a congruence: " << std::endl;
-          pf.d_children[i + count]->debug_print("pf::array", 0, &proofPrinter);
-          congruenceClosures.push_back(pf.d_children[i + count]);
-        }
-
-        Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
-
-        // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
-        bool targetAppearsBefore = true;
-        bool targetAppearsAfter = true;
-
-        if ((i == 0) || (i == 1 && neg == 0)) {
-          Debug("pf::array") << "Target does not appear before" << std::endl;
-          targetAppearsBefore = false;
-        }
-
-        if ((i + count >= pf.d_children.size()) ||
-            (!pf.d_children[i + count]->d_node.isNull() &&
-             pf.d_children[i + count]->d_node.getKind() == kind::NOT)) {
-          Debug("pf::array") << "Target does not appear after" << std::endl;
-          targetAppearsAfter = false;
-        }
-
-        // Assert that we have precisely one target clause.
-        Assert(targetAppearsBefore != targetAppearsAfter);
-
-        // Begin breaking up the congruences and ordering the equalities correctly.
-        std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
-
-        // Insert target clause first.
-        if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf.d_children[i - 1]);
-          // The target has already been added to subTrans; remove it.
-          subTrans->d_children.pop_back();
-        } else {
-          orderedEqualities.push_back(pf.d_children[i + count]);
-        }
-
-        // Start with the congruence closure closest to the target clause, and work our way back/forward.
-        if (targetAppearsBefore) {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]);
-            if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]);
-          }
-        } else {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]);
-            if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]);
-          }
-        }
-
-        // Copy the result into the main transitivity proof.
-        subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
-
-        // Increase i to skip over the children that have been processed.
-        i += count;
-        if (targetAppearsAfter) {
-          ++i;
-        }
-      }
-
-      // Else, just copy the child proof as is
-      else {
-        subTrans->d_children.push_back(pf.d_children[i]);
-        ++i;
-      }
-    }
-
-    bool disequalityFound = (neg >= 0);
-    if (!disequalityFound) {
-      Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
-      Debug("pf::array") << "Proof for: " << pf.d_node << std::endl;
-      Assert(pf.d_node.getKind() == kind::EQUAL);
-      Assert(pf.d_node.getNumChildren() == 2);
-      Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst());
-    }
+    int neg = tp->assertAndPrint(pf, map, subTrans, &proofPrinter);
 
     Node n1;
     std::stringstream ss, ss2;
-    //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
     Debug("mgdx") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
-    if(!disequalityFound || pf.d_children.size() > 2) {
+    bool disequalityFound = (neg >= 0);
+
+    if (!disequalityFound || pf.d_children.size() > 2)
+    {
       n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
     } else {
       n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
@@ -294,7 +128,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     }
 
     out << "(clausify_false (contra _ ";
-
     if (disequalityFound) {
       Node n2 = pf.d_children[neg]->d_node;
       Assert(n2.getKind() == kind::NOT);
@@ -347,77 +180,95 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return Node();
   }
 
-  if (pf.d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
-    Debug("mgd") << "\nok, looking at congruence:\n";
-    pf.debug_print("mgd", 0, &proofPrinter);
-    std::stack<const theory::eq::EqProof*> stk;
-    for (const theory::eq::EqProof* pf2 = &pf;
-         pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
-         pf2 = pf2->d_children[0].get()) {
-      Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node
-                   << std::endl;
-      Assert(!pf2->d_node.isNull());
-      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF ||
-             pf2->d_node.getKind() == kind::BUILTIN ||
-             pf2->d_node.getKind() == kind::APPLY_UF ||
-             pf2->d_node.getKind() == kind::SELECT ||
-             pf2->d_node.getKind() == kind::PARTIAL_SELECT_0 ||
-             pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 ||
-             pf2->d_node.getKind() == kind::STORE);
-
-      Assert(pf2->d_children.size() == 2);
-      out << "(cong _ _ _ _ _ _ ";
-      stk.push(pf2);
-    }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
-    //    NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
-    NodeBuilder<> b1, b2;
-
-    const theory::eq::EqProof* pf2 = stk.top();
-    stk.pop();
-    Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-    Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
-    out << " ";
-    std::stringstream ss;
-    Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
-
-
-    Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
-    pf2->debug_print("mgd", 0, &proofPrinter);
-    // Temp
-    Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
-    Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
-    //
-    Debug("mgd") << "looking at " << pf2->d_node << "\n";
-    Debug("mgd") << "           " << n1 << "\n";
-    Debug("mgd") << "           " << n2 << "\n";
-
-    int side = 0;
-    if(match(pf2->d_node, n1[0])) {
-      Debug("mgd") << "SIDE IS 0\n";
-      side = 0;
-    } else {
-      Debug("mgd") << "SIDE IS 1\n";
-      if(!match(pf2->d_node, n1[1])) {
-        Debug("mgd") << "IN BAD CASE, our first subproof is\n";
-        pf2->d_children[0]->debug_print("mgd", 0, &proofPrinter);
+  switch (pf.d_id)
+  {
+    case theory::eq::MERGED_THROUGH_CONGRUENCE:
+    {
+      Debug("mgd") << "\nok, looking at congruence:\n";
+      pf.debug_print("mgd", 0, &proofPrinter);
+      std::stack<const theory::eq::EqProof*> stk;
+      for (const theory::eq::EqProof* pf2 = &pf;
+           pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
+           pf2 = pf2->d_children[0].get())
+      {
+        Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node
+                     << std::endl;
+        Assert(!pf2->d_node.isNull());
+        Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF
+               || pf2->d_node.getKind() == kind::BUILTIN
+               || pf2->d_node.getKind() == kind::APPLY_UF
+               || pf2->d_node.getKind() == kind::SELECT
+               || pf2->d_node.getKind() == kind::PARTIAL_SELECT_0
+               || pf2->d_node.getKind() == kind::PARTIAL_SELECT_1
+               || pf2->d_node.getKind() == kind::STORE);
+
+        Assert(pf2->d_children.size() == 2);
+        out << "(cong _ _ _ _ _ _ ";
+        stk.push(pf2);
       }
-      Assert(match(pf2->d_node, n1[1]));
-      side = 1;
-    }
+      Assert(stk.top()->d_children[0]->d_id
+             != theory::eq::MERGED_THROUGH_CONGRUENCE);
+      //    NodeBuilder<> b1(kind::PARTIAL_APPLY_UF),
+      //    b2(kind::PARTIAL_APPLY_UF);
+      NodeBuilder<> b1, b2;
 
-    if(n1[side].getKind() == kind::APPLY_UF ||
-       n1[side].getKind() == kind::PARTIAL_APPLY_UF ||
-       n1[side].getKind() == kind::SELECT ||
-       n1[side].getKind() == kind::PARTIAL_SELECT_1 ||
-       n1[side].getKind() == kind::STORE) {
-      if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) {
-        b1 << kind::PARTIAL_APPLY_UF;
-        b1 << n1[side].getOperator();
-      } else if (n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::PARTIAL_SELECT_1) {
-        // b1 << n1[side].getKind();
-        b1 << kind::SELECT;
-      } else {
+      const theory::eq::EqProof* pf2 = stk.top();
+      stk.pop();
+      Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
+      Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
+      out << " ";
+      std::stringstream ss;
+      Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
+
+      Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]"
+                   << "\n";
+      pf2->debug_print("mgd", 0, &proofPrinter);
+      // Temp
+      Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node
+                   << ". It is: " << n1 << std::endl;
+      Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node
+                   << ". It is: " << n2 << std::endl;
+      //
+      Debug("mgd") << "looking at " << pf2->d_node << "\n";
+      Debug("mgd") << "           " << n1 << "\n";
+      Debug("mgd") << "           " << n2 << "\n";
+
+      int side = 0;
+      if (tp->match(pf2->d_node, n1[0]))
+      {
+        Debug("mgd") << "SIDE IS 0\n";
+        side = 0;
+      }
+      else
+      {
+        Debug("mgd") << "SIDE IS 1\n";
+        if (!tp->match(pf2->d_node, n1[1]))
+        {
+          Debug("mgd") << "IN BAD CASE, our first subproof is\n";
+          pf2->d_children[0]->debug_print("mgd", 0, &proofPrinter);
+        }
+        Assert(tp->match(pf2->d_node, n1[1]));
+        side = 1;
+      }
+
+      if (n1[side].getKind() == kind::APPLY_UF
+          || n1[side].getKind() == kind::PARTIAL_APPLY_UF
+          || n1[side].getKind() == kind::SELECT
+          || n1[side].getKind() == kind::PARTIAL_SELECT_1
+          || n1[side].getKind() == kind::STORE)
+      {
+        if (n1[side].getKind() == kind::APPLY_UF
+            || n1[side].getKind() == kind::PARTIAL_APPLY_UF)
+        {
+          b1 << kind::PARTIAL_APPLY_UF;
+          b1 << n1[side].getOperator();
+        }
+        else if (n1[side].getKind() == kind::SELECT
+                 || n1[side].getKind() == kind::PARTIAL_SELECT_1)
+        {
+          // b1 << n1[side].getKind();
+          b1 << kind::SELECT;
+        } else {
         b1 << kind::PARTIAL_APPLY_UF;
         b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
       }
@@ -539,13 +390,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b1.append(n1.begin(), n1.end());
       n1 = b1;
       Debug("mgd") << "New n1: " << n1 << std::endl;
-      // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
-      //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
-      //   b1.clear(kind::PARTIAL_SELECT_1);
-      //   b1.append(n1.begin(), n1.end());
-      //   n1 = b1;
-      //   Debug("mgd") << "New n1: " << n1 << std::endl;
-      // } else
     } else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
       if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
         b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
@@ -573,13 +417,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b2.append(n2.begin(), n2.end());
       n2 = b2;
       Debug("mgd") << "New n2: " << n2 << std::endl;
-      // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
-      //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
-      //   b2.clear(kind::PARTIAL_SELECT_1);
-      //   b2.append(n2.begin(), n2.end());
-      //   n2 = b2;
-      //   Debug("mgd") << "New n2: " << n2 << std::endl;
-      // } else
     } else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
       if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
         b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
@@ -590,22 +427,22 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b2.append(n2.begin(), n2.end());
       n2 = b2;
     }
-    Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
+    Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1));
 
     Debug("mgdx") << "\ncong proved: " << n << "\n";
     return n;
   }
-
-  else if (pf.d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+  case theory::eq::MERGED_THROUGH_REFLEXIVITY:
+  {
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
     out << ")";
-    return eqNode(pf.d_node, pf.d_node);
+    return pf.d_node.eqNode(pf.d_node);
   }
-
-  else if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY) {
+  case theory::eq::MERGED_THROUGH_EQUALITY:
+  {
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
     Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf.d_node.negate() << " ) = " <<
@@ -614,22 +451,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return pf.d_node;
   }
 
-  else if (pf.d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
-    Debug("pf::array") << "Proof for: " << pf.d_node << std::endl;
-    Assert(pf.d_node.getKind() == kind::NOT);
-    Node n = pf.d_node[0];
-    Assert(n.getKind() == kind::EQUAL);
-    Assert(n.getNumChildren() == 2);
-    Assert(n[0].isConst() && n[1].isConst());
-
-    ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
-                                                                        n[0].toExpr(),
-                                                                        n[1].toExpr(),
-                                                                        map);
-    return pf.d_node;
-  }
-
-  else if (pf.d_id == theory::eq::MERGED_THROUGH_TRANS) {
+  case theory::eq::MERGED_THROUGH_TRANS:
+  {
     bool firstNeg = false;
     bool secondNeg = false;
 
@@ -643,6 +466,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node);
 
     Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
+    Node n2;
     Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
       Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n";
@@ -650,134 +474,117 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     bool identicalEqualities = false;
     bool evenLengthSequence;
-    Node nodeAfterEqualitySequence;
+    std::stringstream dontCare;
+    Node nodeAfterEqualitySequence =
+        toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map);
 
     std::map<size_t, Node> childToStream;
 
-    for(size_t i = 1; i < pf.d_children.size(); ++i) {
+    std::stringstream ss1(ss.str()), ss2;
+    std::pair<Node, Node> nodePair;
+    for (size_t i = 1; i < pf.d_children.size(); ++i)
+    {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
-      // In congruences, we can have something like a[x] - it's important to keep these,
-      // and not turn them into (a[x]=true), because that will mess up the congruence application
+      // In congruences, we can have something like a[x] - it's important to
+      // keep these,
+      // and not turn them into (a[x]=true), because that will mess up the
+      // congruence application
       // later.
 
       if (pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
-        pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
+        pf.d_children[i]->d_node =
+            simplifyBooleanNode(pf.d_children[i]->d_node);
 
-      // It is possible that we've already converted the i'th child to stream. If so,
+      // It is possible that we've already converted the i'th child to stream.
+      // If so,
       // use previously stored result. Otherwise, convert and store.
       Node n2;
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
-      else {
+      else
+      {
         n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
         childToStream[i] = n2;
       }
 
       Debug("mgd") << "\ndoing trans proof, got (first) n2 " << n2 << "\n";
 
-      // The following branch is dedicated to handling sequences of identical equalities,
+      // The following branch is dedicated to handling sequences of identical
+      // equalities,
       // i.e. trans[ a=b, a=b, a=b ].
       //
       // There are two cases:
-      //    1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
+      //    1. The number of equalities is odd. Then, the sequence can be
+      //    collapsed to just one equality,
       //       i.e. a=b.
-      //    2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
-      //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
-      //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
+      //    2. The number of equalities is even. Now, we have two options: a=a
+      //    or b=b. To determine this,
+      //       we look at the node after the equality sequence. If it needs a,
+      //       we go for a=a; and if it needs
+      //       b, we go for b=b. If there is no following node, we look at the
+      //       goal of the transitivity proof,
       //       and use it to determine which option we need.
 
-      if(n2.getKind() == kind::EQUAL) {
-        if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
+      if (n2.getKind() == kind::EQUAL)
+      {
+        if (((n1[0] == n2[0]) && (n1[1] == n2[1]))
+            || ((n1[0] == n2[1]) && (n1[1] == n2[0])))
+        {
           // We are in a sequence of identical equalities
 
-          Debug("pf::array") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl;
+          Debug("pf::array") << "Detected identical equalities: " << std::endl
+                             << "\t" << n1 << std::endl;
 
-          if (!identicalEqualities) {
+          if (!identicalEqualities)
+          {
             // The sequence of identical equalities has started just now
             identicalEqualities = true;
 
-            Debug("pf::array") << "The sequence is just beginning. Determining length..." << std::endl;
+            Debug("pf::array")
+                << "The sequence is just beginning. Determining length..."
+                << std::endl;
 
             // Determine whether the length of this sequence is odd or even.
             evenLengthSequence = true;
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf.d_children.size() && !sequenceOver) {
+            while (j < pf.d_children.size() && !sequenceOver)
+            {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map );
-
-              if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
-                  ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
+              nodeAfterEqualitySequence = toStreamRecLFSC(
+                  dontCare, tp, *(pf.d_children[j]), tb + 1, map);
+              if (((nodeAfterEqualitySequence[0] == n1[0])
+                   && (nodeAfterEqualitySequence[1] == n1[1]))
+                  || ((nodeAfterEqualitySequence[0] == n1[1])
+                      && (nodeAfterEqualitySequence[1] == n1[0])))
+              {
                 evenLengthSequence = !evenLengthSequence;
-              } else {
+              }
+              else
+              {
                 sequenceOver = true;
               }
 
               ++j;
             }
 
-            if (evenLengthSequence) {
-              // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
-
-              Debug("pf::array") << "Equality sequence of even length" << std::endl;
-              Debug("pf::array") << "n1 is: " << n1 << std::endl;
-              Debug("pf::array") << "n2 is: " << n2 << std::endl;
-              Debug("pf::array") << "pf-d_node is: " << pf.d_node << std::endl;
-              Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence << std::endl;
-
-              ss << "(trans _ _ _ _ ";
-
-              // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
-              if (!sequenceOver) {
-                if (match(n1[0], pf.d_node[0])) {
-                  n1 = eqNode(n1[0], n1[0]);
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                } else if (match(n1[1], pf.d_node[1])) {
-                  n1 = eqNode(n1[1], n1[1]);
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                } else {
-                  Debug("pf::array") << "Error: identical equalities over, but hands don't match what we're proving."
-                                     << std::endl;
-                  Assert(false);
-                }
-              } else {
-                // We have a "next node". Use it to guide us.
-                if (nodeAfterEqualitySequence.getKind() == kind::NOT) {
-                  nodeAfterEqualitySequence = nodeAfterEqualitySequence[0];
-                }
-
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
-
-                if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[1]
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                  n1 = eqNode(n1[0], n1[0]);
-
-                } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[0]
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                  n1 = eqNode(n1[1], n1[1]);
-
-                } else {
-                  Debug("pf::array") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl;
-                  Assert(false);
-                }
-              }
-
-              ss << ")";
-
-            } else {
-              Debug("pf::array") << "Equality sequence length is odd!" << std::endl;
-              ss.str(ss1.str());
-            }
-
-            Debug("pf::array") << "Have proven: " << n1 << std::endl;
-          } else {
+            nodePair =
+                tp->identicalEqualitiesPrinterHelper(evenLengthSequence,
+                                                     sequenceOver,
+                                                     pf,
+                                                     map,
+                                                     ss1.str(),
+                                                     &ss,
+                                                     n1,
+                                                     nodeAfterEqualitySequence);
+            n1 = nodePair.first;
+            nodeAfterEqualitySequence = nodePair.second;
+          }
+          else
+          {
             ss.str(ss1.str());
           }
 
@@ -786,18 +593,23 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         }
       }
 
-      if (identicalEqualities) {
-        // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
+      if (identicalEqualities)
+      {
+        // We were in a sequence of identical equalities, but it has now ended.
+        // Resume normal operation.
         identicalEqualities = false;
       }
 
       Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n";
-      if(tb == 1) {
+      if (tb == 1)
+      {
         Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
         Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n";
 
-        if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
-          Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
+        if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2))
+        {
+          Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / "
+                        << n2[0].getId() << " " << n2[1].getId() << "\n";
           Debug("mgdx") << n1[0].getId() << " " << n1[0] << "\n";
           Debug("mgdx") << n1[1].getId() << " " << n1[1] << "\n";
           Debug("mgdx") << n2[0].getId() << " " << n2[0] << "\n";
@@ -836,29 +648,29 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       {
         if(n1[0] == n2[0]) {
           if(tb == 1) { Debug("mgdx") << "case 1\n"; }
-          n1 = eqNode(n1[1], n2[1]);
+          n1 = n1[1].eqNode(n2[1]);
           ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str();
         } else if(n1[1] == n2[1]) {
           if(tb == 1) { Debug("mgdx") << "case 2\n"; }
-          n1 = eqNode(n1[0], n2[0]);
+          n1 = n1[0].eqNode(n2[0]);
           ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")";
         } else if(n1[0] == n2[1]) {
           if(tb == 1) { Debug("mgdx") << "case 3\n"; }
           if(!firstNeg && !secondNeg) {
-            n1 = eqNode(n2[0], n1[1]);
+            n1 = n2[0].eqNode(n1[1]);
             ss << ss2.str() << " " << ss1.str();
           } else if (firstNeg) {
-            n1 = eqNode(n1[1], n2[0]);
+            n1 = n1[1].eqNode(n2[0]);
             ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")";
           } else {
             Assert(secondNeg);
-            n1 = eqNode(n1[1], n2[0]);
+            n1 = n1[1].eqNode(n2[0]);
             ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")";
           }
           if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; }
         } else if(n1[1] == n2[0]) {
           if(tb == 1) { Debug("mgdx") << "case 4\n"; }
-          n1 = eqNode(n1[0], n2[1]);
+          n1 = n1[0].eqNode(n2[1]);
           ss << ss1.str() << " " << ss2.str();
         } else {
           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
@@ -912,246 +724,312 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return n1;
   }
 
-  else if (pf.d_id == d_reasonRow) {
-    Debug("mgd") << "row lemma: " << pf.d_node << std::endl;
-    Assert(pf.d_node.getKind() == kind::EQUAL);
-
-
-    if (pf.d_node[1].getKind() == kind::SELECT) {
-      // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k).
-      TNode t1, t2, t3, t4;
-      Node ret;
-      if(pf.d_node[1].getKind() == kind::SELECT &&
-         pf.d_node[1][0].getKind() == kind::STORE &&
-         pf.d_node[0].getKind() == kind::SELECT &&
-         pf.d_node[0][0] == pf.d_node[1][0][0] &&
-         pf.d_node[0][1] == pf.d_node[1][1]) {
-        t2 = pf.d_node[1][0][1];
-        t3 = pf.d_node[1][1];
-        t1 = pf.d_node[0][0];
-        t4 = pf.d_node[1][0][2];
-        ret = pf.d_node[1].eqNode(pf.d_node[0]);
-        Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
-      } else {
-        Assert(pf.d_node[0].getKind() == kind::SELECT &&
-               pf.d_node[0][0].getKind() == kind::STORE &&
-               pf.d_node[1].getKind() == kind::SELECT &&
-               pf.d_node[1][0] == pf.d_node[0][0][0] &&
-               pf.d_node[1][1] == pf.d_node[0][1]);
-        t2 = pf.d_node[0][0][1];
-        t3 = pf.d_node[0][1];
-        t1 = pf.d_node[1][0];
-        t4 = pf.d_node[0][0][2];
-        ret = pf.d_node;
-        Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
-      }
+  case theory::eq::MERGED_THROUGH_CONSTANTS:
+  {
+    Debug("pf::array") << "Proof for: " << pf.d_node << std::endl;
+    Assert(pf.d_node.getKind() == kind::NOT);
+    Node n = pf.d_node[0];
+    Assert(n.getKind() == kind::EQUAL);
+    Assert(n.getNumChildren() == 2);
+    Assert(n[0].isConst() && n[1].isConst());
 
-      // inner index != outer index
-      // t3 is the outer index
+    ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(
+        out, n[0].toExpr(), n[1].toExpr(), map);
+    return pf.d_node;
+  }
 
-      Assert(pf.d_children.size() == 1);
-      std::stringstream ss;
-      Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
+  default:
+  {
+    if (pf.d_id == d_reasonRow)
+    {
+      Debug("mgd") << "row lemma: " << pf.d_node << std::endl;
+      Assert(pf.d_node.getKind() == kind::EQUAL);
 
-      out << "(row _ _ ";
-      tp->printTerm(t2.toExpr(), out, map);
-      out << " ";
-      tp->printTerm(t3.toExpr(), out, map);
-      out << " ";
-      tp->printTerm(t1.toExpr(), out, map);
-      out << " ";
-      tp->printTerm(t4.toExpr(), out, map);
-      out << " ";
+      if (pf.d_node[1].getKind() == kind::SELECT)
+      {
+        // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof
+        // explains why (i != k).
+        TNode t1, t2, t3, t4;
+        Node ret;
+        if (pf.d_node[1].getKind() == kind::SELECT
+            && pf.d_node[1][0].getKind() == kind::STORE
+            && pf.d_node[0].getKind() == kind::SELECT
+            && pf.d_node[0][0] == pf.d_node[1][0][0]
+            && pf.d_node[0][1] == pf.d_node[1][1])
+        {
+          t2 = pf.d_node[1][0][1];
+          t3 = pf.d_node[1][1];
+          t1 = pf.d_node[0][0];
+          t4 = pf.d_node[1][0][2];
+          ret = pf.d_node[1].eqNode(pf.d_node[0]);
+          Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3
+                       << "\nt4 " << t4 << "\n";
+        }
+        else
+        {
+          Assert(pf.d_node[0].getKind() == kind::SELECT
+                 && pf.d_node[0][0].getKind() == kind::STORE
+                 && pf.d_node[1].getKind() == kind::SELECT
+                 && pf.d_node[1][0] == pf.d_node[0][0][0]
+                 && pf.d_node[1][1] == pf.d_node[0][1]);
+          t2 = pf.d_node[0][0][1];
+          t3 = pf.d_node[0][1];
+          t1 = pf.d_node[1][0];
+          t4 = pf.d_node[0][0][2];
+          ret = pf.d_node;
+          Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3
+                       << "\nt4 " << t4 << "\n";
+        }
 
+        // inner index != outer index
+        // t3 is the outer index
 
-      Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node
-                         << ". t3 is: " << t3 << std::endl
-                         << "subproof is: " << subproof << std::endl;
+        Assert(pf.d_children.size() == 1);
+        std::stringstream ss;
+        Node subproof =
+            toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
 
-      Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
+        out << "(row _ _ ";
+        tp->printTerm(t2.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(t3.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(t1.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(t4.toExpr(), out, map);
+        out << " ";
 
-      // The subproof needs to show that t2 != t3. This can either be a direct disequality,
-      // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant.
-      if (subproof.getKind() == kind::NOT) {
-        // The subproof is for t2 != t3 (or t3 != t2)
-        if (subproof[0][1] == t3) {
-          Debug("pf::array") << "Dont need symmetry!" << std::endl;
-          out << ss.str();
-        } else {
-          Debug("pf::array") << "Need symmetry!" << std::endl;
-          out << "(negsymm _ _ _ " << ss.str() << ")";
-        }
-      } else {
-        // Either t2 or t3 is a constant.
-        Assert(subproof.getKind() == kind::EQUAL);
-        Assert(subproof[0].isConst() || subproof[1].isConst());
-        Assert(t2.isConst() || t3.isConst());
-        Assert(!(t2.isConst() && t3.isConst()));
-
-        bool t2IsConst = t2.isConst();
-        if (subproof[0].isConst()) {
-          if (t2IsConst) {
-            // (t3 == subproof[1]) == subproof[0] != t2
-            // goal is t2 != t3
-            // subproof already shows constant = t3
-            Assert(t3 == subproof[1]);
-            out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[0].toExpr(), map);
-            out << " ";
-            out << ss.str();
-            out << ")";
-          } else {
-            Assert(t2 == subproof[1]);
-            out << "(negsymm _ _ _ ";
-            out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[0].toExpr(), map);
-            out << " ";
+        Debug("pf::array") << "pf.d_children[0]->d_node is: "
+                           << pf.d_children[0]->d_node << ". t3 is: " << t3
+                           << std::endl
+                           << "subproof is: " << subproof << std::endl;
+
+        Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
+
+        // The subproof needs to show that t2 != t3. This can either be a direct
+        // disequality,
+        // or, if (wlog) t2 is constant, it can show that t3 is equal to another
+        // constant.
+        if (subproof.getKind() == kind::NOT)
+        {
+          // The subproof is for t2 != t3 (or t3 != t2)
+          if (subproof[0][1] == t3)
+          {
+            Debug("pf::array") << "Dont need symmetry!" << std::endl;
             out << ss.str();
-            out << "))";
           }
-        } else {
-          if (t2IsConst) {
-            // (t3 == subproof[0]) == subproof[1] != t2
-            // goal is t2 != t3
-            // subproof already shows constant = t3
-            Assert(t3 == subproof[0]);
-            out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t2.toExpr(), subproof[1].toExpr(), map);
-            out << " ";
-            out << "(symm _ _ _ " << ss.str() << ")";
-            out << ")";
-          } else {
-            Assert(t2 == subproof[0]);
-            out << "(negsymm _ _ _ ";
-            out << "(negtrans _ _ _ _ ";
-            tp->printConstantDisequalityProof(out, t3.toExpr(), subproof[1].toExpr(), map);
-            out << " ";
-            out << "(symm _ _ _ " << ss.str() << ")";
-            out << "))";
+          else
+          {
+            Debug("pf::array") << "Need symmetry!" << std::endl;
+            out << "(negsymm _ _ _ " << ss.str() << ")";
+          }
+        }
+        else
+        {
+          // Either t2 or t3 is a constant.
+          Assert(subproof.getKind() == kind::EQUAL);
+          Assert(subproof[0].isConst() || subproof[1].isConst());
+          Assert(t2.isConst() || t3.isConst());
+          Assert(!(t2.isConst() && t3.isConst()));
+
+          bool t2IsConst = t2.isConst();
+          if (subproof[0].isConst())
+          {
+            if (t2IsConst)
+            {
+              // (t3 == subproof[1]) == subproof[0] != t2
+              // goal is t2 != t3
+              // subproof already shows constant = t3
+              Assert(t3 == subproof[1]);
+              out << "(negtrans _ _ _ _ ";
+              tp->printConstantDisequalityProof(
+                  out, t2.toExpr(), subproof[0].toExpr(), map);
+              out << " ";
+              out << ss.str();
+              out << ")";
+            }
+            else
+            {
+              Assert(t2 == subproof[1]);
+              out << "(negsymm _ _ _ ";
+              out << "(negtrans _ _ _ _ ";
+              tp->printConstantDisequalityProof(
+                  out, t3.toExpr(), subproof[0].toExpr(), map);
+              out << " ";
+              out << ss.str();
+              out << "))";
+            }
+          }
+          else
+          {
+            if (t2IsConst)
+            {
+              // (t3 == subproof[0]) == subproof[1] != t2
+              // goal is t2 != t3
+              // subproof already shows constant = t3
+              Assert(t3 == subproof[0]);
+              out << "(negtrans _ _ _ _ ";
+              tp->printConstantDisequalityProof(
+                  out, t2.toExpr(), subproof[1].toExpr(), map);
+              out << " ";
+              out << "(symm _ _ _ " << ss.str() << ")";
+              out << ")";
+            }
+            else
+            {
+              Assert(t2 == subproof[0]);
+              out << "(negsymm _ _ _ ";
+              out << "(negtrans _ _ _ _ ";
+              tp->printConstantDisequalityProof(
+                  out, t3.toExpr(), subproof[1].toExpr(), map);
+              out << " ";
+              out << "(symm _ _ _ " << ss.str() << ")";
+              out << "))";
+            }
           }
         }
-      }
-
-      out << ")";
-      return ret;
-    } else {
-      Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl;
-
-      Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf.d_children[0]->d_node << std::endl;
 
-      // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k])
+        out << ")";
+        return ret;
+      }
+      else
+      {
+        Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl;
+
+        Debug("pf::array") << "pf.d_children[0]->d_node is: "
+                           << pf.d_children[0]->d_node << std::endl;
+
+        // This is the case where (i == k), and the sub-proof explains why
+        // ((a[i]:=t)[k] != a[k])
+
+        // If we wanted to remove the need for "negativerow", we would need to
+        // prove i==k using a new satlem. We would:
+        // 1. Create a new satlem.
+        // 2. Assume that i != k
+        // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k])
+        // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]),
+        // obtaining our contradiction
+
+        TNode t1, t2, t3, t4;
+        Node ret;
+
+        // pf.d_node is an equality, i==k.
+        t1 = pf.d_node[0];
+        t2 = pf.d_node[1];
+
+        // pf.d_children[0]->d_node will have the form: (not (= (select (store
+        // a_565 i7 e_566) i1) (select a_565 i1))),
+        // or its symmetrical version.
+
+        unsigned side;
+        if (pf.d_children[0]->d_node[0][0].getKind() == kind::SELECT
+            && pf.d_children[0]->d_node[0][0][0].getKind() == kind::STORE)
+        {
+          side = 0;
+        }
+        else if (pf.d_children[0]->d_node[0][1].getKind() == kind::SELECT
+                 && pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE)
+        {
+          side = 1;
+        }
+        else
+        {
+          Unreachable();
+        }
 
-      // If we wanted to remove the need for "negativerow", we would need to prove i==k using a new satlem. We would:
-      // 1. Create a new satlem.
-      // 2. Assume that i != k
-      // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k])
-      // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), obtaining our contradiction
+        Debug("pf::array") << "Side is: " << side << std::endl;
 
-      TNode t1, t2, t3, t4;
-      Node ret;
+        // The array's index and element types will come from the subproof...
+        t3 = pf.d_children[0]->d_node[0][side][0][0];
+        t4 = pf.d_children[0]->d_node[0][side][0][2];
+        ret = pf.d_node;
 
-      // pf.d_node is an equality, i==k.
-      t1 = pf.d_node[0];
-      t2 = pf.d_node[1];
+        // The order of indices needs to match; we might have to swap t1 and t2
+        // and then apply symmetry.
+        bool swap = (t2 == pf.d_children[0]->d_node[0][side][0][1]);
 
-      // pf.d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
-      // or its symmetrical version.
+        Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 "
+                     << t4 << "\n";
 
-      unsigned side;
-      if (pf.d_children[0]->d_node[0][0].getKind() == kind::SELECT &&
-          pf.d_children[0]->d_node[0][0][0].getKind() == kind::STORE) {
-        side = 0;
-      } else if (pf.d_children[0]->d_node[0][1].getKind() == kind::SELECT &&
-                 pf.d_children[0]->d_node[0][1][0].getKind() == kind::STORE) {
-        side = 1;
-      }
-      else {
-        Unreachable();
-      }
+        Assert(pf.d_children.size() == 1);
+        std::stringstream ss;
+        Node subproof =
+            toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
 
-      Debug("pf::array") << "Side is: " << side << std::endl;
+        Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
 
-      // The array's index and element types will come from the subproof...
-      t3 = pf.d_children[0]->d_node[0][side][0][0];
-      t4 = pf.d_children[0]->d_node[0][side][0][2];
-      ret = pf.d_node;
+        if (swap)
+        {
+          out << "(symm _ _ _ ";
+        }
 
-      // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
-      bool swap = (t2 == pf.d_children[0]->d_node[0][side][0][1]);
+        out << "(negativerow _ _ ";
+        tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(t3.toExpr(), out, map);
+        out << " ";
+        tp->printTerm(t4.toExpr(), out, map);
+        out << " ";
 
-      Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
+        if (side != 0)
+        {
+          out << "(negsymm _ _ _ " << ss.str() << ")";
+        }
+        else
+        {
+          out << ss.str();
+        }
 
-      Assert(pf.d_children.size() == 1);
-      std::stringstream ss;
-      Node subproof = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
+        out << ")";
 
-      Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
+        if (swap)
+        {
+          out << ") ";
+        }
 
-      if (swap) {
-        out << "(symm _ _ _ ";
+        return ret;
       }
-
-      out << "(negativerow _ _ ";
-      tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
+    }
+    else if (pf.d_id == d_reasonRow1)
+    {
+      Debug("mgd") << "row1 lemma: " << pf.d_node << std::endl;
+      Assert(pf.d_node.getKind() == kind::EQUAL);
+      TNode t1, t2, t3;
+      Node ret;
+      if (pf.d_node[1].getKind() == kind::SELECT
+          && pf.d_node[1][0].getKind() == kind::STORE
+          && pf.d_node[1][0][1] == pf.d_node[1][1]
+          && pf.d_node[1][0][2] == pf.d_node[0])
+      {
+        t1 = pf.d_node[1][0][0];
+        t2 = pf.d_node[1][0][1];
+        t3 = pf.d_node[0];
+        ret = pf.d_node[1].eqNode(pf.d_node[0]);
+        Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
+      }
+      else
+      {
+        Assert(pf.d_node[0].getKind() == kind::SELECT
+               && pf.d_node[0][0].getKind() == kind::STORE
+               && pf.d_node[0][0][1] == pf.d_node[0][1]
+               && pf.d_node[0][0][2] == pf.d_node[1]);
+        t1 = pf.d_node[0][0][0];
+        t2 = pf.d_node[0][0][1];
+        t3 = pf.d_node[1];
+        ret = pf.d_node;
+        Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
+      }
+      out << "(row1 _ _ ";
+      tp->printTerm(t1.toExpr(), out, map);
       out << " ";
-      tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
+      tp->printTerm(t2.toExpr(), out, map);
       out << " ";
       tp->printTerm(t3.toExpr(), out, map);
-      out << " ";
-      tp->printTerm(t4.toExpr(), out, map);
-      out << " ";
-
-      if (side != 0) {
-        out << "(negsymm _ _ _ " << ss.str() << ")";
-      } else {
-        out << ss.str();
-      }
-
       out << ")";
-
-      if (swap) {
-        out << ") ";
-      }
-
       return ret;
-    }
-  }
-
-  else if (pf.d_id == d_reasonRow1) {
-    Debug("mgd") << "row1 lemma: " << pf.d_node << std::endl;
-    Assert(pf.d_node.getKind() == kind::EQUAL);
-    TNode t1, t2, t3;
-    Node ret;
-    if(pf.d_node[1].getKind() == kind::SELECT &&
-       pf.d_node[1][0].getKind() == kind::STORE &&
-       pf.d_node[1][0][1] == pf.d_node[1][1] &&
-       pf.d_node[1][0][2] == pf.d_node[0]) {
-      t1 = pf.d_node[1][0][0];
-      t2 = pf.d_node[1][0][1];
-      t3 = pf.d_node[0];
-      ret = pf.d_node[1].eqNode(pf.d_node[0]);
-      Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
-    } else {
-      Assert(pf.d_node[0].getKind() == kind::SELECT &&
-             pf.d_node[0][0].getKind() == kind::STORE &&
-             pf.d_node[0][0][1] == pf.d_node[0][1] &&
-             pf.d_node[0][0][2] == pf.d_node[1]);
-      t1 = pf.d_node[0][0][0];
-      t2 = pf.d_node[0][0][1];
-      t3 = pf.d_node[1];
-      ret = pf.d_node;
-      Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
-    }
-    out << "(row1 _ _ ";
-    tp->printTerm(t1.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t2.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t3.toExpr(), out, map);
-    out << ")";
-    return ret;
   }
-
   else if (pf.d_id == d_reasonExt) {
     Assert(pf.d_node.getKind() == kind::NOT);
     Assert(pf.d_node[0].getKind() == kind::EQUAL);
@@ -1186,11 +1064,14 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return pf.d_node;
   }
 }
+  }
+}
 
 ArrayProof::ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* pe)
   : TheoryProof(arrays, pe)
 {}
 
+theory::TheoryId ArrayProof::getTheoryId() { return theory::THEORY_ARRAYS; }
 void ArrayProof::registerTerm(Expr term) {
   // already registered
   if (d_declarations.find(term) != d_declarations.end())
@@ -1214,8 +1095,10 @@ void ArrayProof::registerTerm(Expr term) {
   if (term.getKind() == kind::SELECT && term.getType().isBoolean()) {
     // Ensure cnf literals
     Node asNode(term);
-    ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true)));
-    ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false)));
+    ProofManager::currentPM()->ensureLiteral(
+        asNode.eqNode(NodeManager::currentNM()->mkConst(true)));
+    ProofManager::currentPM()->ensureLiteral(
+        asNode.eqNode(NodeManager::currentNM()->mkConst(false)));
   }
 
   // recursively declare all other terms
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 779624df0..ea865f9d8 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -79,8 +79,9 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
   ExprSet d_skolemDeclarations; // all the skolem variable declarations
   std::map<Expr, std::string> d_skolemToLiteral;
+  theory::TheoryId getTheoryId();
 
-public:
+ public:
   ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine);
 
   std::string skolemToLiteral(Expr skolem);
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 7a2faba37..afddfd323 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -51,6 +51,7 @@ void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) {
   d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true);
 }
 
+theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
 void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
                                   context::Context* cnf) {
   Assert (d_cnfProof == NULL);
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index b5487a352..a41d5d515 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -83,7 +83,7 @@ protected:
 
   std::map<Expr,std::string> d_constantLetMap;
   bool d_useConstantLetification;
-
+  theory::TheoryId getTheoryId();
   context::Context d_fakeContext;
 public:
   BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 0dd573dc6..34f3a92ec 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -29,6 +29,7 @@
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof.h"
+#include "proof/simplify_boolean_node.h"
 #include "proof/uf_proof.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine.h"
@@ -38,13 +39,11 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/output_channel.h"
 #include "theory/term_registration_visitor.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 #include "util/proof.h"
 
-
 namespace CVC4 {
 
 unsigned CVC4::ProofLetCount::counter = 0;
@@ -1099,6 +1098,7 @@ void BooleanProof::registerTerm(Expr term) {
   }
 }
 
+theory::TheoryId BooleanProof::getTheoryId() { return theory::THEORY_BOOL; }
 void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   Node falseNode = NodeManager::currentNM()->mkConst(false);
   Node trueNode = NodeManager::currentNM()->mkConst(true);
@@ -1264,4 +1264,373 @@ void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node
   os << "))";
 }
 
+inline bool TheoryProof::match(TNode n1, TNode n2)
+{
+  theory::TheoryId theoryId = this->getTheoryId();
+  ProofManager* pm = ProofManager::currentPM();
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  Debug(ufProof ? "pf::uf" : "mgd") << "match " << n1 << " " << n2 << std::endl;
+  if (pm->hasOp(n1))
+  {
+    n1 = pm->lookupOp(n1);
+  }
+  if (pm->hasOp(n2))
+  {
+    n2 = pm->lookupOp(n2);
+  }
+  Debug(ufProof ? "pf::uf" : "mgd") << "+ match " << n1 << " " << n2
+                                    << std::endl;
+  if (!ufProof)
+  {
+    Debug("pf::array") << "+ match: step 1" << std::endl;
+  }
+  if (n1 == n2)
+  {
+    return true;
+  }
+
+  if (n1.getType().isFunction() && n2.hasOperator())
+  {
+    if (pm->hasOp(n2.getOperator()))
+    {
+      return n1 == pm->lookupOp(n2.getOperator());
+    }
+    else
+    {
+      return n1 == n2.getOperator();
+    }
+  }
+
+  if (n2.getType().isFunction() && n1.hasOperator())
+  {
+    if (pm->hasOp(n1.getOperator()))
+    {
+      return n2 == pm->lookupOp(n1.getOperator());
+    }
+    else
+    {
+      return n2 == n1.getOperator();
+    }
+  }
+
+  if (n1.hasOperator() && n2.hasOperator()
+      && n1.getOperator() != n2.getOperator())
+  {
+    if (ufProof
+        || !((n1.getKind() == kind::SELECT
+              && n2.getKind() == kind::PARTIAL_SELECT_0)
+             || (n1.getKind() == kind::SELECT
+                 && n2.getKind() == kind::PARTIAL_SELECT_1)
+             || (n1.getKind() == kind::PARTIAL_SELECT_1
+                 && n2.getKind() == kind::SELECT)
+             || (n1.getKind() == kind::PARTIAL_SELECT_1
+                 && n2.getKind() == kind::PARTIAL_SELECT_0)
+             || (n1.getKind() == kind::PARTIAL_SELECT_0
+                 && n2.getKind() == kind::SELECT)
+             || (n1.getKind() == kind::PARTIAL_SELECT_0
+                 && n2.getKind() == kind::PARTIAL_SELECT_1)))
+    {
+      return false;
+    }
+  }
+
+  for (size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i)
+  {
+    if (n1[i] != n2[i])
+    {
+      return false;
+    }
+  }
+
+  return true;
+}
+
+int TheoryProof::assertAndPrint(
+    const theory::eq::EqProof& pf,
+    const ProofLetMap& map,
+    std::shared_ptr<theory::eq::EqProof> subTrans,
+    theory::eq::EqProof::PrettyPrinter* pPrettyPrinter)
+{
+  theory::TheoryId theoryId = getTheoryId();
+  int neg = -1;
+  Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS);
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  std::string theoryName = theory::getStatsPrefix(theoryId);
+  pf.debug_print(("pf::" + theoryName).c_str(), 0, pPrettyPrinter);
+  Debug("pf::" + theoryName) << std::endl;
+
+  Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
+  Assert(!pf.d_node.isNull());
+  Assert(pf.d_children.size() >= 2);
+
+  subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
+  subTrans->d_node = pf.d_node;
+
+  size_t i = 0;
+  while (i < pf.d_children.size())
+  {
+    // special treatment for uf and not for array
+    if (ufProof
+        || pf.d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+    {
+      pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
+    }
+
+    // Look for the negative clause, with which we will form a contradiction.
+    if (!pf.d_children[i]->d_node.isNull()
+        && pf.d_children[i]->d_node.getKind() == kind::NOT)
+    {
+      Assert(neg < 0);
+      (neg) = i;
+      ++i;
+    }
+
+    // Handle congruence closures over equalities.
+    else if (pf.d_children[i]->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE
+             && pf.d_children[i]->d_node.isNull())
+    {
+      Debug("pf::" + theoryName) << "Handling congruence over equalities"
+                                 << std::endl;
+
+      // Gather the sequence of consecutive congruence closures.
+      std::vector<std::shared_ptr<const theory::eq::EqProof>>
+          congruenceClosures;
+      unsigned count;
+      Debug("pf::" + theoryName) << "Collecting congruence sequence"
+                                 << std::endl;
+      for (count = 0; i + count < pf.d_children.size()
+                      && pf.d_children[i + count]->d_id
+                             == theory::eq::MERGED_THROUGH_CONGRUENCE
+                      && pf.d_children[i + count]->d_node.isNull();
+           ++count)
+      {
+        Debug("pf::" + theoryName) << "Found a congruence: " << std::endl;
+        pf.d_children[i + count]->debug_print(
+            ("pf::" + theoryName).c_str(), 0, pPrettyPrinter);
+        congruenceClosures.push_back(pf.d_children[i + count]);
+      }
+
+      Debug("pf::" + theoryName)
+          << "Total number of congruences found: " << congruenceClosures.size()
+          << std::endl;
+
+      // Determine if the "target" of the congruence sequence appears right
+      // before or right after the sequence.
+      bool targetAppearsBefore = true;
+      bool targetAppearsAfter = true;
+
+      if ((i == 0) || (i == 1 && neg == 0))
+      {
+        Debug("pf::" + theoryName) << "Target does not appear before"
+                                   << std::endl;
+        targetAppearsBefore = false;
+      }
+
+      if ((i + count >= pf.d_children.size())
+          || (!pf.d_children[i + count]->d_node.isNull()
+              && pf.d_children[i + count]->d_node.getKind() == kind::NOT))
+      {
+        Debug("pf::" + theoryName) << "Target does not appear after"
+                                   << std::endl;
+        targetAppearsAfter = false;
+      }
+
+      // Flow changes between uf and array
+      if (ufProof)
+      {
+        // Assert that we have precisely at least one possible clause.
+        Assert(targetAppearsBefore || targetAppearsAfter);
+
+        // If both are valid, assume the one after the sequence is correct
+        if (targetAppearsAfter && targetAppearsBefore)
+        {
+          targetAppearsBefore = false;
+        }
+      }
+      else
+      {  // not a uf proof
+        // Assert that we have precisely one target clause.
+        Assert(targetAppearsBefore != targetAppearsAfter);
+      }
+
+      // Begin breaking up the congruences and ordering the equalities
+      // correctly.
+      std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
+
+      // Insert target clause first.
+      if (targetAppearsBefore)
+      {
+        orderedEqualities.push_back(pf.d_children[i - 1]);
+        // The target has already been added to subTrans; remove it.
+        subTrans->d_children.pop_back();
+      }
+      else
+      {
+        orderedEqualities.push_back(pf.d_children[i + count]);
+      }
+
+      // Start with the congruence closure closest to the target clause, and
+      // work our way back/forward.
+      if (targetAppearsBefore)
+      {
+        for (unsigned j = 0; j < count; ++j)
+        {
+          if (pf.d_children[i + j]->d_children[0]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(orderedEqualities.begin(),
+                                     pf.d_children[i + j]->d_children[0]);
+          if (pf.d_children[i + j]->d_children[1]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(orderedEqualities.end(),
+                                     pf.d_children[i + j]->d_children[1]);
+        }
+      }
+      else
+      {
+        for (unsigned j = 0; j < count; ++j)
+        {
+          if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(
+                orderedEqualities.begin(),
+                pf.d_children[i + count - 1 - j]->d_children[0]);
+          if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id
+              != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(
+                orderedEqualities.end(),
+                pf.d_children[i + count - 1 - j]->d_children[1]);
+        }
+      }
+
+      // Copy the result into the main transitivity proof.
+      subTrans->d_children.insert(subTrans->d_children.end(),
+                                  orderedEqualities.begin(),
+                                  orderedEqualities.end());
+
+      // Increase i to skip over the children that have been processed.
+      i += count;
+      if (targetAppearsAfter)
+      {
+        ++i;
+      }
+    }
+
+    // Else, just copy the child proof as is
+    else
+    {
+      subTrans->d_children.push_back(pf.d_children[i]);
+      ++i;
+    }
+  }
+
+  bool disequalityFound = (neg >= 0);
+  if (!disequalityFound)
+  {
+    Debug("pf::" + theoryName)
+        << "A disequality was NOT found. UNSAT due to merged constants"
+        << std::endl;
+    Debug("pf::" + theoryName) << "Proof for: " << pf.d_node << std::endl;
+    Assert(pf.d_node.getKind() == kind::EQUAL);
+    Assert(pf.d_node.getNumChildren() == 2);
+    Assert(pf.d_node[0].isConst() && pf.d_node[1].isConst());
+  }
+  return neg;
+}
+
+std::pair<Node, Node> TheoryProof::identicalEqualitiesPrinterHelper(
+    bool evenLengthSequence,
+    bool sequenceOver,
+    const theory::eq::EqProof& pf,
+    const ProofLetMap& map,
+    const std::string subproofStr,
+    std::stringstream* outStream,
+    Node n,
+    Node nodeAfterEqualitySequence)
+{
+  theory::TheoryId theoryId = getTheoryId();
+  Assert(theoryId == theory::THEORY_UF || theoryId == theory::THEORY_ARRAYS);
+  bool ufProof = (theoryId == theory::THEORY_UF);
+  std::string theoryName = theory::getStatsPrefix(theoryId);
+  if (evenLengthSequence)
+  {
+    // If the length is even, we need to apply transitivity for the "correct"
+    // hand of the equality.
+
+    Debug("pf::" + theoryName) << "Equality sequence of even length"
+                               << std::endl;
+    Debug("pf::" + theoryName) << "n1 is: " << n << std::endl;
+    Debug("pf::" + theoryName) << "pf-d_node is: " << pf.d_node << std::endl;
+    Debug("pf::" + theoryName) << "Next node is: " << nodeAfterEqualitySequence
+                               << std::endl;
+
+    (*outStream) << "(trans _ _ _ _ ";
+
+    // If the sequence is at the very end of the transitivity proof, use
+    // pf.d_node to guide us.
+    if (!sequenceOver)
+    {
+      if (match(n[0], pf.d_node[0]))
+      {
+        n = n[0].eqNode(n[0]);
+        (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")";
+      }
+      else if (match(n[1], pf.d_node[1]))
+      {
+        n = n[1].eqNode(n[1]);
+        (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr;
+      }
+      else
+      {
+        Debug("pf::" + theoryName) << "Error: identical equalities over, but "
+                                      "hands don't match what we're proving."
+                                   << std::endl;
+        Assert(false);
+      }
+    }
+    else
+    {
+      // We have a "next node". Use it to guide us.
+      if (!ufProof && nodeAfterEqualitySequence.getKind() == kind::NOT)
+      {
+        nodeAfterEqualitySequence = nodeAfterEqualitySequence[0];
+      }
+
+      Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
+
+      if ((n[0] == nodeAfterEqualitySequence[0])
+          || (n[0] == nodeAfterEqualitySequence[1]))
+      {
+        // Eliminate n[1]
+        (*outStream) << subproofStr << " (symm _ _ _ " << subproofStr << ")";
+        n = n[0].eqNode(n[0]);
+      }
+      else if ((n[1] == nodeAfterEqualitySequence[0])
+               || (n[1] == nodeAfterEqualitySequence[1]))
+      {
+        // Eliminate n[0]
+        (*outStream) << " (symm _ _ _ " << subproofStr << ")" << subproofStr;
+        n = n[1].eqNode(n[1]);
+      }
+      else
+      {
+        Debug("pf::" + theoryName) << "Error: even length sequence, but I "
+                                      "don't know which hand to keep!"
+                                   << std::endl;
+        Assert(false);
+      }
+    }
+
+    (*outStream) << ")";
+  }
+  else
+  {
+    Debug("pf::" + theoryName) << "Equality sequence length is odd!"
+                               << std::endl;
+    (*outStream).str(subproofStr);
+  }
+
+  Debug("pf::" + theoryName) << "Have proven: " << n << std::endl;
+  return std::make_pair<Node&, Node&>(n, nodeAfterEqualitySequence);
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 4e599f570..efe05bce8 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -26,10 +26,10 @@
 
 #include "expr/expr.h"
 #include "proof/clause_id.h"
+#include "proof/proof_utils.h"
 #include "prop/sat_solver_types.h"
+#include "theory/uf/equality_engine.h"
 #include "util/proof.h"
-#include "proof/proof_utils.h"
-
 namespace CVC4 {
 
 namespace theory {
@@ -207,7 +207,9 @@ protected:
   // Pointer to the theory for this proof
   theory::Theory* d_theory;
   TheoryProofEngine* d_proofEngine;
-public:
+  virtual theory::TheoryId getTheoryId() = 0;
+
+ public:
   TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine)
     : d_theory(th)
     , d_proofEngine(proofEngine)
@@ -238,6 +240,54 @@ public:
   void printSort(Type type, std::ostream& os) {
     d_proofEngine->printSort(type, os);
   }
+
+  // congrence matching term helper
+  inline bool match(TNode n1, TNode n2);
+
+  /**
+   * Helper function for ProofUF::toStreamRecLFSC and
+   * ProofArray::toStreamRecLFSC
+   * Inputs:
+   *    - pf: equality engine proof
+   *    - map: A map for the let-expressions in the proof
+   *    - subTrans: main transitivity proof part
+   *    - pPrettyPrinter: optional pretty printer for sub-proofs
+   * returns:
+   *    - the index of the contradicting node in pf.
+   *    */
+  int assertAndPrint(
+      const theory::eq::EqProof& pf,
+      const ProofLetMap& map,
+      std::shared_ptr<theory::eq::EqProof> subTrans,
+      theory::eq::EqProof::PrettyPrinter* pPrettyPrinter = nullptr);
+
+  /**
+   * Helper function for ProofUF::toStreamRecLFSC and
+   * ProofArray::toStreamRecLFSC
+   * Inputs:
+   *    - evenLengthSequence: true iff the length of the sequence
+   *                          of the identical equalities is even.
+   *    - sequenceOver: have we reached the last equality of this sequence?
+   *    - pf: equality engine proof
+   *    - map: A map for the let-expressions in the proof
+   *    - subproofStr: current stringstream content
+   *    - outStream: output stream to which the proof is printed
+   *    - n: transitivity sub-proof
+   *    - nodeAfterEqualitySequence: The node after the identical sequence.
+   * Returns:
+   *    A pair of nodes, that are the updated nodes n and nodeAfterEqualitySequence
+   *
+   */
+  std::pair<Node, Node> identicalEqualitiesPrinterHelper(
+      bool evenLengthSequence,
+      bool sequenceOver,
+      const theory::eq::EqProof& pf,
+      const ProofLetMap& map,
+      const std::string subproofStr,
+      std::stringstream* outStream,
+      Node n,
+      Node nodeAfterEqualitySequence);
+
   /**
    * Print the proof representation of the given type that belongs to THIS theory.
    *
@@ -313,7 +363,9 @@ public:
 class BooleanProof : public TheoryProof {
 protected:
   ExprSet d_declarations; // all the boolean variables
-public:
+  theory::TheoryId getTheoryId();
+
+ public:
   BooleanProof(TheoryProofEngine* proofEngine);
 
   void registerTerm(Expr term) override;
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 746cbbc54..9f7ae7ac1 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -24,48 +24,6 @@
 
 namespace CVC4 {
 
-inline static Node eqNode(TNode n1, TNode n2) {
-  return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
-}
-
-// congrence matching term helper
-inline static bool match(TNode n1, TNode n2) {
-  Debug("pf::uf") << "match " << n1 << " " << n2 << std::endl;
-  if(ProofManager::currentPM()->hasOp(n1)) {
-    n1 = ProofManager::currentPM()->lookupOp(n1);
-  }
-  if(ProofManager::currentPM()->hasOp(n2)) {
-    n2 = ProofManager::currentPM()->lookupOp(n2);
-  }
-  Debug("pf::uf") << "+ match " << n1 << " " << n2 << std::endl;
-  if(n1 == n2) {
-    return true;
-  }
-  if(n1.getType().isFunction() && n2.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
-      return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator());
-    } else {
-      return n1 == n2.getOperator();
-    }
-  }
-  if(n2.getType().isFunction() && n1.hasOperator()) {
-    if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
-      return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator());
-    } else {
-      return n2 == n1.getOperator();
-    }
-  }
-  if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) {
-    return false;
-  }
-  for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) {
-    if(n1[i] != n2[i]) {
-      return false;
-    }
-  }
-  return true;
-}
-
 void ProofUF::toStream(std::ostream& out) const
 {
   ProofLetMap map;
@@ -101,10 +59,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
                   << std::endl
                   << "toStreamRecLFSC called. tb = " << tb
                   << " . proof:" << std::endl;
-  pf.debug_print("pf::uf");
-  Debug("pf::uf") << std::endl;
-
-  if (tb == 0) {
+  if (tb == 0)
+  {
     // Special case: false was an input, so the proof is just "false".
     if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
         pf.d_node == NodeManager::currentNM()->mkConst(false)) {
@@ -114,149 +70,38 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       return Node();
     }
 
-    Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
-    Assert(!pf.d_node.isNull());
-    Assert(pf.d_children.size() >= 2);
-
-    int neg = -1;
     std::shared_ptr<theory::eq::EqProof> subTrans =
         std::make_shared<theory::eq::EqProof>();
-    subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
-    subTrans->d_node = pf.d_node;
-
-    size_t i = 0;
-
-    while (i < pf.d_children.size()) {
-      pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
-
-      // Look for the negative clause, with which we will form a contradiction.
-      if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) {
-        Assert(neg < 0);
-        Node node = pf.d_children[i]->d_node[0];
-        neg = i;
-        ++i;
-      }
-
-      // Handle congruence closures over equalities.
-      else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) {
-        Debug("pf::uf") << "Handling congruence over equalities" << std::endl;
-
-        // Gather the sequence of consecutive congruence closures.
-        std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures;
-        unsigned count;
-        Debug("pf::uf") << "Collecting congruence sequence" << std::endl;
-        for (count = 0;
-             i + count < pf.d_children.size() &&
-               pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-               pf.d_children[i + count]->d_node.isNull();
-             ++count) {
-          Debug("pf::uf") << "Found a congruence: " << std::endl;
-          pf.d_children[i+count]->debug_print("pf::uf");
-          congruenceClosures.push_back(pf.d_children[i+count]);
-        }
-
-        Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
 
-        // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
-        bool targetAppearsBefore = true;
-        bool targetAppearsAfter = true;
-
-        if ((i == 0) || (i == 1 && neg == 0)) {
-          Debug("pf::uf") << "Target does not appear before" << std::endl;
-          targetAppearsBefore = false;
-        }
-
-        if ((i + count >= pf.d_children.size()) ||
-            (!pf.d_children[i + count]->d_node.isNull() &&
-             pf.d_children[i + count]->d_node.getKind() == kind::NOT)) {
-          Debug("pf::uf") << "Target does not appear after" << std::endl;
-          targetAppearsAfter = false;
-        }
-
-        // Assert that we have precisely at least one possible clause.
-        Assert(targetAppearsBefore || targetAppearsAfter);
-
-        // If both are valid, assume the one after the sequence is correct
-        if (targetAppearsAfter && targetAppearsBefore)
-          targetAppearsBefore = false;
-
-        // Begin breaking up the congruences and ordering the equalities correctly.
-        std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
-
-        // Insert target clause first.
-        if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf.d_children[i - 1]);
-          // The target has already been added to subTrans; remove it.
-          subTrans->d_children.pop_back();
-        } else {
-          orderedEqualities.push_back(pf.d_children[i + count]);
-        }
-
-        // Start with the congruence closure closest to the target clause, and work our way back/forward.
-        if (targetAppearsBefore) {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]);
-            if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]);
-          }
-        } else {
-          for (unsigned j = 0; j < count; ++j) {
-            if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]);
-            if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]);
-          }
-        }
-
-        // Copy the result into the main transitivity proof.
-        subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
-
-        // Increase i to skip over the children that have been processed.
-        i += count;
-        if (targetAppearsAfter) {
-          ++i;
-        }
-      }
-
-      // Else, just copy the child proof as is
-      else {
-        subTrans->d_children.push_back(pf.d_children[i]);
-        ++i;
-      }
-    }
-
-    bool disequalityFound = (neg >= 0);
-    if (!disequalityFound) {
-      Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
-      Debug("pf::uf") << "Proof for: " << pf.d_node << std::endl;
-      Assert(pf.d_node.getKind() == kind::EQUAL);
-      Assert(pf.d_node.getNumChildren() == 2);
-      Assert (pf.d_node[0].isConst() && pf.d_node[1].isConst());
-    }
+    int neg = tp->assertAndPrint(pf, map, subTrans);
 
     Node n1;
-    std::stringstream ss;
+    std::stringstream ss, ss2;
     Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
+    bool disequalityFound = (neg >= 0);
 
     if(!disequalityFound || subTrans->d_children.size() >= 2) {
       n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
     } else {
       n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
-      Debug("pf::uf") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+      Debug("pf::uf") << "\nsubTrans unique child "
+                      << subTrans->d_children[0]->d_id
+                      << " was proven\ngot: " << n1 << std::endl;
     }
 
     Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
 
     out << "(clausify_false (contra _ ";
-
     if (disequalityFound) {
       Node n2 = pf.d_children[neg]->d_node;
       Assert(n2.getKind() == kind::NOT);
 
       Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 
-      if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
+      if (n2[0].getNumChildren() > 0)
+      {
+        Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl;
+      }
       if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
 
       if(n2[0].getKind() == kind::APPLY_UF) {
@@ -289,7 +134,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
       out << ss.str();
       out << " ";
-      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr(), map);
+      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(
+          out, n1[0].toExpr(), n1[1].toExpr(), map);
       out << "))" << std::endl;
     }
 
@@ -305,7 +151,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
          pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
          pf2 = pf2->d_children[0].get()) {
       Assert(!pf2->d_node.isNull());
-      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
+      Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF
+             || pf2->d_node.getKind() == kind::BUILTIN
+             || pf2->d_node.getKind() == kind::APPLY_UF
+             || pf2->d_node.getKind() == kind::SELECT
+             || pf2->d_node.getKind() == kind::STORE);
       Assert(pf2->d_children.size() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
@@ -325,7 +175,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
     Debug("pf::uf") << "           " << n1 << "\n";
     Debug("pf::uf") << "           " << n2 << "\n";
     int side = 0;
-    if(match(pf2->d_node, n1[0])) {
+    if (tp->match(pf2->d_node, n1[0]))
+    {
       //if(tb == 1) {
       Debug("pf::uf") << "SIDE IS 0\n";
       //}
@@ -334,15 +185,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       //if(tb == 1) {
       Debug("pf::uf") << "SIDE IS 1\n";
       //}
-      if(!match(pf2->d_node, n1[1])) {
+      if (!tp->match(pf2->d_node, n1[1]))
+      {
         Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
         pf2->d_children[0]->debug_print("pf::uf");
       }
-      Assert(match(pf2->d_node, n1[1]));
+      Assert(tp->match(pf2->d_node, n1[1]));
       side = 1;
     }
-    if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
-      if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) {
+    if (n1[side].getKind() == kind::APPLY_UF
+        || n1[side].getKind() == kind::PARTIAL_APPLY_UF
+        || n1[side].getKind() == kind::SELECT
+        || n1[side].getKind() == kind::STORE)
+    {
+      if (n1[side].getKind() == kind::APPLY_UF
+          || n1[side].getKind() == kind::PARTIAL_APPLY_UF)
+      {
         b1 << n1[side].getOperator();
       } else {
         b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
@@ -352,7 +210,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       b1 << n1[side];
     }
     if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
-      if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) {
+      if (n1[1 - side].getKind() == kind::PARTIAL_APPLY_UF
+          || n1[1 - side].getKind() == kind::APPLY_UF)
+      {
         b2 << n1[1-side].getOperator();
       } else {
         b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
@@ -435,7 +295,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       b2.append(n2.begin(), n2.end());
       n2 = b2;
     }
-    Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
+    Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1));
     if(tb == 1) {
       Debug("pf::uf") << "\ncong proved: " << n << "\n";
     }
@@ -443,13 +303,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
   }
 
   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
+  {
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
     out << ")";
-    return eqNode(pf.d_node, pf.d_node);
-
+    return pf.d_node.eqNode(pf.d_node);
+  }
   case theory::eq::MERGED_THROUGH_EQUALITY:
     Assert(!pf.d_node.isNull());
     Assert(pf.d_children.empty());
@@ -468,128 +329,109 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
     Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
     Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
+    Node n2;
     if(tb == 1) {
       Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n";
     }
 
     bool identicalEqualities = false;
     bool evenLengthSequence;
-    Node nodeAfterEqualitySequence;
+    std::stringstream dontCare;
+    Node nodeAfterEqualitySequence =
+        toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map);
 
     std::map<size_t, Node> childToStream;
-
+    std::stringstream ss1(ss.str()), ss2;
+    std::pair<Node, Node> nodePair;
     for(size_t i = 1; i < pf.d_children.size(); ++i) {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
       pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
 
-      // It is possible that we've already converted the i'th child to stream. If so,
+      // It is possible that we've already converted the i'th child to stream.
+      // If so,
       // use previously stored result. Otherwise, convert and store.
       Node n2;
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
-      else {
+      else
+      {
         n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
         childToStream[i] = n2;
       }
 
-      // The following branch is dedicated to handling sequences of identical equalities,
+      // The following branch is dedicated to handling sequences of identical
+      // equalities,
       // i.e. trans[ a=b, a=b, a=b ].
       //
       // There are two cases:
-      //    1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
+      //    1. The number of equalities is odd. Then, the sequence can be
+      //    collapsed to just one equality,
       //       i.e. a=b.
-      //    2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
-      //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
-      //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
+      //    2. The number of equalities is even. Now, we have two options: a=a
+      //    or b=b. To determine this,
+      //       we look at the node after the equality sequence. If it needs a,
+      //       we go for a=a; and if it needs
+      //       b, we go for b=b. If there is no following node, we look at the
+      //       goal of the transitivity proof,
       //       and use it to determine which option we need.
-      if(n2.getKind() == kind::EQUAL) {
-        if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
+      if (n2.getKind() == kind::EQUAL)
+      {
+        if (((n1[0] == n2[0]) && (n1[1] == n2[1]))
+            || ((n1[0] == n2[1]) && (n1[1] == n2[0])))
+        {
           // We are in a sequence of identical equalities
 
-          Debug("pf::uf") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl;
+          Debug("pf::uf") << "Detected identical equalities: " << std::endl
+                          << "\t" << n1 << std::endl;
 
-          if (!identicalEqualities) {
+          if (!identicalEqualities)
+          {
             // The sequence of identical equalities has started just now
             identicalEqualities = true;
 
-            Debug("pf::uf") << "The sequence is just beginning. Determining length..." << std::endl;
+            Debug("pf::uf")
+                << "The sequence is just beginning. Determining length..."
+                << std::endl;
 
             // Determine whether the length of this sequence is odd or even.
             evenLengthSequence = true;
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf.d_children.size() && !sequenceOver) {
+            while (j < pf.d_children.size() && !sequenceOver)
+            {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, *(pf.d_children[j]), tb + 1, map );
-
-              if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
-                  ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
+              nodeAfterEqualitySequence = toStreamRecLFSC(
+                  dontCare, tp, *(pf.d_children[j]), tb + 1, map);
+
+              if (((nodeAfterEqualitySequence[0] == n1[0])
+                   && (nodeAfterEqualitySequence[1] == n1[1]))
+                  || ((nodeAfterEqualitySequence[0] == n1[1])
+                      && (nodeAfterEqualitySequence[1] == n1[0])))
+              {
                 evenLengthSequence = !evenLengthSequence;
-              } else {
+              }
+              else
+              {
                 sequenceOver = true;
               }
 
               ++j;
             }
 
-            if (evenLengthSequence) {
-              // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
-
-              Debug("pf::uf") << "Equality sequence of even length" << std::endl;
-              Debug("pf::uf") << "n1 is: " << n1 << std::endl;
-              Debug("pf::uf") << "n2 is: " << n2 << std::endl;
-              Debug("pf::uf") << "pf-d_node is: " << pf.d_node << std::endl;
-              Debug("pf::uf") << "Next node is: " << nodeAfterEqualitySequence << std::endl;
-
-              ss << "(trans _ _ _ _ ";
-
-              // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
-              if (!sequenceOver) {
-                if (match(n1[0], pf.d_node[0])) {
-                  n1 = eqNode(n1[0], n1[0]);
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                } else if (match(n1[1], pf.d_node[1])) {
-                  n1 = eqNode(n1[1], n1[1]);
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                } else {
-                  Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving."
-                                  << std::endl;
-                  Assert(false);
-                }
-              } else {
-                // We have a "next node". Use it to guide us.
-
-                Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
-
-                if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[1]
-                  ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
-                  n1 = eqNode(n1[0], n1[0]);
-
-                } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) {
-
-                  // Eliminate n1[0]
-                  ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
-                  n1 = eqNode(n1[1], n1[1]);
-
-                } else {
-                  Debug("pf::uf") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl;
-                  Assert(false);
-                }
-              }
-
-              ss << ")";
-
-            } else {
-              Debug("pf::uf") << "Equality sequence length is odd!" << std::endl;
-              ss.str(ss1.str());
-            }
-
-            Debug("pf::uf") << "Have proven: " << n1 << std::endl;
+            nodePair =
+                tp->identicalEqualitiesPrinterHelper(evenLengthSequence,
+                                                     sequenceOver,
+                                                     pf,
+                                                     map,
+                                                     ss1.str(),
+                                                     &ss,
+                                                     n1,
+                                                     nodeAfterEqualitySequence);
+            n1 = nodePair.first;
+            nodeAfterEqualitySequence = nodePair.second;
           } else {
             ss.str(ss1.str());
           }
@@ -621,6 +463,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
           Debug("pf::uf") << (n1[1] == n2[0]) << "\n";
         }
       }
+
       ss << "(trans _ _ _ _ ";
 
       if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL)
@@ -628,20 +471,20 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
       {
         if(n1[0] == n2[0]) {
           if(tb == 1) { Debug("pf::uf") << "case 1\n"; }
-          n1 = eqNode(n1[1], n2[1]);
+          n1 = n1[1].eqNode(n2[1]);
           ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
         } else if(n1[1] == n2[1]) {
           if(tb == 1) { Debug("pf::uf") << "case 2\n"; }
-          n1 = eqNode(n1[0], n2[0]);
+          n1 = n1[0].eqNode(n2[0]);
           ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
         } else if(n1[0] == n2[1]) {
           if(tb == 1) { Debug("pf::uf") << "case 3\n"; }
-          n1 = eqNode(n2[0], n1[1]);
+          n1 = n2[0].eqNode(n1[1]);
           ss << ss2.str() << " " << ss1.str();
           if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; }
         } else if(n1[1] == n2[0]) {
           if(tb == 1) { Debug("pf::uf") << "case 4\n"; }
-          n1 = eqNode(n1[0], n2[1]);
+          n1 = n1[0].eqNode(n2[1]);
           ss << ss1.str() << " " << ss2.str();
         } else {
           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
@@ -734,6 +577,7 @@ UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe)
   : TheoryProof(uf, pe)
 {}
 
+theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; }
 void UFProof::registerTerm(Expr term) {
   // already registered
   if (d_declarations.find(term) != d_declarations.end())
@@ -757,8 +601,10 @@ void UFProof::registerTerm(Expr term) {
     if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
       // Ensure cnf literals
       Node asNode(term);
-      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true)));
-      ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false)));
+      ProofManager::currentPM()->ensureLiteral(
+          asNode.eqNode(NodeManager::currentNM()->mkConst(true)));
+      ProofManager::currentPM()->ensureLiteral(
+          asNode.eqNode(NodeManager::currentNM()->mkConst(false)));
     }
   }
 
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 7aa00cc35..a4e4cff0b 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -62,8 +62,9 @@ class UFProof : public TheoryProof {
 protected:
   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
   ExprSet d_declarations; // all the variable/function declarations
+  theory::TheoryId getTheoryId();
 
-public:
+ public:
   UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
 
   void registerTerm(Expr term) override;