* removing rewriteEquality from the rewriter

* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized 

2 files changed, 2 insertions, 8 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;
     }
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 627f34a30..c6ef5cd25 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -109,10 +109,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static Node rewriteEquality(TNode node) {
-    return postRewrite(node).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}