diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 752f9006f0..15ce274b6e 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -424,10 +424,16 @@ public:
     // 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).
+    // array variable being eliminated) occurs *nested inside* a select/store
+    // *index* position, because the index is a first-class term whose value
+    // must be preserved and the merge can silently change it (for example
+    // (select va (= v va)) becomes (select v true), issues #7259, #7036).
+    //
+    // An array variable that appears *directly* as an index (e.g. the store
+    // index r in (store base r val)) is not affected by this rewrite: the
+    // index is exactly that variable and mbp_qel substitutes its model value
+    // soundly. Only flag the dangerous case where the variable occurs as a
+    // proper subterm of a compound index term.
     bool has_array_var_in_index(app_ref_vector const& vars, expr* fml) {
         array_util au(m);
         ptr_vector<app> arr_vars;
@@ -448,9 +454,11 @@ public:
             // 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)
-                if (any_of(arr_vars, [&](app* v) { return occurs(v, a->get_arg(i)); }))
+            for (unsigned i = 1; i < last; ++i) {
+                auto idx = a->get_arg(i);
+                if (any_of(arr_vars, [&](app* v) { return idx != v && occurs(v, idx); }))
                     return true;
+            }
         }
         return false;
     }