From 4a652a4c0c088bd69cb7ea1ce0b45fdfd95c53ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 10 Sep 2022 16:02:58 -0700
Subject: [PATCH] relax giveup condition for as-array when it occurs only in
 beta redex positions.

---
 src/smt/theory_array_full.cpp | 15 +++++++++++++--
 src/smt/theory_array_full.h   |  2 ++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 5de571255..360d34cd4 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -330,7 +330,8 @@ namespace smt {
             // Even if there was, as-array on interpreted 
             // functions will be incomplete.
             // The instantiation operations are still sound to include.
-            found_unsupported_op(n);
+            m_as_array.push_back(node);
+            ctx.push_trail(push_back_vector(m_as_array));
             instantiate_default_as_array_axiom(node);
         }
         else if (is_array_ext(n)) {
@@ -815,12 +816,22 @@ namespace smt {
         if (r == FC_DONE && m_bapa) {
             r = m_bapa->final_check();
         }
-        bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
+        bool should_giveup = m_found_unsupported_op || has_propagate_up_trail() || has_non_beta_as_array();
         if (r == FC_DONE && should_giveup)
             r = FC_GIVEUP;
         return r;
     }
 
+    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))
+                    return true;
+        }
+        return false;
+    }
+
+
     bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
         SASSERT(v != null_theory_var);
         TRACE("array", tout << "v" << v << "\n";);
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 09a6daaec..210426e10 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -85,6 +85,8 @@ namespace smt {
         bool has_large_domain(app* array_term);
         bool has_unitary_domain(app* array_term);
         std::pair<app*,func_decl*> mk_epsilon(sort* s);
+        enode_vector m_as_array;
+        bool has_non_beta_as_array();
 
         bool instantiate_select_const_axiom(enode* select, enode* cnst);
         bool instantiate_select_as_array_axiom(enode* select, enode* arr);