1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 1bf42a105..25797dda3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -271,16 +271,14 @@ class TheoryArrays : public Theory {
           }
         }
         // Propagate equality between shared terms
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality);
+        return d_arrays.propagate(t1.eqNode(t2));
       } else {
         if (t1.getType().isArray()) {
           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
             return true;
           }
         }
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality.notNode());
+        return d_arrays.propagate(t1.eqNode(t2).notNode());
       }
       return true;
     }