diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 57483deb4..5bafdc68b 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -270,6 +270,8 @@ namespace nlsat {
                     tout << "Level " << m_level << " SECTOR: rfunc.size=" << m_rel.m_rfunc.size()
                          << " < 2, using default heuristic\n";
                 );
+                // Clear m_omit_lc to avoid using stale values from a previous level
+                m_omit_lc.clear();
                 return m_sector_relation_mode;
             }
 
@@ -331,6 +333,8 @@ namespace nlsat {
                     tout << "Level " << m_level << " SECTION: rfunc.size=" << m_rel.m_rfunc.size()
                          << " < 2, using default heuristic\n";
                 );
+                // Clear m_omit_lc to avoid using stale values from a previous level
+                m_omit_lc.clear();
                 return m_section_relation_mode;
             }
 
@@ -504,6 +508,11 @@ namespace nlsat {
 
         void request_factorized(polynomial_ref const& poly, inv_req req) {
             for_each_distinct_factor(poly, [&](polynomial_ref const& f) {
+                TRACE(lws,
+                    tout << "      request_factorized: factor=";
+                    m_pm.display(tout, f);
+                    tout << " at level " << m_pm.max_var(f) << "\n";
+                );
                 request(f.get(), req); // inherit tag across factorization (SMT-RAT appendOnCorrectLevel)
             });
         }
@@ -577,6 +586,11 @@ namespace nlsat {
         }
 
         void add_projections_for(polynomial_ref const& p, unsigned x, polynomial_ref const& nonzero_coeff, bool add_leading_coeff, bool add_discriminant) {
+            TRACE(lws,
+                tout << "  add_projections_for: p=";
+                m_pm.display(tout, p);
+                tout << " x=" << x << " add_lc=" << add_leading_coeff << " add_disc=" << add_discriminant << "\n";
+            );
             // Line 11 (non-null witness coefficient)
             if (nonzero_coeff && !is_const(nonzero_coeff))
                 request_factorized(nonzero_coeff, inv_req::sign);
@@ -588,6 +602,11 @@ namespace nlsat {
                 unsigned deg = m_pm.degree(p, x);
                 polynomial_ref lc(m_pm);
                 lc = m_pm.coeff(p, x, deg);
+                TRACE(lws,
+                    tout << "    adding lc: ";
+                    m_pm.display(tout, lc);
+                    tout << "\n";
+                );
                 request_factorized(lc, inv_req::sign);
             }
         }
@@ -774,18 +793,29 @@ namespace nlsat {
 
         // Relation construction heuristics (same intent as previous implementation).
         void fill_relation_with_biggest_cell_heuristic() {
+            TRACE(lws,
+                tout << "  fill_biggest_cell: m_l_rf=" << m_l_rf << ", m_u_rf=" << m_u_rf << ", rfunc.size=" << m_rel.m_rfunc.size() << "\n";
+            );
             if (is_set(m_l_rf))
-                for (unsigned j = 0; j < m_l_rf; ++j)
+                for (unsigned j = 0; j < m_l_rf; ++j) {
+                    TRACE(lws, tout << "    add_pair(" << j << ", " << m_l_rf << ")\n";);
                     m_rel.add_pair(j, m_l_rf);
+                }
 
             if (is_set(m_u_rf))
-                for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j)
+                for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j) {
+                    TRACE(lws, tout << "    add_pair(" << m_u_rf << ", " << j << ")\n";);
                     m_rel.add_pair(m_u_rf, j);
+                }
 
             if (is_set(m_l_rf) && is_set(m_u_rf)) {
                 SASSERT(m_l_rf + 1 == m_u_rf);
+                TRACE(lws, tout << "    add_pair(" << m_l_rf << ", " << m_u_rf << ")\n";);
                 m_rel.add_pair(m_l_rf, m_u_rf);
             }
+            TRACE(lws,
+                tout << "  fill_biggest_cell done: pairs.size=" << m_rel.m_pairs.size() << "\n";
+            );
         }
 
         void fill_relation_with_chain_heuristic() {
@@ -1338,10 +1368,31 @@ namespace nlsat {
 
 
         void add_relation_resultants() {
+            TRACE(lws,
+                tout << "  add_relation_resultants: " << m_rel.m_pairs.size() << " pairs\n";
+            );
             for (auto const& pr : m_rel.m_pairs) {
                 poly* p1 = m_level_ps.get(pr.first);
                 poly* p2 = m_level_ps.get(pr.second);
-                request_factorized(psc_resultant(p1, p2, m_level), inv_req::ord);
+                TRACE(lws,
+                    tout << "    resultant(" << pr.first << ", " << pr.second << "): ";
+                    m_pm.display(tout, p1);
+                    tout << " and ";
+                    m_pm.display(tout, p2);
+                    tout << "\n";
+                );
+                polynomial_ref res = psc_resultant(p1, p2, m_level);
+                TRACE(lws,
+                    tout << "      resultant poly: ";
+                    if (res) {
+                        m_pm.display(tout, res);
+                        tout << "\n      resultant sign at sample: " << m_am.eval_sign_at(res, sample());
+                    } else {
+                        tout << "(null)";
+                    }
+                    tout << "\n";
+                );
+                request_factorized(res, inv_req::ord);
             }
         }
 
@@ -1393,6 +1444,20 @@ namespace nlsat {
         }
 
         void add_level_projections_sector() {
+            TRACE(lws,
+                tout << "\n  add_level_projections_sector at level " << m_level << "\n";
+                tout << "  Lower bound rf=" << m_l_rf << ", Upper bound rf=" << m_u_rf << "\n";
+                if (is_set(m_l_rf)) {
+                    tout << "    lower poly idx=" << m_rel.m_rfunc[m_l_rf].ps_idx << ": ";
+                    m_pm.display(tout, m_level_ps.get(m_rel.m_rfunc[m_l_rf].ps_idx));
+                    tout << "\n";
+                }
+                if (is_set(m_u_rf)) {
+                    tout << "    upper poly idx=" << m_rel.m_rfunc[m_u_rf].ps_idx << ": ";
+                    m_pm.display(tout, m_level_ps.get(m_rel.m_rfunc[m_u_rf].ps_idx));
+                    tout << "\n";
+                }
+            );
             // Lines 11-12 (Algorithm 1): add projections for each p
             // Note: Algorithm 1 adds disc + ldcf for ALL polynomials (classical delineability)
             // We additionally omit leading coefficients for rootless polynomials when possible
@@ -1407,6 +1472,19 @@ namespace nlsat {
                 lc = m_pm.coeff(p, m_level, deg);
 
                 bool add_lc = (i >= m_omit_lc.size() || !m_omit_lc[i]);
+                bool is_lower_bound = is_set(m_l_rf) && i == m_rel.m_rfunc[m_l_rf].ps_idx;
+                bool is_upper_bound = is_set(m_u_rf) && i == m_rel.m_rfunc[m_u_rf].ps_idx;
+
+                // Per Algorithm 2, Line 13 of projective_delineability.pdf:
+                // Bound-defining polynomials MUST have their LC projected for delineability
+                if (is_lower_bound || is_upper_bound)
+                    add_lc = true;
+
+                TRACE(lws,
+                    tout << "  poly[" << i << "] is_lower=" << is_lower_bound << " is_upper=" << is_upper_bound;
+                    tout << " omit_lc[i]=" << (i < m_omit_lc.size() ? (m_omit_lc[i] ? "true" : "false") : "N/A");
+                    tout << " add_lc=" << add_lc << "\n";
+                );
 
                 if (add_lc && i < usize(m_poly_has_roots) && !m_poly_has_roots[i])
                     if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
@@ -1559,6 +1637,16 @@ namespace nlsat {
         }
 
         void process_level() {
+            TRACE(lws,
+                tout << "\n--- process_level: level=" << m_level << " ---\n";
+                tout << "Polynomials at this level (" << m_level_ps.size() << "):\n";
+                for (unsigned i = 0; i < m_level_ps.size(); ++i) {
+                    tout << "  ps[" << i << "]: ";
+                    m_pm.display(tout, m_level_ps.get(i));
+                    tout << "\n";
+                }
+            );
+
             // Line 10/11: detect nullification + pick a non-zero coefficient witness per p.
             m_witnesses.clear();
             m_witnesses.reserve(m_level_ps.size());
@@ -1572,6 +1660,20 @@ namespace nlsat {
 
             // Lines 3-8: Θ + I_level + relation ≼
             bool have_interval = build_interval();
+
+            TRACE(lws,
+                tout << "Interval: ";
+                display(tout, m_solver, m_I[m_level]);
+                tout << "\n";
+                tout << "Section? " << (m_I[m_level].section ? "yes" : "no") << "\n";
+                tout << "have_interval=" << have_interval << ", rfunc.size=" << m_rel.m_rfunc.size() << "\n";
+                for (unsigned i = 0; i < m_rel.m_rfunc.size(); ++i) {
+                    tout << "  rfunc[" << i << "]: ps_idx=" << m_rel.m_rfunc[i].ps_idx << ", val=";
+                    m_am.display(tout, m_rel.m_rfunc[i].val);
+                    tout << "\n";
+                }
+            );
+
             if (m_I[m_level].section)
                 process_level_section(have_interval);
             else
@@ -1579,6 +1681,16 @@ namespace nlsat {
         }
 
         void process_top_level() {
+            TRACE(lws,
+                tout << "\n--- process_top_level: level=" << m_n << " ---\n";
+                tout << "Polynomials at top level (" << m_level_ps.size() << "):\n";
+                for (unsigned i = 0; i < m_level_ps.size(); ++i) {
+                    tout << "  ps[" << i << "]: ";
+                    m_pm.display(tout, m_level_ps.get(i));
+                    tout << "\n";
+                }
+            );
+
             m_witnesses.clear();
             m_witnesses.reserve(m_level_ps.size());
             for (unsigned i = 0; i < m_level_ps.size(); ++i) {
@@ -1619,6 +1731,21 @@ namespace nlsat {
         }
 
         std_vector<root_function_interval> single_cell_work() {
+            TRACE(lws,             
+                tout << "Input polynomials (" << m_P.size() << "):\n";
+                for (unsigned i = 0; i < m_P.size(); ++i) {
+                    tout << "  p[" << i << "]: ";
+                    m_pm.display(tout, m_P.get(i));
+                    tout << "\n";
+                }
+                tout << "Sample values:\n";
+                for (unsigned j = 0; j < m_n; ++j) {
+                    tout << "  x" << j << " = ";
+                    m_am.display(tout, sample().value(j));
+                    tout << "\n";
+                }
+            );
+
             if (m_n == 0)
                 return m_I;
 
@@ -1646,8 +1773,21 @@ namespace nlsat {
                 extract_max_tagged();
                 SASSERT(m_level < m_n);
                 process_level();
+                TRACE(lws,
+                    tout << "After level " << m_level << ": m_todo.empty()=" << m_todo.empty();
+                    if (!m_todo.empty()) tout << ", m_todo.max_var()=" << m_todo.max_var();
+                    tout << "\n";
+                );
             }
 
+            TRACE(lws,
+                for (unsigned i = 0; i < m_I.size(); ++i) {
+                    tout << "I[" << i << "]: ";
+                    display(tout, m_solver, m_I[i]);
+                    tout << "\n";
+                }
+            );
+
             return m_I;
         }
 
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index a3155f494..f1a7a4ca8 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -50,7 +50,6 @@ namespace nlsat {
         bool                    m_factor;
         bool                    m_add_all_coeffs;
         bool                    m_add_zero_disc;
-        bool                    m_sample_cell_project;
 
         assignment const &      sample() const { return m_solver.sample(); }
         assignment &            sample() { return m_solver.sample(); }
@@ -142,7 +141,7 @@ namespace nlsat {
         evaluator &             m_evaluator;
 
         imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
-            evaluator & ev, bool sample_cell_project, bool canonicalize):
+            evaluator & ev, bool canonicalize):
             m_solver(s),
             m_atoms(atoms),
             m_x2eq(x2eq),
@@ -155,7 +154,6 @@ namespace nlsat {
             m_factors(m_pm),
             m_factors_save(m_pm),
             m_roots_tmp(m_am),
-            m_sample_cell_project(sample_cell_project),
             m_todo(u, canonicalize),
             m_core1(s),
             m_core2(s),
@@ -1083,35 +1081,6 @@ namespace nlsat {
            \brief Apply model-based projection operation defined in our paper.
         */
 
-        void project_original(polynomial_ref_vector & ps, var max_x) {
-            if (ps.empty())
-                return;
-            m_todo.reset();
-            for (poly* p : ps) {
-                m_todo.insert(p);
-            }
-            var x = m_todo.extract_max_polys(ps);
-            // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
-            if (x < max_x)
-                add_cell_lits(ps, x);
-            while (true) {
-                if (all_univ(ps, x) && m_todo.empty()) {
-                    m_todo.reset();
-                    break;
-                }
-                TRACE(nlsat_explain, tout << "project loop, processing var "; m_solver.display_var(tout, x); 
-                tout << "\npolynomials\n";
-                display(tout, m_solver, ps); tout << "\n";);
-                add_lcs(ps, x);
-                psc_discriminant(ps, x);
-                psc_resultant(ps, x);
-                if (m_todo.empty())
-                    break;
-                x = m_todo.extract_max_polys(ps);
-                add_cell_lits(ps, x);
-            }
-        }
-
         bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
             levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
             auto cell = lws.single_cell();
@@ -1208,12 +1177,7 @@ namespace nlsat {
         }
 
         void project(polynomial_ref_vector & ps, var max_x) {
-            if (m_sample_cell_project) {
-                project_cdcac(ps, max_x);
-            }
-            else {
-                project_original(ps, max_x);
-            }
+            project_cdcac(ps, max_x);
         }
 
         bool check_already_added() const {
@@ -1906,8 +1870,8 @@ namespace nlsat {
     };
 
     explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, 
-                     atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample, bool canonicalize) {
-        m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample, canonicalize);
+                     atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool canonicalize) {
+        m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, canonicalize);
     }
 
     explain::~explain() {
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index 41dd1c2c5..2fe967efb 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -35,7 +35,7 @@ namespace nlsat {
         imp * m_imp;
     public:
         explain(solver & s, assignment const & x2v, polynomial::cache & u, 
-                atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj, bool canonicalize);
+                atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool canonicalize);
 
         ~explain();
 
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index a2c0d8f25..21d6221d6 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -5,7 +5,6 @@ def_module_params('nlsat',
                   params=(max_memory_param(),
                           ('simple_check', BOOL, False, "precheck polynomials using variables sign"),
                           ('variable_ordering_strategy', UINT, 0, "Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"),
-                          ('cell_sample', BOOL, True, "cell sample projection"),
                           ('lazy', UINT, 0, "how lazy the solver is."),
                           ('reorder', BOOL, True, "reorder variables."),
                           ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 6fd2d318a..43e119624 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -231,7 +231,6 @@ namespace nlsat {
         unsigned               m_lemma_count;
         unsigned m_variable_ordering_strategy;
         bool m_set_0_more;
-        bool m_cell_sample;
 
         struct stats {
             unsigned               m_simplifications;
@@ -277,7 +276,7 @@ namespace nlsat {
             m_simplify(s, m_atoms, m_clauses, m_learned, m_pm),
             m_display_var(m_perm),
             m_display_assumption(nullptr),
-            m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).cell_sample(), nlsat_params(c.m_params).canonicalize()),
+            m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).canonicalize()),
             m_scope_lvl(0),
             m_lemma(s),
             m_lazy_clause(s),
@@ -327,7 +326,6 @@ namespace nlsat {
             m_lws_dynamic_heuristic = p.lws_dynamic_heuristic();
             m_lws_spt_threshold = std::max(2u, p.lws_spt_threshold());
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
-            m_cell_sample = p.cell_sample();
   
             m_ism.set_seed(m_random_seed);
             m_explain.set_simplify_cores(m_simplify_cores);
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index ee1aaca9b..2684abb49 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -1056,7 +1056,117 @@ static void tst_nullified_polynomial() {
     ENSURE(lws.failed());
 }
 
+// Test case for unsound lemma lws2380 - comparing standard projection vs levelwise
+// The issue: x7 is unconstrained in levelwise output but affects the section polynomial
+static void tst_unsound_lws2380() {
+    enable_trace("nlsat_explain");
+    
+    auto run_test = [](bool use_lws) {
+        std::cout << "=== tst_unsound_lws2380: " << (use_lws ? "Levelwise" : "Standard") << " projection (lws=" << use_lws << ") ===\n";
+        params_ref      ps;
+        ps.set_bool("lws", use_lws);
+        reslimit        rlim;
+        nlsat::solver s(rlim, ps, false);
+        anum_manager & am     = s.am();
+        nlsat::pmanager & pm  = s.pm();
+        nlsat::assignment as(am);
+        nlsat::explain& ex    = s.get_explain();
+
+        // Create 14 variables x0-x13
+        nlsat::var x0 = s.mk_var(false);
+        nlsat::var x1 = s.mk_var(false);
+        nlsat::var x2 = s.mk_var(false);
+        nlsat::var x3 = s.mk_var(false);
+        nlsat::var x4 = s.mk_var(false);
+        nlsat::var x5 = s.mk_var(false);
+        nlsat::var x6 = s.mk_var(false);
+        nlsat::var x7 = s.mk_var(false);
+        nlsat::var x8 = s.mk_var(false);
+        nlsat::var x9 = s.mk_var(false);
+        nlsat::var x10 = s.mk_var(false);
+        nlsat::var x11 = s.mk_var(false);
+        nlsat::var x12 = s.mk_var(false);
+        nlsat::var x13 = s.mk_var(false);
+
+        polynomial_ref _x0(pm), _x1(pm), _x2(pm), _x3(pm), _x4(pm), _x5(pm), _x6(pm);
+        polynomial_ref _x7(pm), _x8(pm), _x9(pm), _x10(pm), _x11(pm), _x12(pm), _x13(pm);
+        _x0 = pm.mk_polynomial(x0);
+        _x1 = pm.mk_polynomial(x1);
+        _x2 = pm.mk_polynomial(x2);
+        _x3 = pm.mk_polynomial(x3);
+        _x4 = pm.mk_polynomial(x4);
+        _x5 = pm.mk_polynomial(x5);
+        _x6 = pm.mk_polynomial(x6);
+        _x7 = pm.mk_polynomial(x7);
+        _x8 = pm.mk_polynomial(x8);
+        _x9 = pm.mk_polynomial(x9);
+        _x10 = pm.mk_polynomial(x10);
+        _x11 = pm.mk_polynomial(x11);
+        _x12 = pm.mk_polynomial(x12);
+        _x13 = pm.mk_polynomial(x13);
+
+        // p[0]: x13
+        polynomial_ref p0(pm);
+        p0 = _x13;
+
+        // p[1]: 170*x8*x13 + x10*x11*x12 - x11*x12 - x7*x8*x12 + x5*x10*x11 + 184*x1*x10*x11
+        //       - x0*x10*x11 - x5*x11 - 184*x1*x11 + x0*x11 - x3*x8*x10 + x2*x8*x10
+        //       - 2*x10 - 184*x1*x7*x8 - x2*x8 + 2
+        polynomial_ref p1(pm);
+        p1 = (170 * _x8 * _x13) +
+             (_x10 * _x11 * _x12) -
+             (_x11 * _x12) -
+             (_x7 * _x8 * _x12) +
+             (_x5 * _x10 * _x11) +
+             (184 * _x1 * _x10 * _x11) -
+             (_x0 * _x10 * _x11) -
+             (_x5 * _x11) -
+             (184 * _x1 * _x11) +
+             (_x0 * _x11) -
+             (_x3 * _x8 * _x10) +
+             (_x2 * _x8 * _x10) -
+             (2 * _x10) -
+             (184 * _x1 * _x7 * _x8) -
+             (_x2 * _x8) +
+             2;
+
+        std::cout << "p0: " << p0 << "\n";
+        std::cout << "p1: " << p1 << "\n";
+
+        // Set sample: x0=-1, x1=-1, x2=0, x3=-1, x5=0, x7=0, x8=2, x10=0, x11=0, x12=2
+        scoped_anum val(am);
+        am.set(val, -1); as.set(x0, val);
+        am.set(val, -1); as.set(x1, val);
+        am.set(val, 0);  as.set(x2, val);
+        am.set(val, -1); as.set(x3, val);
+        am.set(val, 0);  as.set(x4, val);
+        am.set(val, 0);  as.set(x5, val);
+        am.set(val, 0);  as.set(x6, val);
+        am.set(val, 0);  as.set(x7, val);
+        am.set(val, 2);  as.set(x8, val);
+        am.set(val, 0);  as.set(x9, val);
+        am.set(val, 0);  as.set(x10, val);
+        am.set(val, 0);  as.set(x11, val);
+        am.set(val, 2);  as.set(x12, val);
+        am.set(val, 1);  as.set(x13, val);
+        s.set_rvalues(as);
+
+        // Create literals for the two polynomials
+        nlsat::scoped_literal_vector lits(s);
+        lits.push_back(mk_gt(s, p0.get()));  // x13 > 0
+        lits.push_back(mk_gt(s, p1.get()));  // p1 > 0
+
+        project_fa(s, ex, x13, lits.size(), lits.data());
+        std::cout << "\n";
+    };
+
+    run_test(false);  // Standard projection
+    run_test(true);   // Levelwise projection
+}
+
 void tst_nlsat() {
+    tst_unsound_lws2380();
+    std::cout << "------------------\n";
     tst_polynomial_cache_mk_unique();
     std::cout << "------------------\n";
     tst_nullified_polynomial();