2 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 6985aaea8..0aff30d74 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -118,7 +118,7 @@ void TheoryArrays::check(Effort e) {
         // which can lead to a conflict
         Node conflict = constructConflict(d_conflict);
         d_conflict = Node::null();
-        d_out->conflict(conflict, false);
+        d_out->conflict(conflict);
         return;
       }
       merge(assertion[0], assertion[1]);
@@ -139,13 +139,13 @@ void TheoryArrays::check(Effort e) {
         // after addTerm since we weren't watching a or b before
         Node conflict = constructConflict(d_conflict);
         d_conflict = Node::null();
-        d_out->conflict(conflict, false);
+        d_out->conflict(conflict);
         return;
       }
       else if(find(a) == find(b)) {
         Node conflict = constructConflict(assertion[0]);
         d_conflict = Node::null();
-        d_out->conflict(conflict, false);
+        d_out->conflict(conflict);
         return;
         }
       Assert(!d_cc.areCongruent(a,b));
@@ -764,7 +764,7 @@ bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) {
       nb << literal1.notNode() << literal2.notNode();
       literal1 = nb;
       d_conflict = Node::null();
-      d_out->conflict(literal1, false);
+      d_out->conflict(literal1);
       Trace("arrays") << "TheoryArrays::isRedundantInContext() "
                       << "conflict via lemma: " << literal1 << endl;
       return true;
@@ -870,7 +870,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
   return false;
 }
 
-void TheoryArrays::explain(TNode n) {
+Node TheoryArrays::explain(TNode n) {
 
 
   Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
@@ -901,7 +901,7 @@ void TheoryArrays::explain(TNode n) {
   }
   Node reason = nb;
 
-  d_out->explanation(reason);
+  return reason;
 
   /*
   context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 37fffd2ec..a984cb342 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -476,7 +476,7 @@ public:
     */
 
   }
-  void explain(TNode n);
+  Node explain(TNode n);
 
   Node getValue(TNode n);
   SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);