diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 84552282b..ffceec277 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -690,8 +690,10 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
 
 
 app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
-    // degrades simplification 
-    // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
+    if (m().are_equal(lhs, rhs))
+        return m().mk_true();
+    if (m().are_distinct(lhs, rhs))
+        return m().mk_false();
     return m().mk_eq(lhs, rhs);
 }