From ecdfab81a640c7591d572602b7a58a1cc04a11c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Oct 2024 17:50:53 -0700 Subject: [PATCH] fix #7434 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7b54f76a10e..20241536fe3 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2785,9 +2785,16 @@ br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) { result = m.mk_false(); return BR_REWRITE1; } - if (m_util.is_bv2int(lhs, x) && m_util.is_bv2int(rhs, y)) { + if (m_util.is_bv2int(lhs, x) && + m_util.is_bv2int(rhs, y)) { + auto szx = m_util.get_bv_size(x); + auto szy = m_util.get_bv_size(y); + if (szx < szy) + x = m_util.mk_zero_extend(szy - szx, x); + else if (szx > szy) + y = m_util.mk_zero_extend(szx - szy, y); result = m.mk_eq(x, y); - return BR_REWRITE1; + return BR_REWRITE2; } return BR_FAILED; }