Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

2 files changed, 1 insertions, 55 deletions

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 6dfd14157..11c3dc081 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -101,59 +101,8 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         Debug("pf::ee") << "Getting explanation for ROW guard: "
                         << indexOne << " != " << indexTwo << std::endl;
 
-
         eq::EqProof* childProof = new eq::EqProof;
         d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
-
-        // It could be that the guard condition is a constant disequality. In this case,
-        // we need to change it to a different format.
-        if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
-          // The proof has two children, explaining why each index is a (different) constant.
-          Assert(childProof->d_children.size() == 2);
-
-          Node constantOne, constantTwo;
-          // Each subproof explains why one of the indices is constant.
-
-          if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantOne = childProof->d_children[0]->d_node;
-          } else {
-            Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
-            if ((childProof->d_children[0]->d_node[0] == indexOne) ||
-                (childProof->d_children[0]->d_node[0] == indexTwo)) {
-              constantOne = childProof->d_children[0]->d_node[1];
-            } else {
-              constantOne = childProof->d_children[0]->d_node[0];
-            }
-          }
-
-          if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantTwo = childProof->d_children[1]->d_node;
-          } else {
-            Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
-            if ((childProof->d_children[1]->d_node[0] == indexOne) ||
-                (childProof->d_children[1]->d_node[0] == indexTwo)) {
-              constantTwo = childProof->d_children[1]->d_node[1];
-            } else {
-              constantTwo = childProof->d_children[1]->d_node[0];
-            }
-          }
-
-          eq::EqProof* constantDisequalityProof = new eq::EqProof;
-          constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
-          constantDisequalityProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
-
-          // Middle is where we need to insert the new disequality
-          std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
-          ++middle;
-
-          childProof->d_children.insert(middle, constantDisequalityProof);
-
-          childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
-          childProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
-        }
-
         proof->d_children.push_back(childProof);
       } else {
         // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 28a08630e..6add1b55f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -829,8 +829,7 @@ void TheoryArrays::propagate(Effort e)
 
 
 Node TheoryArrays::explain(TNode literal) {
-  Node explanation = explain(literal, NULL);
-  return explanation;
+  return explain(literal, NULL);
 }
 
 Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
@@ -1395,7 +1394,6 @@ void TheoryArrays::check(Effort e) {
         break;
     default:
       Unreachable();
-      break;
     }
   }
 
@@ -2233,7 +2231,6 @@ bool TheoryArrays::dischargeLemmas()
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
   eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
-
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b), proof);
   } else {