fix regression crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 15, 2022 · 255414f · 255414f
1 parent 9845c33
commit 255414f
Showing 1 changed file with 13 additions and 12 deletions.
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
@@ -647,11 +647,13 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
     SASSERT(m().is_value(val));
 
     if (m().are_distinct(val, e)) {
-        result = m().mk_and(mk_eq(t, val), cond);
+        mk_eq(t, val, result);
+        result = m().mk_and(result, cond);
         return BR_REWRITE2;
     }
     if (m().are_distinct(val, t)) {
-        result = m().mk_and(mk_eq(e, val), m().mk_not(cond));
+        mk_eq(e, val, result);
+        result = m().mk_and(result, m().mk_not(cond));
         return BR_REWRITE2;
     }
     if (m().are_equal(val, t)) {
@@ -660,12 +662,14 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
             return BR_DONE;
         }
         else {
-            result = m().mk_or(mk_eq(e, val), cond);
+            mk_eq(e, val, result);
+            result = m().mk_or(result, cond);
         }
         return BR_REWRITE2;
     }
     if (m().are_equal(val, e)) {
-        result = m().mk_or(mk_eq(t, val), m().mk_not(cond));
+        mk_eq(t, val, result);
+        result = m().mk_or(result, m().mk_not(cond));
         return BR_REWRITE2;
     }
 
@@ -686,10 +690,6 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
 
 
 app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
-    if (m().are_distinct(lhs, rhs))
-        return m().mk_false();
-    if (lhs == rhs)
-        return m().mk_true();
     // degrades simplification 
     // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
     return m().mk_eq(lhs, rhs);
@@ -761,7 +761,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
         }
 
         if (unfolded) {
-            result = mk_eq(lhs, rhs);
+            result = m().mk_eq(lhs, rhs);
             return BR_REWRITE1;
         }
 
@@ -789,7 +789,8 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
 
     if (num_args == 2) {
         expr_ref tmp(m());
-        result = mk_not(mk_eq(args[0], args[1]));
+        mk_eq(args[0], args[1], tmp);
+        mk_not(tmp, result);
         return BR_REWRITE2; // mk_eq may be dispatched to other rewriters.
     }
 
@@ -828,10 +829,10 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
     }
 
     if (m_blast_distinct && num_args < m_blast_distinct_threshold) {
-        ptr_buffer<expr> new_diseqs;
+        expr_ref_vector new_diseqs(m());
         for (unsigned i = 0; i < num_args; i++) {
             for (unsigned j = i + 1; j < num_args; j++)
-                new_diseqs.push_back(mk_not(mk_eq(args[i], args[j])));
+                new_diseqs.push_back(m().mk_not(m().mk_eq(args[i], args[j])));
         }
         result = m().mk_and(new_diseqs);
         return BR_REWRITE3;