diff --git a/src/math/lp/factorization.cpp b/src/math/lp/factorization.cpp
index c4e8fb90b..f81a011dc 100644
--- a/src/math/lp/factorization.cpp
+++ b/src/math/lp/factorization.cpp
@@ -23,21 +23,30 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
     std::sort(k_vars.begin(), k_vars.end());
     std::sort(j_vars.begin(), j_vars.end());
 
+    if (false && m_num_failures > 10) {
+        for (bool& m : m_mask) m = true;
+        m_mask[0] = false;
+        m_full_factorization_returned = true;
+        return false;
+    }
     if (k_vars.size() == 1) {
         k.set(k_vars[0], factor_type::VAR);
     } else {
         unsigned i;
         if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) {
+            ++m_num_failures;
             return false;
         }
         k.set(i, factor_type::MON);
     }
+    m_num_failures = 0;
 
     if (j_vars.size() == 1) {
         j.set(j_vars[0], factor_type::VAR);
     } else {
         unsigned i;
         if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) {
+            ++m_num_failures;
             return false;
         }
         j.set(i, factor_type::MON);
@@ -46,7 +55,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
 }
 
 factorization const_iterator_mon::operator*() const {
-    if (m_full_factorization_returned == false)  {
+    if (!m_full_factorization_returned)  {
         return create_full_factorization(m_ff->m_monic);
     }
     factor j, k; rational sign;
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index 78f3ab1a4..a021a2a36 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -30,12 +30,12 @@ struct factorization_factory;
 enum class factor_type { VAR, MON };
 
 class factor {
-    lpvar        m_var;
-    factor_type  m_type;
-    bool        m_sign;
+    lpvar        m_var{ UINT_MAX };
+    factor_type  m_type{ factor_type::VAR };
+    bool         m_sign{ false };
 public:
     factor(): factor(false) {}
-    factor(bool sign): m_var(UINT_MAX), m_type(factor_type::VAR), m_sign(sign) {}
+    factor(bool sign): m_sign(sign) {}
     explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
     unsigned var() const { return m_var; }
     factor_type type() const { return m_type; }
@@ -77,9 +77,10 @@ public:
 
 struct const_iterator_mon {
     // fields
-    bool_vector                  m_mask;
+    mutable bool_vector                    m_mask;
     const factorization_factory *  m_ff;
-    bool                           m_full_factorization_returned;
+    mutable bool                           m_full_factorization_returned;
+    mutable unsigned               m_num_failures{ 0 };
 
     // typedefs
     typedef const_iterator_mon self_type;