From c30b8842470203b1ae7ca02d08afdb0ad58f2a48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Sep 2022 11:01:24 -0700
Subject: [PATCH] fix #6340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_array_full.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index d72eb4c06..120e12418 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -607,7 +607,7 @@ namespace smt {
         expr_ref val(mk_select(args), m);
         ctx.get_rewriter()(val);
         if (has_quantifiers(val)) {
-            expr_ref fn(m.mk_fresh_const("lambda-body", m.mk_bool_sort()), m);
+            expr_ref fn(m.mk_fresh_const("lambda-body", val->get_sort()), m);
             expr_ref eq(m.mk_eq(fn, val), m);
             ctx.assert_expr(eq);
             ctx.internalize_assertions();