From 7a55bd568730df527b742d4ea9adcf07dc6f11a5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 Sep 2022 05:44:11 -0700
Subject: [PATCH] beta redex check is used in array theory to filter out safe
 as-arrays

---
 src/smt/smt_context.h         | 4 ++--
 src/smt/theory_array_full.cpp | 4 +++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index f91878632..2fb888bc3 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -777,8 +777,6 @@ namespace smt {
 
         bool has_lambda();
 
-        bool is_beta_redex(enode* p, enode* n) const;
-
         void internalize_lambda(quantifier * q);
 
         void internalize_formula_core(app * n, bool gate_ctx);
@@ -1035,6 +1033,8 @@ namespace smt {
 
         bool is_shared(enode * n) const;
 
+        bool is_beta_redex(enode* p, enode* n) const;
+
         void assign_eq(enode * lhs, enode * rhs, eq_justification const & js) {
             push_eq(lhs, rhs, js);
         }
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 360d34cd4..d72eb4c06 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -825,8 +825,10 @@ namespace smt {
     bool theory_array_full::has_non_beta_as_array() {
         for (enode* n : m_as_array) {
             for (enode* p : n->get_parents())
-                if (!is_beta_redex(p, n))
+                if (!ctx.is_beta_redex(p, n)) {
+                    TRACE("array", tout << "not a beta redex " << enode_pp(p, ctx) << "\n");
                     return true;
+                }
         }
         return false;
     }