From 6ea8599e0c98d7a94c836cb6e25e4de204c522a0 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 14 Oct 2025 09:46:41 +0000
Subject: [PATCH] Use array select instead of function application for map and
 select axioms

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/rewriter/finite_set_axioms.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index 5a9c4c5d8..ad78c5956 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/ast.h"
 #include "ast/finite_set_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
 #include "ast/rewriter/finite_set_axioms.h"
 
 // a ~ set.empty => not (x in a)
@@ -208,9 +209,9 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
     
     expr_ref x_in_b(u.mk_in(x, b), m);
     
-    // Apply function f to x
-    app* f_app = to_app(f);
-    expr_ref fx(m.mk_app(f_app->get_decl(), x), m);
+    // Apply function f to x using array select
+    array_util autil(m);
+    expr_ref fx(autil.mk_select(f, x), m);
     expr_ref fx_in_a(u.mk_in(fx, a), m);
     
     // (x in b) => f(x) in a
@@ -230,9 +231,9 @@ void finite_set_axioms::in_select_axiom(expr *x, expr *a) {
     expr_ref x_in_a(u.mk_in(x, a), m);
     expr_ref x_in_b(u.mk_in(x, b), m);
     
-    // Apply predicate p to x
-    app* p_app = to_app(p);
-    expr_ref px(m.mk_app(p_app->get_decl(), x), m);
+    // Apply predicate p to x using array select
+    array_util autil(m);
+    expr_ref px(autil.mk_select(p, x), m);
     
     // (x in a) => (x in b)
     expr_ref_vector clause1(m);