diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index aaf66979b..1d139338a 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -15,7 +15,7 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
     }
 }
             
-bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) const {
+bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const {
     unsigned_vector k_vars;
     unsigned_vector j_vars;
     init_vars_by_the_mask(k_vars, j_vars);
@@ -23,27 +23,29 @@ bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) c
     std::sort(k_vars.begin(), k_vars.end());
     std::sort(j_vars.begin(), j_vars.end());
 
-    rational k_sign, j_sign;
-    monomial m;
     if (k_vars.size() == 1) {
-        k = k_vars[0];
-        k_sign = 1;
+        k.index() = k_vars[0];
+        k.type() = factor_type::VAR;
     } else {
-        if (!m_ff->find_monomial_of_vars(k_vars, m, k_sign)) {
+        unsigned i;
+        if (!m_ff->find_monomial_of_vars(k_vars,i)) {
             return false;
         }
-        k = m.var();
+        k.index() = i;
+        k.type() = factor_type::RM;
     }
+
     if (j_vars.size() == 1) {
-        j = j_vars[0];
-        j_sign = 1;
+        j.index() = j_vars[0];
+        j.type() = factor_type::VAR;
     } else {
-        if (!m_ff->find_monomial_of_vars(j_vars, m, j_sign)) {
+        unsigned i;
+        if (!m_ff->find_monomial_of_vars(j_vars,i)) {
             return false;
         }
-        j = m.var();
+        j.index() = i;
+        j.type() = factor_type::RM;
     }
-    sign = j_sign * k_sign;
     return true;
 }
 
@@ -51,7 +53,7 @@ const_iterator_mon::reference const_iterator_mon::operator*() const {
     if (m_full_factorization_returned == false)  {
         return create_full_factorization();
     }
-    unsigned j, k; rational sign;
+    factor j, k; rational sign;
     if (!get_factors(j, k, sign))
         return factorization();
     return create_binary_factorization(j, k);
@@ -90,7 +92,7 @@ bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other)
 }
 bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); }
             
-factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k) const {
+factorization const_iterator_mon::create_binary_factorization(factor j, factor k) const {
     // todo : the current explanation is an overkill
     // std::function<void (expl_set&)> explain = [&](expl_set& exp){
     //                                               const imp & impl = m_ff->m_impf;
@@ -105,14 +107,17 @@ factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k)
     //                                               impl.add_explanation_of_reducing_to_rooted_monomial(m_ff->m_mon, exp);
     //                                           };
     factorization f;
-    f.vars().push_back(j);
-    f.vars().push_back(k);  
+    f.push_back(j);
+    f.push_back(k);  
     return f;
 }
 
 factorization const_iterator_mon::create_full_factorization() const {
     factorization f;
-    f.vars() = m_ff->m_vars; 
+    //    f.vars() = m_ff->m_vars;
+    for (lpvar j : m_ff->m_vars) {
+        f.push_back(factor(j, factor_type::VAR));
+    }
     return f;
 }
 }
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 59c9c2bcf..d13b7f9e5 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -26,16 +26,30 @@ namespace nla {
 struct factorization_factory;
 typedef unsigned lpvar;
 
+enum class factor_type { VAR, RM}; // RM stands for rooted monomial 
+
+class factor {
+    unsigned     m_index;
+    factor_type  m_type;
+public:
+    factor() {}
+    factor(unsigned i, factor_type t) : m_index(i), m_type(t) {}
+    unsigned index() const {return m_index;}
+    unsigned& index() {return m_index;}
+    factor_type type() const {return m_type;}
+    factor_type& type() {return m_type;}
+};
+
 class factorization {
-    svector<lpvar>         m_vars;
+    vector<factor>         m_vars;
 public:
     bool is_empty() const { return m_vars.empty(); }
-    svector<lpvar> & vars() { return m_vars; }
-    const svector<lpvar> & vars() const { return m_vars; }
-    unsigned operator[](unsigned k) const { return m_vars[k]; }
+    const vector<factor> & vars() const { return m_vars; }
+    factor operator[](unsigned k) const { return m_vars[k]; }
     size_t size() const { return m_vars.size(); }
-    const lpvar* begin() const { return m_vars.begin(); }
-    const lpvar* end() const { return m_vars.end(); }
+    const factor* begin() const { return m_vars.begin(); }
+    const factor* end() const { return m_vars.end(); }
+    void push_back(factor v) {m_vars.push_back(v);}
 };
 
 struct const_iterator_mon {
@@ -53,7 +67,7 @@ struct const_iterator_mon {
 
     void init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const;
             
-    bool get_factors(unsigned& k, unsigned& j, rational& sign) const;
+    bool get_factors(factor& k, factor& j, rational& sign) const;
 
     reference operator*() const;
     void advance_mask();
@@ -66,7 +80,7 @@ struct const_iterator_mon {
     bool operator==(const self_type &other) const;
     bool operator!=(const self_type &other) const;
             
-    factorization create_binary_factorization(lpvar j, lpvar k) const;
+    factorization create_binary_factorization(factor j, factor k) const;
     
     factorization create_full_factorization() const;
 };
@@ -74,7 +88,7 @@ struct const_iterator_mon {
 struct factorization_factory {
     const svector<lpvar>& m_vars;
     // returns true if found
-    virtual bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const = 0;
+    virtual bool find_monomial_of_vars(const svector<lpvar>& vars, unsigned& i) const = 0;
 
     factorization_factory(const svector<lpvar>& vars) :
         m_vars(vars) {