Sharing work

1 files changed, 5 insertions, 6 deletions

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 8c1c16de2..f3a19ff02 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -68,12 +68,7 @@ public:
         }
         if (node[0] > node[1]) {
           Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
-          // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
-          if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
-            return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
-          } else {
-            return RewriteResponse(REWRITE_DONE, newNode);
-          }
+          return RewriteResponse(REWRITE_DONE, newNode);
         }
         break;
       }
@@ -89,6 +84,10 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
+  static Node rewriteEquality(TNode node) {
+    return postRewrite(node).node;
+  }
+
   static inline void init() {}
   static inline void shutdown() {}