diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 5c6981004..1edd0f41a 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -57,8 +57,6 @@ namespace nlsat {
 
         unsigned               m_level = 0;      // current level being processed
         unsigned               m_spanning_tree_threshold = 3; // minimum both-side count for spanning tree
-        bool                   m_null_fail = false;
-        bool                   m_fail = false;
         unsigned               m_l_rf = UINT_MAX; // position of lower bound in m_rel.m_rfunc
         unsigned               m_u_rf = UINT_MAX; // position of upper bound in m_rel.m_rfunc, UINT_MAX in section case
 
@@ -264,7 +262,6 @@ namespace nlsat {
                 m_I.emplace_back(m_pm);
 
             m_spanning_tree_threshold = m_solver.lws_spt_threshold();
-            m_null_fail = m_solver.lws_null_fail();
         }
 
         // Handle a polynomial whose every coefficient evaluates to zero at the sample.
@@ -272,9 +269,7 @@ namespace nlsat {
         // request_factorized each of them and continue to the next level.
         // When a non-vanishing derivative is found, request_factorized it and stop.
         void handle_nullified_poly(polynomial_ref const& p) {
-            if (m_null_fail)
-                throw nullified_poly_exception();
-            // Add all coefficients of p (w.r.t. m_level) to m_todo.
+            // Add all coefficients of p as a polynomial of x_{m_level} to m_todo.
             unsigned deg = m_pm.degree(p, m_level);
             for (unsigned j = 0; j <= deg; ++j) {
                 polynomial_ref coeff(m_pm.coeff(p, m_level, j), m_pm);
@@ -1302,7 +1297,7 @@ namespace nlsat {
             }
         }
 
-        std_vector<root_function_interval> single_cell_work() {
+        std_vector<root_function_interval> single_cell() {
             TRACE(lws,             
                   tout << "Input polynomials (" << m_P.size() << "):\n";
                   for (unsigned i = 0; i < m_P.size(); ++i)
@@ -1350,15 +1345,6 @@ namespace nlsat {
             return m_I;
         }
 
-        std_vector<root_function_interval> single_cell() {
-            try {
-                return single_cell_work();
-            }
-            catch (nullified_poly_exception&) {
-                m_fail = true;
-                return m_I;
-            }
-        }
     };
 
     levelwise::levelwise(
@@ -1376,9 +1362,6 @@ namespace nlsat {
     std_vector<levelwise::root_function_interval> levelwise::single_cell() {
         return m_impl->single_cell();
     }
-
-    bool levelwise::failed() const { return m_impl->m_fail; }
-
 } // namespace nlsat
 
 // Free pretty-printer for symbolic_interval
diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h
index 27e379374..950bee641 100644
--- a/src/nlsat/levelwise.h
+++ b/src/nlsat/levelwise.h
@@ -46,7 +46,6 @@ namespace nlsat {
         levelwise(levelwise const&) = delete;
         levelwise& operator=(levelwise const&) = delete;
         std_vector<root_function_interval> single_cell();
-        bool failed() const;
     };
 
     //
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 3240cae2a..d5aadf683 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -1048,8 +1048,6 @@ namespace nlsat {
             
             levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
             auto cell = lws.single_cell();
-            if (lws.failed())
-                return false;
             TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
                                  display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
             // Enumerate all intervals in the computed cell and add literals for each non-trivial interval.
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index 9d1ed45fc..1ab305984 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -24,6 +24,5 @@ def_module_params('nlsat',
                           ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
                           ('lws', BOOL, True, "apply levelwise."),
                           ('lws_spt_threshold', UINT, 2, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"),
-                          ('lws_null_fail', BOOL, False, "fail levelwise projection on nullified polynomials and fall back to standard projection."),
                           ('canonicalize', BOOL, True, "canonicalize polynomials.")
                           ))                  
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index eba014358..3d595b919 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -313,7 +313,6 @@ namespace nlsat {
             m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
             m_apply_lws = p.lws();
             m_lws_spt_threshold = p.lws_spt_threshold();  // 0 disables spanning tree
-            m_lws_null_fail = p.lws_null_fail();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
   
             m_ism.set_seed(m_random_seed);