diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 59dc1948f..11928e186 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -189,6 +189,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
 }
 
 bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
+    TRACE("nla_cn_details", tout << "a = " << *a << " , b = " << *b << "\n";);
     SASSERT(is_simplified(a) && is_simplified(b));
     unsigned a_deg = a->get_degree();
     unsigned b_deg = b->get_degree();
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index 270cea2b8..289dcc8d8 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -157,7 +157,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
 
 template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) {
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
-    c().prepare_active_var_set();
+    
     SASSERT(row.size() > 1);
     sum.children().clear();
     for (const auto &p : row) {
@@ -167,8 +167,7 @@ template <typename T> void common::create_sum_from_row(const T& row, nex_creator
             sum.add_child(nexvar(p.coeff(), p.var(), cn));
         }
     }
-    set_active_vars_weights();
-}
+   }
 
 void common::set_active_vars_weights() {
     m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 2a2a46b43..86f0ef822 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -183,11 +183,20 @@ void nla_grobner::add_row(unsigned i) {
     assert_eq_0(ns, dep);
 }
 
+void nla_grobner::simplify_equations_to_process() {
+    for (equation *eq : m_to_process) {
+        eq->exp() = m_nex_creator.simplify(eq->exp());
+    }
+}
+
 void nla_grobner::init() {
     find_nl_cluster();
+    c().prepare_active_var_set();
     for (unsigned i : m_rows) {
         add_row(i);
     }
+    set_active_vars_weights();
+    simplify_equations_to_process();
 }
 
 bool nla_grobner::is_trivial(equation* eq) const {
@@ -325,7 +334,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
         m_equations_to_unfreeze.push_back(target);
         to_remove.push_back(target);
         if (m_changed_leading_term) {
-            m_to_process.insert(new_target);
+            insert_to_process(new_target);
             to_remove.push_back(target);
         }
         else {
@@ -335,7 +344,7 @@ void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equ
     }
     else {
         if (m_changed_leading_term) {
-            m_to_process.insert(target);
+            insert_to_process(target);
             to_remove.push_back(target);
         }
     }
@@ -383,7 +392,7 @@ void  nla_grobner::simplify_to_process(equation* eq) {
             to_delete.push_back(target);
     }
     for (equation* eq : to_insert)
-        m_to_process.insert(eq);
+        insert_to_process(eq);
     for (equation* eq : to_remove)
         m_to_process.erase(eq);
     for (equation* eq : to_delete)
@@ -612,16 +621,16 @@ void nla_grobner::display(std::ostream & out) const {
     NOT_IMPLEMENTED_YET();
 }
 
-void nla_grobner::assert_eq_0(const nex* e, ci_dependency * dep) {
+void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
     TRACE("nla_grobner", tout << "e = " << *e << "\n";);
     if (e == nullptr)
         return;
     equation * eq = new equation();
     init_equation(eq, e, dep);
-    m_to_process.insert(eq);
+    insert_to_process(eq);
 }
 
-void nla_grobner::init_equation(equation* eq, const nex*e, ci_dependency * dep) {
+void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
     unsigned bidx   = m_equations_to_delete.size();
     eq->m_bidx      = bidx;
     eq->m_dep       = dep;
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 84efd8038..9b0a9633b 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -41,7 +41,7 @@ class nla_grobner : common {
     class equation {
         unsigned                   m_bidx:31;       //!< position at m_equations_to_delete
         unsigned                   m_lc:1;          //!< true if equation if a linear combination of the input equations.
-        const nex *                m_exp;           //!< sorted monomials
+        nex *                      m_exp;           //  simplified expressionted monomials
         ci_dependency *            m_dep;           //!< justification for the equality
         friend class nla_grobner;
         equation() {}
@@ -49,6 +49,7 @@ class nla_grobner : common {
         unsigned get_num_monomials() const { return m_exp->size(); }
         nex_mul* const * get_monomial(unsigned idx) const { NOT_IMPLEMENTED_YET();
             return nullptr; }
+        nex* & exp() { return m_exp; }
         ci_dependency * get_dependency() const { return m_dep; }
         unsigned hash() const { return m_bidx; }
         bool is_linear_combination() const { return m_lc; }
@@ -116,13 +117,13 @@ bool simplify_processed_with_eq(equation*);
     bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
     bool internalize_gb_eq(equation*);
     void add_row(unsigned);
-    void assert_eq_0(const nex*, ci_dependency * dep);
+    void assert_eq_0(nex*, ci_dependency * dep);
     void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&);
 
     nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&);
 
     
-    void init_equation(equation* eq, const nex*, ci_dependency* d);
+    void init_equation(equation* eq, nex*, ci_dependency* d);
     equation * simplify(equation const * source, equation * target);    
     // bool less_than_on_vars(lpvar a, lpvar b) const {
     //     const auto &aw = m_nex_creatorm_active_vars_weights[a];
@@ -141,6 +142,7 @@ bool simplify_processed_with_eq(equation*);
     // }
     
     std::ostream& display_dependency(std::ostream& out, ci_dependency*);
-    
+    void insert_to_process(equation *eq) { m_to_process.insert(eq); }
+    void simplify_equations_to_process();
 }; // end of grobner
 }