From 964dd2a71ae398149b4bcba27ce41318af735a64 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Aug 2025 07:46:53 -0700
Subject: [PATCH] fixup loop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_explain.cpp | 12 ++++++++----
 src/nlsat/nlsat_solver.cpp  | 31 ++++++++++++++-----------------
 2 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 19c6316d5..55c5f5315 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1303,7 +1303,8 @@ namespace nlsat {
                 // Temporarily unassign x, s.t. isolate_roots does not assume p as constant.
                 m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
                 unsigned num_roots = roots.size();
-                if (num_roots == 0) continue;
+                if (num_roots == 0) 
+                    continue;
 
                 // find p's smallest root above the sample
                 unsigned i = 0;
@@ -1319,7 +1320,8 @@ namespace nlsat {
                     p_lower = p;
                     i_lower = i+1;
                     break; // TODO: choose the best among multiple section polynomials?
-                } else if (s < 0) {
+                } 
+                else if (s < 0) {
                     // x_val < roots[i]
                     ps_above.push_back(p);
                     if (upper_inf || m_am.lt(roots[i], upper)) {
@@ -1348,7 +1350,8 @@ namespace nlsat {
                 if (!m_am.is_rational(x_val)) {
                     // TODO: FAIL
                     NOT_IMPLEMENTED_YET();
-                } else if (m_pm.total_degree(p_lower) > 1) {
+                } 
+                else if (m_pm.total_degree(p_lower) > 1) {
                     rational bound;
                     m_am.to_rational(x_val, bound);
                     p_lower = m_pm.mk_polynomial(x);
@@ -1446,7 +1449,8 @@ namespace nlsat {
                     // section
                     lb = ps_equal_sample.back();
                     psc_resultants_with(ps, lb, x);
-                } else {
+                } 
+                else {
                     if (!ps_below_sample.empty()) {
                         lb = ps_below_sample.back();
                         psc_resultants_with(ps_below_sample, lb, x);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 34109578c..8631fa0b8 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2044,22 +2044,24 @@ namespace nlsat {
             literal best_literal = null_literal;
             unsigned sz = m_clauses.size();
             lbool satisfied = l_true;
-            for (unsigned i = 0; i < sz; i++) {
-                bool c_satisfied = false;
-                clause const & c = *(m_clauses[i]);
-                for (literal l : c) {
-                    if (const_cast<imp*>(this)->value(l) != l_false) {
-                        c_satisfied = true;
-                        break;
-                    }
+            for (auto cp : m_clauses) {
+                auto& c = *cp;
+                bool is_false = all_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_false; });
+                bool is_true = any_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_true; });
+                if (is_true)
+                    continue;                
+                
+                if (!is_false) {
+                    satisfied = l_undef;
+                    continue;
                 }
-                if (c_satisfied) continue;
 
                 // take best literal from c
                 for (literal l : c) {
                     if (best_literal == null_literal) {
                         best_literal = l;
-                    } else {
+                    } 
+                    else {
                         bool_var b_best = best_literal.var();
                         bool_var b_l = l.var();
                         if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) {
@@ -2070,14 +2072,9 @@ namespace nlsat {
                 }
             }
 
-            if (satisfied == l_true) {
-                // nothing to do
-                return l_true;
-            }
-            if (satisfied == l_undef) {
-                // nothing to do?
+            if (best_literal == null_literal)
+                return satisfied;
                 return l_undef;
-            }
 
             // assignment does not satisfy the constraints -> create lemma
             SASSERT(best_literal != null_literal);