From 1fe251e19ef23d409b23e50644dff5a11a98ad79 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:07:17 -0700 Subject: [PATCH] Simplify `has_array_var_in_index` in `qe_mbp.cpp` (#10289) This refines the recently added `has_array_var_in_index` helper in `src/qe/qe_mbp.cpp` to match the surrounding style without changing behavior. The array-index guard remains identical; the implementation is just expressed more consistently. - **What changed** - Replaced the nested `for`/`if` occurrence check with the local `any_of(...)` pattern already used nearby in `has_unsupported_th`. - Added the missing blank line before `operator()` to align with spacing used between other methods in the class. - **Behavior** - No functional change intended. - The helper still returns `true` as soon as any array variable occurs in a `select`/`store` index position. - **Example** ```c++ for (unsigned i = 1; i < last; ++i) if (any_of(arr_vars, [&](app* v) { return occurs(v, a->get_arg(i)); })) return true; ``` - Fixes #10282 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/qe/qe_mbp.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index fbcff6f28b..752f9006f0 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -449,12 +449,12 @@ public: 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; + if (any_of(arr_vars, [&](app* v) { return 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* 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