Fix #7259, #7036: unsound MBP array projection with array var in select/store index

The array term-graph projection (mbp_qel) treats an array equality (= a b)
as an implicit partial array equality and eliminates it by merging the
array variable's congruence class. That rewrite is unsound when the array
variable being eliminated occurs inside a select/store index position,
because the index is a first-class term whose value must be preserved.

For example, (select va (= v va)) was rewritten to (select v true) after
merging va into v, turning a model-false literal into a model-true one and
triggering the qe_mbp validation assertions (qe_mbp.cpp:412 for #7259,
qe_mbp.cpp:622 for #7036), or a crash at qsat.cpp:579 in release builds.

Detect when an array variable to be eliminated occurs inside a select or
store index and fall back to the classic model-based projection
(spacer_qe_lite) for such formulas. Both reproducers now return the correct
unsat verdict with no assertion failure, and all unit tests pass.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9

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);