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