From 230ee01fe2cee007dfc9e25849d5cb8077a8d0e1 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 4 Dec 2025 16:55:49 -1000
Subject: [PATCH] call levelwise on a correct set of polynomials

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_explain.cpp | 11 +++++------
 src/nlsat/nlsat_solver.cpp  | 14 +++++++-------
 2 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 24a0c94ae..5b8b60c05 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1129,7 +1129,7 @@ namespace nlsat {
             bool first = true;
             if (ps.empty())
                 return;
-
+            TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);            
             m_todo.reset();
             for (unsigned i = 0; i < ps.size(); i++) {
                 polynomial_ref p(m_pm);
@@ -1140,19 +1140,18 @@ namespace nlsat {
             ps.reset();
             for (auto p: m_todo.m_set)
                 ps.push_back(p);
-            
-            var x = m_todo.extract_max_polys(ps);
 
-            TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";);
             if (m_solver.apply_levelwise()) {
                 bool levelwise_ok = levelwise_single_cell(ps, max_x, m_cache);
                 m_solver.record_levelwise_result(levelwise_ok);
                 if (levelwise_ok)
                     return;
-
             }
+            TRACE(nlsat_explain, ::nlsat::display(tout << "ps before extract:", m_solver, ps)<< "\n";);
+            var x = m_todo.extract_max_polys(ps);
+
+            TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
             polynomial_ref_vector samples(m_pm);
-            
             if (x < max_x)
                 cac_add_cell_lits(ps, x, samples);
 
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 84ddd8864..2a2f8322a 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1142,14 +1142,14 @@ namespace nlsat {
                     used_bools[b] = true;
                 vars.reset();
                 this->vars(lit, vars);
-                for (var v : vars)
+            for (var v : vars)
                         used_vars[v] = true;            
             }
-            display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
-            /*  if (m_lemma_count == 60) {
+            if (m_lemma_count >= 7 && false) {
                 enable_trace("lws");
-                enable_trace("nlsat_explain");
-                }*/
+                enable_trace("nlsat_explain");                
+            }
+            display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
             if (m_log_lemma_smtrat)
                 out << "(set-logic NRA)\n";
             else 
@@ -1163,10 +1163,10 @@ namespace nlsat {
             for (unsigned i = 0; i < n; ++i) 
                 display_smt2(out << "(assert ", ~cls[i]) << ")\n";
             out << "(check-sat)\n(reset)\n";
-            /*  if (m_lemma_count == 62) {                
+            if (m_lemma_count == 10 && false) {                
                 std::cout << "early exit\n";
                 exit(1);
-                } */  
+            }
         }
 
         clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {