Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 1 insertions, 4 deletions

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 {