3 files changed, 15 insertions, 18 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 7946fea59..f9b97d524 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -247,16 +247,14 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
         for (j = leftWrites - 1; j > i; --j) {
           index_j = write_j[1];
           if (!ppCheck || !ppDisequal(index_i, index_j)) {
-            Node hyp2(index_i.getType() == nm->booleanType()?
-                      index_i.iffNode(index_j) : index_i.eqNode(index_j));
+            Node hyp2(index_i.eqNode(index_j));
             hyp << hyp2.notNode();
           }
           write_j = write_j[0];
         }
 
         Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
-        conc = (r1.getType() == nm->booleanType())?
-          r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
+        conc = r1.eqNode(write_i[2]);
         if (hyp.getNumChildren() != 0) {
           if (hyp.getNumChildren() == 1) {
             conc = hyp.getChild(0).impNode(conc);
@@ -356,8 +354,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     case kind::NOT:
     {
       d_ppFacts.push_back(in);
-      Assert(in[0].getKind() == kind::EQUAL ||
-             in[0].getKind() == kind::IFF );
+      Assert(in[0].getKind() == kind::EQUAL );
       Node a = in[0][0];
       Node b = in[0][1];
       d_ppEqualityEngine.assertEquality(in[0], false, in);
@@ -403,7 +400,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::E
   TNode atom = polarity ? literal : literal[0];
   //eq::EqProof * eqp = new eq::EqProof;
   // eq::EqProof * eqp = NULL;
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
@@ -2235,11 +2232,7 @@ 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 {
-    d_conflictNode = explain(a.eqNode(b), proof);
-  }
+  d_conflictNode = explain(a.eqNode(b), proof);
 
   if (!d_inCheckModel) {
     ProofArray* proof_array = NULL;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 77c5928f0..a1d275364 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -296,7 +296,13 @@ class TheoryArrays : public Theory {
     }
 
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Unreachable();
+      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
+      // Just forward to arrays
+      if (value) {
+        return d_arrays.propagate(predicate);
+      } else {
+        return d_arrays.propagate(predicate.notNode());
+      }
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 2726f386b..e63c224a0 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -33,7 +33,7 @@ void setMostFrequentValue(TNode store, TNode value);
 void setMostFrequentValueCount(TNode store, uint64_t count);
 
 static inline Node mkEqNode(Node a, Node b) {
-  return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
+  return a.eqNode(b);
 }
 
 class TheoryArraysRewriter {
@@ -377,8 +377,7 @@ public:
         }
         break;
       }
-      case kind::EQUAL:
-      case kind::IFF: {
+      case kind::EQUAL:{
         if(node[0] == node[1]) {
           Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
@@ -483,8 +482,7 @@ public:
         }
         break;
       }
-      case kind::EQUAL:
-      case kind::IFF: {
+      case kind::EQUAL:{
         if(node[0] == node[1]) {
           Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));