Sharing work

1 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 716323b8a..e299f84e7 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -36,9 +36,6 @@ class TheoryBuiltinRewriter {
 public:
 
   static inline RewriteResponse postRewrite(TNode node) {
-    if(node.getKind() == kind::EQUAL) {
-      return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node);
-    }
     return RewriteResponse(REWRITE_DONE, node);
   }
 
@@ -46,13 +43,16 @@ public:
     switch(node.getKind()) {
     case kind::DISTINCT:
       return RewriteResponse(REWRITE_DONE, blastDistinct(node));
-    case kind::EQUAL:
-      return Rewriter::callPreRewrite(Theory::theoryOf(node[0]), node);
     default:
       return RewriteResponse(REWRITE_DONE, node);
     }
   }
 
+  static inline Node rewriteEquality(TNode equality) {
+    Unreachable();
+    return equality;
+  }
+
   static inline void init() {}
   static inline void shutdown() {}