diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 460e07f58..be60fb052 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -42,7 +42,8 @@ namespace nlsat {
         bool                    m_simplify_cores;
         bool                    m_full_dimensional;
         bool                    m_minimize_cores;
-        
+        bool                    m_factor;
+
         struct todo_set {
             polynomial::cache  &    m_cache;
             polynomial_ref_vector   m_set;
@@ -568,21 +569,22 @@ namespace nlsat {
             elim_vanishing(p);
             if (is_const(p))
                 return;
-#if 1
-            TRACE("nlsat_explain", tout << "adding factors of\n"; display(tout, p); tout << "\n";);
-            factor(p, m_factors);
-            polynomial_ref f(m_pm);
-            for (unsigned i = 0; i < m_factors.size(); i++) {
-                f = m_factors.get(i);
-                elim_vanishing(f);
-                if (!is_const(f)) {
-                    TRACE("nlsat_explain", tout << "adding factor:\n"; display(tout, f); tout << "\n";);
-                    m_todo.insert(f);
+            if (m_factor) {
+                TRACE("nlsat_explain", tout << "adding factors of\n"; display(tout, p); tout << "\n";);
+                factor(p, m_factors);
+                polynomial_ref f(m_pm);
+                for (unsigned i = 0; i < m_factors.size(); i++) {
+                    f = m_factors.get(i);
+                    elim_vanishing(f);
+                    if (!is_const(f)) {
+                        TRACE("nlsat_explain", tout << "adding factor:\n"; display(tout, f); tout << "\n";);
+                        m_todo.insert(f);
+                    }
                 }
             }
-#else
-            m_todo.insert(normalize(p));
-#endif
+            else {
+                m_todo.insert(p);
+            }
         }
         
         /**
@@ -1344,6 +1346,10 @@ namespace nlsat {
         m_imp->m_minimize_cores = f;
     }
 
+    void explain::set_factor(bool f) {
+        m_imp->m_factor = f;
+    }
+
     void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) {
         (*m_imp)(n, ls, result);
     }
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index 5ecb9d385..85c598f73 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -40,6 +40,7 @@ namespace nlsat {
         void set_simplify_cores(bool f);
         void set_full_dimensional(bool f);
         void set_minimize_cores(bool f);
+        void set_factor(bool f);
 
         /**
            \brief Given a set of literals ls[0], ... ls[n-1] s.t.
diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index 4faad3379..6b1577113 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -10,5 +10,7 @@ def_module_params('nlsat',
                           ('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
                           ('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."),
                           ('shuffle_vars', BOOL, False, "use a random variable order."),
-                          ('seed', UINT, 0, "random seed.")))
+                          ('seed', UINT, 0, "random seed."),
+                          ('factor', BOOL, True, "factor polynomials produced during conflict resolution.")     
+                          ))         
                 
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 341431556..368e7eb83 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -212,6 +212,7 @@ namespace nlsat {
             m_ism.set_seed(m_random_seed);
             m_explain.set_simplify_cores(m_simplify_cores);
             m_explain.set_minimize_cores(min_cores);
+            m_explain.set_factor(p.factor());
             m_am.updt_params(p.p);
         }