diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 099f7aef53..fbcff6f28b 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -420,6 +420,41 @@ public:
         e = mk_and(fmls);
         return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); });
     }
+
+    // The array term-graph projection (mbp_qel) treats an array equality
+    // (= a b) as an implicit partial array equality and eliminates it via
+    // class-merging. That rewrite is unsound when such an equality (or an
+    // array variable being eliminated) occurs inside a select/store *index*
+    // position, because the index is a first-class term whose value must be
+    // preserved. Detect that situation so we can fall back to the classic,
+    // model-based projection which handles it correctly (issues #7259, #7036).
+    bool has_array_var_in_index(app_ref_vector const& vars, expr* fml) {
+        array_util au(m);
+        ptr_vector<app> arr_vars;
+        for (app* v : vars)
+            if (au.is_array(v))
+                arr_vars.push_back(v);
+        if (arr_vars.empty())
+            return false;
+        for (expr* t : subterms::all(expr_ref(fml, m))) {
+            if (!is_app(t))
+                continue;
+            app* a = to_app(t);
+            bool is_sel = au.is_select(a);
+            bool is_st = au.is_store(a);
+            if (!is_sel && !is_st)
+                continue;
+            // args[0] is the array; the trailing arg of a store is the stored
+            // value; everything in between is an index argument.
+            unsigned n = a->get_num_args();
+            unsigned last = is_st ? n - 1 : n;
+            for (unsigned i = 1; i < last; ++i)
+                for (app* v : arr_vars)
+                    if (occurs(v, a->get_arg(i)))
+                        return true;
+        }
+        return false;
+    }
     void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs = nullptr) {
         //don't use mbp_qel on some theories where model evaluation is
         //incomplete This is not a limitation of qel. Fix this either by
@@ -554,6 +589,15 @@ public:
     void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) {
         TRACE(qe, tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
 
+        // The array term-graph projection is unsound when an array variable to
+        // be eliminated occurs inside a select/store index. Fall back to the
+        // classic model-based projection in that case (issues #7259, #7036).
+        if (has_array_var_in_index(vars, fml)) {
+            TRACE(qe, tout << "array var in index: using model-based projection\n";);
+            spacer_qe_lite(vars, mdl, fml);
+            return;
+        }
+
         model_evaluator eval(mdl, m_params);
         eval.set_model_completion(true);
         app_ref_vector other_vars(m);