3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00

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

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10282

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-29 09:07:17 -07:00 committed by GitHub
parent d46fbad3b6
commit 1fe251e19e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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<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