diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index 8d6705fb5..7551911a4 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -20,17 +20,12 @@ namespace polysat {
     bool ve_reduction::perform(solver& s, pvar v, conflict& core) {
         // without any further hints, we just do core reduction with the stronger premise "C contains a c' that evaluates to false",
         // and kick out all other constraints.
-        auto pred = [&s, v](signed_constraint c) -> bool {
-            return !c->contains_var(v) && c.is_currently_false(s);
-        };
-        auto it = std::find_if(core.begin(), core.end(), pred);
-        if (it != core.end()) {
-            signed_constraint c = *it;
-            core.reset();
-            core.set(c);
-            // core.insert(c);
-            // core.set_needs_model(true);
-            return true;
+        for (signed_constraint c : core) {
+            if (!c->contains_var(v) && c.is_currently_false(s)) {
+                core.reset();
+                core.set(c);
+                return true;
+            }                
         }
         return false;
     }