diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 9da662566..3afad027b 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -508,6 +508,8 @@ namespace nlsat {
         }
 
         void normalize(polynomial_ref & p) {
+            if (!m_solver.lws_norm())
+                return;
             unsigned level = max_var(p);
             if (find_in_Q(p, level)) return;
             TRACE(lws_norm, tout << "p:" << p << std::endl;);
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index b780a651b..ec55ca561 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -24,5 +24,6 @@ def_module_params('nlsat',
                           ('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."),
                           ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
                           ('apply_levelwise', BOOL, True, "apply levelwise."),
+                          ('lws_norm', BOOL, True, "normalize polynomials in levelwise."),
                           ('canonicalize', BOOL, True, "canonicalize polynomials.")
                           ))         
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 6e0550fde..9c25d6d91 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -248,6 +248,7 @@ namespace nlsat {
         stats                  m_stats;
         std::string m_debug_known_solution_file_name;
         bool m_apply_lws;
+        bool m_lws_norm;
         imp(solver& s, ctx& c):
             m_ctx(c),
             m_solver(s),
@@ -308,6 +309,7 @@ namespace nlsat {
             m_variable_ordering_strategy = p.variable_ordering_strategy();
             m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
             m_apply_lws = p.apply_levelwise();
+            m_lws_norm = p.lws_norm();
             m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
             m_cell_sample = p.cell_sample();
   
@@ -4635,6 +4637,7 @@ namespace nlsat {
     }
 
     bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
+    bool solver::lws_norm() const { return m_imp->m_lws_norm; }
 
         
 };
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index b1cc29179..a40c2d4d0 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -248,6 +248,7 @@ namespace nlsat {
         const assignment& sample() const;
         assignment& sample(); 
         bool apply_levelwise() const;
+        bool lws_norm() const;
         void reset();
         void collect_statistics(statistics & st);
         void reset_statistics();