From 87095950cb7ac8a5f5653b44d0a1bd8ac50f5636 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Dec 2022 13:02:45 -0800
Subject: [PATCH] fix #6477

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

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 34d2f6508..179113241 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1988,6 +1988,10 @@ bool bv_rewriter::distribute_concat(decl_kind k, unsigned n, expr* const* args,
             expr* e = to_app(arg)->get_arg(0);
             unsigned sz1 = get_bv_size(e);
             unsigned sz2 = get_bv_size(arg);
+            if (sz1 == sz2) {
+                result = m.mk_app(get_fid(), k, n, args);
+                return true;
+            }
             expr_ref_vector args1(m), args2(m);
             for (unsigned j = 0; j < n; ++j) {
                 args1.push_back(m_mk_extract(sz2 - 1, sz2 - sz1, args[j]));