From eceeb295fc1f006b30c0932b3adad4173b65f327 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Nov 2022 14:41:50 +0700
Subject: [PATCH] fix #6457

---
 src/ast/rewriter/bv_rewriter.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index c59423310..972259bd7 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2388,7 +2388,9 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
     expr* a = nullptr, *b = nullptr, *c = nullptr;
     if (m().is_ite(lhs, a, b, c)) {
         bool_rewriter rw(m());
-        result = rw.mk_ite(a, rw.mk_eq(b, rhs), rw.mk_eq(c, rhs));
+        expr_ref e1(rw.mk_eq(b, rhs), m());
+        expr_ref e2(rw.mk_eq(c, rhs), m());
+        result = rw.mk_ite(a, e1, e2);
         return BR_REWRITE2;
     }