From e895cfb4ae8efc62ec7dccab4795f712a496e2f5 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 5 Dec 2025 06:13:37 -1000
Subject: [PATCH] cosmetics

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

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 5b8b60c05..d582524fb 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1129,7 +1129,6 @@ 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);
@@ -1147,10 +1146,7 @@ namespace nlsat {
                 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 2a2f8322a..48a50759f 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1145,10 +1145,6 @@ namespace nlsat {
             for (var v : vars)
                         used_vars[v] = true;            
             }
-            if (m_lemma_count >= 7 && false) {
-                enable_trace("lws");
-                enable_trace("nlsat_explain");                
-            }
             display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
             if (m_log_lemma_smtrat)
                 out << "(set-logic NRA)\n";
@@ -1163,10 +1159,6 @@ 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 == 10 && false) {                
-                std::cout << "early exit\n";
-                exit(1);
-            }
         }
 
         clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {