From 2daf569da63ed93801ff88c4fff1297313af764b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Aug 2021 17:50:49 -0700
Subject: [PATCH] update Bool rewriter to pull negations up

---
 src/ast/rewriter/bool_rewriter.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index f21b2c554..101bbd771 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -721,9 +721,18 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             result = m().mk_false();
             return BR_DONE;
         }
+
+	    if (m().is_not(rhs))
+            std::swap(lhs, rhs);
+	
+	    if (m().is_not(lhs, lhs)) {
+	        result = m().mk_not(m().mk_eq(lhs, rhs));
+	        return BR_REWRITE2;
+        }
+	    
         if (unfolded) {
             result = mk_eq(lhs, rhs);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
 
         expr *la, *lb, *ra, *rb;