diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index ebd1dd66b..9de69064d 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -59,7 +59,7 @@ public:
     
     void run(nex *e) {
         TRACE("nla_cn", tout << *e << "\n";);
-        SASSERT(m_nex_creator.is_simplified(e));
+        SASSERT(m_nex_creator.is_simplified(*e));
         m_e = e;
 #ifdef Z3DEBUG
         m_e_clone = m_nex_creator.clone(m_e);
@@ -126,7 +126,7 @@ public:
         }
         TRACE("nla_cn", tout << "common factor f=" << *f << "\n";);
         
-        nex* c_over_f = m_nex_creator.mk_div(*c, f);
+        nex* c_over_f = m_nex_creator.mk_div(**c, *f);
         c_over_f = m_nex_creator.simplify(c_over_f);
         TRACE("nla_cn", tout << "c_over_f = " << *c_over_f << std::endl;);
         nex_mul* cm; 
@@ -376,13 +376,13 @@ public:
     // all factors of j go to a, the rest to b
     void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
         TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;);
-        SASSERT(m_nex_creator.is_simplified(e));
+        SASSERT(m_nex_creator.is_simplified(*e));
         a = m_nex_creator.mk_sum();
         m_b_split_vec.clear();
         for (nex * ce: *e) {
             TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";);
             if (is_divisible_by_var(ce, j)) {
-                a->add_child(m_nex_creator.mk_div(ce , j));
+                a->add_child(m_nex_creator.mk_div(*ce , j));
             } else {
                 m_b_split_vec.push_back(ce);
             }        
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 2e8d14025..983309f16 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -122,13 +122,10 @@ public:
     expr_type type() const { return expr_type::VAR; }
     lpvar var() const {  return m_j; }
     lpvar& var() {  return m_j; } // the setter
-    std::ostream & print(std::ostream& out) const {
-        //        out <<  (char)('a' + m_j);
-        return out << "v" << m_j;
-    }    
+    std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }    
 
     bool contains(lpvar j) const { return j == m_j; }
-    int get_degree() const { return 1; }
+    int get_degree() const override { return 1; }
     bool is_linear() const override { return true; }
 };
 
@@ -140,10 +137,10 @@ public:
     expr_type type() const { return expr_type::SCALAR; }
     const rational& value() const {  return m_v; }
     rational& value() {  return m_v; } // the setter
-    std::ostream& print(std::ostream& out) const { return out << m_v; }
+    std::ostream& print(std::ostream& out) const override { return out << m_v; }
     
-    int get_degree() const { return 0; }
-    bool is_linear() const { return true; }
+    int get_degree() const override { return 0; }
+    bool is_linear() const override { return true; }
 };
 
 class nex_pow {
@@ -200,7 +197,7 @@ public:
 
     unsigned number_of_child_powers() const { return m_children.size(); }
 
-    nex_mul() : m_coeff(rational(1)) {}
+    nex_mul() : m_coeff(1) {}
 
     const rational& coeff() const {
         return m_coeff;
@@ -210,14 +207,14 @@ public:
         return m_coeff;
     }
     
-    unsigned size() const { return m_children.size(); }
-    expr_type type() const { return expr_type::MUL; }
+    unsigned size() const override { return m_children.size(); }
+    expr_type type() const override { return expr_type::MUL; }
     vector<nex_pow>& children() { return m_children;}
     const vector<nex_pow>& children() const { return m_children;}
     // A monomial is 'pure' if does not have a numeric coefficient.
     bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); }    
 
-    std::ostream & print(std::ostream& out) const {        
+    std::ostream & print(std::ostream& out) const override {
         bool first = true;
         if (!m_coeff.is_one()) {
             out << m_coeff;
@@ -289,11 +286,11 @@ public:
         TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
     }
 
-    int get_degree() const {
+    int get_degree() const override {
         return get_degree_children(children());
     }    
     
-    bool is_linear() const {
+    bool is_linear() const override {
         return get_degree() < 2; // todo: make it more efficient
     }
 
@@ -315,15 +312,15 @@ class nex_sum : public nex {
     ptr_vector<nex> m_children;
 public:
     nex_sum()  {}
-    expr_type type() const { return expr_type::SUM; }
+    expr_type type() const override { return expr_type::SUM; }
     ptr_vector<nex>& children() { return m_children;}
     const ptr_vector<nex>& children() const { return m_children;}    
     const ptr_vector<nex>* children_ptr() const { return &m_children;}
     ptr_vector<nex>* children_ptr() { return &m_children;}
-    unsigned size() const { return m_children.size(); }
+    unsigned size() const override { return m_children.size(); }
 
 
-    bool is_linear() const {
+    bool is_linear() const override {
         TRACE("nex_details", tout << *this << "\n";);
         for (auto  e : *this) {
             if (!e->is_linear())
@@ -347,7 +344,7 @@ public:
         return number_of_non_scalars > 1;
     }
     
-    std::ostream & print(std::ostream& out) const {
+    std::ostream & print(std::ostream& out) const override {
         bool first = true;
         for (const nex* v : m_children) {            
             std::string s = v->str();
@@ -372,7 +369,7 @@ public:
         return out;
     }
 
-    int get_degree() const {
+    int get_degree() const override {
         int degree = 0;       
         for (auto  e : *this) {
             degree = std::max(degree, e->get_degree());
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 574e5a34d..07b65549f 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -21,30 +21,28 @@
 #include "math/lp/nex_creator.h"
 #include <map>
 
-namespace nla {
+using namespace nla;
 
-nex * nex_creator::mk_div(const nex* a, lpvar j) {
+// divides by variable j. A precondition is that a is a multiple of j.
+nex * nex_creator::mk_div(const nex& a, lpvar j) {
     SASSERT(is_simplified(a));
-    SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
-    if (a->is_var())
+    SASSERT(a.contains(j));
+    SASSERT(a.is_mul() || (a.is_var() && a.to_var().var() == j));
+    if (a.is_var())
         return mk_scalar(rational(1));
     vector<nex_pow> bv; 
     bool seenj = false;
-    auto ma = *to_mul(a);
+    auto ma = a.to_mul();
     for (auto& p : ma) {
         const nex * c = p.e();
         int pow = p.pow();
         if (!seenj && c->contains(j)) {
-            if (!c->is_var()) {                    
-                bv.push_back(nex_pow(mk_div(c, j)));
-                if (pow != 1) {
-                    bv.push_back(nex_pow(clone(c), pow - 1)); 
-                }
-            } else {
-                SASSERT(to_var(c)->var() == j);
-                if (p.pow() != 1) {
-                    bv.push_back(nex_pow(mk_var(j), pow - 1));
-                }
+            SASSERT(!c->is_var() || c->to_var().var() == j);
+            if (!c->is_var()) {
+                bv.push_back(nex_pow(mk_div(*c, j)));
+            }
+            if (pow != 1) {
+                bv.push_back(nex_pow(clone(c), pow - 1));
             }
             seenj = true;
         } else {
@@ -64,9 +62,10 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
 
 }
 
+// TBD: describe what this does
 bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
     if (p.e()->is_mul()) {
-        const nex_mul & m = *to_mul(p.e());
+        const nex_mul & m = p.e()->to_mul();
         if (m.size() == 0) {
             const rational& coeff = m.coeff();
             if (coeff.is_one())
@@ -78,10 +77,10 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
     }
     if (!p.e()->is_scalar())
         return false;
-    const nex_scalar *pe = to_scalar(p.e());
-    if (pe->value().is_one())
+    const nex_scalar &pe = p.e()->to_scalar();
+    if (pe.value().is_one())
         return true; // r does not change here
-    r *= pe->value().expt(p.pow() * pow);
+    r *= pe.value().expt(p.pow() * pow);
     return true;
 }
 
@@ -89,22 +88,16 @@ bool nex_creator::eat_scalar_pow(rational& r, const nex_pow& p, unsigned pow) {
 void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational& coeff) {
     TRACE("grobner_d", print_vector(children, tout););
     vector<nex_pow> to_promote;
-    bool skipped = false;
     unsigned j = 0;
     for (nex_pow& p : children) {        
         if (eat_scalar_pow(coeff, p, 1)) {
-            skipped = true;
             continue;
-        }
-        
+        }        
         p.e() = simplify(p.e());
-        if ((p.e())->is_mul()) {
-            skipped = true;
+        if (p.e()->is_mul()) {
             to_promote.push_back(p);
         } else {
-            if (skipped) 
-                children[j] = p;
-            j++;
+            children[j++] = p;
         }
     }
     
@@ -112,13 +105,13 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
 
     for (nex_pow & p : to_promote) {
         TRACE("grobner_d", tout << p << "\n";);
-        nex_mul *pm = to_mul(p.e());
-        for (nex_pow& pp : *pm) {
+        nex_mul &pm = p.e()->to_mul();
+        for (nex_pow& pp : pm) {
             TRACE("grobner_d", tout << pp << "\n";);
             if (!eat_scalar_pow(coeff, pp, p.pow()))
                 children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));            
         }
-        coeff *= pm->coeff().expt(p.pow());
+        coeff *= pm.coeff().expt(p.pow());
     }
 
     mul_to_powers(children);
@@ -159,29 +152,28 @@ bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) con
             if (it_b != b.end()) b_pow = it_b->pow();
         }
     }
-    TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret?" > ":" <= ") << b << "\n";);
+    TRACE("nex_gt", tout << "a = "; print_vector(a, tout) << (ret?" > ":" <= ") << b << "\n";);
     return ret;
 }
 
 bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
     for (auto c : children) 
-        if (!is_simplified(c.e()) || c.pow() == 0)
+        if (!is_simplified(*c.e()) || c.pow() == 0)
             return false;
     return true;
 }
 
 bool nex_creator::gt_on_powers_mul(const vector<nex_pow>& children, const nex_mul& b) const {
-    TRACE("nex_less", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";);
-    SASSERT(children_are_simplified(children) && is_simplified(&b));
+    TRACE("nex_gt", tout << "children = "; print_vector(children, tout) << " , b = " << b << "\n";);
+    SASSERT(children_are_simplified(children) && is_simplified(b));
     unsigned a_deg = get_degree_children(children);
     unsigned b_deg = b.get_degree();
-
     return a_deg == b_deg ? gt_on_powers_mul_same_degree(children, b) : a_deg > b_deg;
 }
 
 bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
     TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";);
-    SASSERT(is_simplified(&a) && is_simplified(&b));
+    SASSERT(is_simplified(a) && is_simplified(b));
     unsigned a_deg = a.get_degree();
     unsigned b_deg = b.get_degree();
     return a_deg == b_deg ? gt_on_powers_mul_same_degree(a, b) : a_deg > b_deg;
@@ -208,15 +200,12 @@ bool nex_creator::gt_nex_powers(const vector<nex_pow>& children, const nex* b) c
     switch (b->type()) {
     case expr_type::SCALAR: 
         return false;
-    case expr_type::VAR: { 
+    case expr_type::VAR: 
         if (get_degree_children(children) > 1)
             return true;
-        const nex_pow & c  = children[0];
-        SASSERT(c.pow() == 1);
-        const nex * f = c.e();
-        SASSERT(!f->is_scalar());
-        return gt(f, b);
-    }
+        SASSERT(children[0].pow() == 1);
+        SASSERT(!children[0].e()->is_scalar());
+        return gt(children[0].e(), b);    
     case expr_type::MUL:
         return gt_on_powers_mul(children, *to_mul(b));            
     case expr_type::SUM:
@@ -231,15 +220,12 @@ bool nex_creator::gt_on_mul_nex(const nex_mul* a, const nex* b) const {
     switch (b->type()) {
     case expr_type::SCALAR: 
         return false;
-    case expr_type::VAR: {   
+    case expr_type::VAR: 
         if (a->get_degree() > 1)
             return true;
-        const nex_pow & c  = *a->begin();
-        SASSERT(c.pow() == 1);
-        const nex * f = c.e();
-        SASSERT(!f->is_scalar());
-        return gt(f, b);
-    }
+        SASSERT(a->begin()->pow() == 1);
+        SASSERT(!a->begin()->e()->is_scalar());
+        return gt(a->begin()->e(), b);    
     case expr_type::MUL:
         return gt_on_mul_mul(*a, *to_mul(b));            
     case expr_type::SUM:
@@ -258,8 +244,7 @@ bool nex_creator::gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const {
         if (gt((*b)[j], (*a)[j]))
             return false;
     }
-    return size > b->size();
-            
+    return a->size() > size;
 }
 
 // the only difference with gt() that it disregards the coefficient in nex_mul
@@ -321,11 +306,11 @@ bool nex_creator::gt(const nex* a, const nex* b) const {
     return ret;
 }
 
-bool nex_creator::is_sorted(const nex_mul* e) const {
-    for (unsigned j = 0; j < e->size() - 1; j++) {
-        if (!(gt_on_nex_pow((*e)[j], (*e)[j+1]))) {
-            TRACE("grobner_d", tout << "not sorted e " << * e << "\norder is incorrect " <<
-                  (*e)[j] << " >= " << (*e)[j + 1]<< "\n";);
+bool nex_creator::is_sorted(const nex_mul& e) const {
+    for (unsigned j = 0; j < e.size() - 1; j++) {
+        if (!(gt_on_nex_pow(e[j], e[j+1]))) {
+            TRACE("grobner_d", tout << "not sorted e " << e << "\norder is incorrect " <<
+                  e[j] << " >= " << e[j + 1]<< "\n";);
 
             return false;
         }
@@ -333,18 +318,18 @@ bool nex_creator::is_sorted(const nex_mul* e) const {
     return true;
 }
 
-bool nex_creator::mul_is_simplified(const nex_mul* e) const {
-    TRACE("nla_cn_", tout <<  "e = " << *e << "\n";);
-    if (e->size() == 0) {
+bool nex_creator::mul_is_simplified(const nex_mul& e) const {
+    TRACE("nla_cn_", tout <<  "e = " << e << "\n";);
+    if (e.size() == 0) {
         TRACE("nla_cn", );
         return false; // it has to be a scalar
     }
-    if (e->size() == 1 && e->begin()->pow() == 1 && e->coeff().is_one()) { 
+    if (e.size() == 1 && e.begin()->pow() == 1 && e.coeff().is_one()) { 
         TRACE("nla_cn", );
         return false;
     }
     std::set<const nex*, nex_lt> s([this](const nex* a, const nex* b) {return gt(a, b); });
-    for (const auto &p : *e) {
+    for (const auto &p : e) {
         const nex* ee = p.e();
         if (p.pow() == 0) {
             TRACE("nla_cn", tout << "not simplified " << *ee << "\n";);
@@ -380,7 +365,7 @@ nex * nex_creator::simplify_mul(nex_mul *e) {
     if (e->size() == 0 || e->coeff().is_zero())
         return mk_scalar(e->coeff());
     TRACE("grobner_d", tout << *e << "\n";);
-    SASSERT(is_simplified(e));
+    SASSERT(is_simplified(*e));
     return e;
 }
 
@@ -399,19 +384,19 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
     return r;
 }
 
-bool nex_creator::sum_is_simplified(const nex_sum* e) const {
-    if (e->size() < 2)  return false;
+bool nex_creator::sum_is_simplified(const nex_sum& e) const {
+    if (e.size() < 2)  return false;
     bool scalar = false;
-    for (nex * ee : *e) {
+    for (nex * ee : e) {
         TRACE("nla_cn_details", tout << "ee = " << *ee << "\n";);
         if (ee->is_sum()) {
-            TRACE("nla_cn", tout << "not simplified e = " << *e << "\n"
+            TRACE("nla_cn", tout << "not simplified e = " << e << "\n"
                   << " has a child which is a sum " << *ee << "\n";);
             return false;
         }
         if (ee->is_scalar()) {
             if (scalar) {
-                TRACE("nla_cn", tout <<  "not simplified e = " << *e << "\n"
+                TRACE("nla_cn", tout <<  "not simplified e = " << e << "\n"
                       << " have more than one scalar " << *ee << "\n";);
                 
                 return false;
@@ -425,7 +410,7 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
                 scalar = true;
             }
         }
-        if (!is_simplified(ee))
+        if (!is_simplified(*ee))
             return false;
     }
     return true;
@@ -457,7 +442,7 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
     TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";);
     if (coeff.is_one())
         return e;
-    SASSERT(is_simplified(e));
+    SASSERT(is_simplified(*e));
     switch (e->type()) {
     case expr_type::VAR: {
         if (coeff.is_one())
@@ -538,7 +523,7 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
     std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b)
                                        { return gt_for_sort_join_sum(a, b); });
     std::unordered_set<nex*> allocated_nexs; // handling (nex*) as numbers
-    nex_scalar * common_scalar;
+    nex_scalar * common_scalar = nullptr;
     fill_join_map_for_sum(children, map, allocated_nexs, common_scalar);
 
     TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
@@ -551,32 +536,24 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
     }
     TRACE("grobner_d",
           tout << "map=";
-          for (auto & p : map )
-              { tout << "(" << *p.first << ", " << p.second << ") "; }
+          for (auto & p : map ) tout << "(" << *p.first << ", " << p.second << ") "; 
           tout << "\nchildren="; print_vector_of_ptrs(children, tout) << "\n";);    
 }
 
 void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
     TRACE("grobner_d", print_vector_of_ptrs(children, tout););
     ptr_vector<nex> to_promote;
-    bool skipped = false;
     unsigned k = 0; 
     for (unsigned j = 0; j < children.size(); j++) {
         nex* e = children[j] = simplify(children[j]);
         if (e->is_sum()) {
-            skipped = true;
             to_promote.push_back(e);
         } else if (is_zero_scalar(e)) {
-            skipped = true;
             continue;
         } else if (e->is_mul() && to_mul(e)->coeff().is_zero() ) {
-            skipped = true;
             continue;
-        }else {
-            if (skipped) {
-                children[k] = e;
-            }
-            k++;
+        } else {
+            children[k++] = e;
         }
     }
     
@@ -584,7 +561,7 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
     children.shrink(k);
     
     for (nex *e : to_promote) {
-        for (nex *ee : *(to_sum(e)->children_ptr())) {
+        for (nex *ee : *(e->to_sum().children_ptr())) {
             if (!is_zero_scalar(ee))
                 children.push_back(ee);            
         }
@@ -594,11 +571,10 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
 }
 
 
-bool have_no_scalars(const nex_mul* a) {
-    for (auto & p : *a)
+static bool have_no_scalars(const nex_mul& a) {
+    for (auto & p : a)
         if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
             return false;
-
     return true;
 }
 
@@ -606,24 +582,23 @@ bool nex_mul::all_factors_are_elementary() const {
     for (auto & p : *this)
         if (!p.e()->is_elementary())
             return false;
-
     return true;
 }
 
-nex * nex_creator::mk_div_sum_by_mul(const nex_sum* m, const nex_mul* b) {
+nex * nex_creator::mk_div_sum_by_mul(const nex_sum& m, const nex_mul& b) {
     nex_sum * r = mk_sum();
-    for (auto e : *m) {
-        r->add_child(mk_div_by_mul(e, b));
+    for (auto e : m) {
+        r->add_child(mk_div_by_mul(*e, b));
     }
     TRACE("grobner_d", tout << *r << "\n";);
     return r;
 }
 
-nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
-    SASSERT(a->all_factors_are_elementary() && b->all_factors_are_elementary());
-    b->get_powers_from_mul(m_powers);
+nex * nex_creator::mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b) {
+    SASSERT(a.all_factors_are_elementary() && b.all_factors_are_elementary());
+    b.get_powers_from_mul(m_powers);
     nex_mul* ret = new nex_mul();
-    for (auto& p_from_a : *a) {
+    for (auto& p_from_a : a) {
         TRACE("grobner_d", tout << "p_from_a = " << p_from_a << "\n";);
         const nex* e = p_from_a.e();
         if (e->is_scalar()) {
@@ -658,46 +633,45 @@ nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
     if (ret->size() == 0) {
         delete ret;
         TRACE("grobner_d", tout << "return scalar\n";);
-        return mk_scalar(a->coeff() / b->coeff());
+        return mk_scalar(a.coeff() / b.coeff());
     }
-    ret->coeff() = a->coeff() / b->coeff();
+    ret->coeff() = a.coeff() / b.coeff();
     add_to_allocated(ret);
     TRACE("grobner_d", tout << *ret << "\n";);        
     return ret;
 }
 
-nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) {
+nex * nex_creator::mk_div_by_mul(const nex& a, const nex_mul& b) {
     SASSERT(have_no_scalars(b));
-    if (a->is_sum()) {
-        return mk_div_sum_by_mul(to_sum(a), b);
-    }
-    
-    if (a->is_var()) {
-        SASSERT(b->get_degree() == 1 && get_vars_of_expr(a) == get_vars_of_expr(b) && b->coeff().is_one());
+    SASSERT(!a.is_var() || (b.get_degree() == 1 && get_vars_of_expr(&a) == get_vars_of_expr(&b) && b.coeff().is_one()));
+    if (a.is_sum()) {
+        return mk_div_sum_by_mul(a.to_sum(), b);
+    }    
+    if (a.is_var()) {        
         return mk_scalar(rational(1));
     }    
-    return mk_div_mul_by_mul(to_mul(a), b);
+    return mk_div_mul_by_mul(a.to_mul(), b);
 }
 
-nex * nex_creator::mk_div(const nex* a, const nex* b) {
-    TRACE("grobner_d", tout << *a <<" / " << *b << "\n";);
-    if (b->is_var()) {
-        return mk_div(a, to_var(b)->var());
+nex * nex_creator::mk_div(const nex& a, const nex& b) {
+    TRACE("grobner_d", tout << a <<" / " << b << "\n";);
+    if (b.is_var()) {
+        return mk_div(a, b.to_var().var());
     }
-    return mk_div_by_mul(a, to_mul(b));
+    return mk_div_by_mul(a, b.to_mul());
 }
 
 nex* nex_creator::simplify(nex* e) {
     nex* es;
     TRACE("grobner_d", tout << *e << std::endl;);
     if (e->is_mul())
-        es =  simplify_mul(to_mul(e));
+        es = simplify_mul(to_mul(e));
     else if (e->is_sum())
-        es =  simplify_sum(to_sum(e));
+        es = simplify_sum(to_sum(e));
     else
         es = e;
     TRACE("grobner_d", tout << "simplified = " << *es << std::endl;);
-    SASSERT(is_simplified(es));
+    SASSERT(is_simplified(*es));
     return es;
 }
 
@@ -713,7 +687,7 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
         m_allocated.push_back(e);
     }
     if (e->is_mul()) {
-        to_mul(e)->coeff() = coeff;
+        e->to_mul().coeff() = coeff;
         children.push_back(simplify(e));
     } else {
         SASSERT(e->is_var());
@@ -725,13 +699,12 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
     }
 }
 
-bool nex_creator::is_simplified(const nex *e) const 
-{
-    TRACE("nla_cn_details", tout << "e = " << *e << "\n";);
-    if (e->is_mul())
-        return mul_is_simplified(to_mul(e));
-    if (e->is_sum())
-        return sum_is_simplified(to_sum(e));
+bool nex_creator::is_simplified(const nex& e) const {
+    TRACE("nla_cn_details", tout << "e = " << e << "\n";);
+    if (e.is_mul())
+        return mul_is_simplified(e.to_mul());
+    if (e.is_sum())
+        return sum_is_simplified(e.to_sum());
     return true;
 }
 
@@ -752,10 +725,10 @@ nex* nex_creator::canonize_mul(nex_mul *a) {
     nex_pow& np = (*a)[j];
     SASSERT(np.pow());
     unsigned power = np.pow();
-    nex_sum * s = to_sum(np.e()); // s is going to explode        
+    nex_sum const& s = np.e()->to_sum(); // s is going to explode        
     nex_sum * r = mk_sum();
-    nex *sclone = power > 1? clone(s) : nullptr;
-    for (nex *e : *s) {
+    nex *sclone = power > 1 ? clone(&s) : nullptr;
+    for (nex *e : s) {
         nex_mul *m = mk_mul();
         if (power > 1)
             m->add_child_in_power(sclone, power - 1);
@@ -777,11 +750,11 @@ nex* nex_creator::canonize(const nex *a) {
     
     nex *t = simplify(clone(a));
     if (t->is_sum()) {
-        nex_sum * s = to_sum(t);
-        for (unsigned j = 0; j < s->size(); j++) {
-            (*s)[j] = canonize((*s)[j]);
+        nex_sum & s = t->to_sum();
+        for (unsigned j = 0; j < s.size(); j++) {
+            s[j] = canonize(s[j]);
         }
-        t = simplify(s);
+        t = simplify(&s);
         TRACE("grobner_d", tout << *t << "\n";);
         return t;
     }
@@ -810,4 +783,3 @@ bool nex_creator::equal(const nex* a, const nex* b) {
 }
 #endif
 
-}
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 7b46e543e..7f38c3fe7 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -19,6 +19,7 @@
   --*/
 #pragma once
 #include <map>
+#include "util/map.h"
 #include "math/lp/nex.h"
 namespace nla {
 
@@ -209,20 +210,20 @@ public:
         return r;
     }
 
-    nex * mk_div(const nex* a, lpvar j);
-    nex * mk_div(const nex* a, const nex* b);
-    nex * mk_div_by_mul(const nex* a, const nex_mul* b);
-    nex * mk_div_sum_by_mul(const nex_sum* a, const nex_mul* b);
-    nex * mk_div_mul_by_mul(const nex_mul* a, const nex_mul* b);
+    nex * mk_div(const nex& a, lpvar j);
+    nex * mk_div(const nex& a, const nex& b);
+    nex * mk_div_by_mul(const nex& a, const nex_mul& b);
+    nex * mk_div_sum_by_mul(const nex_sum& a, const nex_mul& b);
+    nex * mk_div_mul_by_mul(const nex_mul& a, const nex_mul& b);
     
     nex * simplify_mul(nex_mul *e);    
-    bool is_sorted(const nex_mul * e) const;    
+    bool is_sorted(const nex_mul & e) const;    
 
     nex* simplify_sum(nex_sum *e);
 
-    bool is_simplified(const nex *e) const;
-    bool sum_is_simplified(const nex_sum* e) const;
-    bool mul_is_simplified(const nex_mul*e ) const;
+    bool is_simplified(const nex &e) const;
+    bool sum_is_simplified(const nex_sum& e) const;
+    bool mul_is_simplified(const nex_mul& e) const;
     
     void mul_to_powers(vector<nex_pow>& children);
     
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 1e910df52..5f3a6ef58 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -90,7 +90,7 @@ public:
     intervals                m_intervals;                
     horner                   m_horner;
     nla_settings             m_nla_settings;
-    nla_grobner              m_grobner;
+    grobner              m_grobner;
 private:
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index d1bf7cafd..44aef516e 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -20,8 +20,9 @@
 #include "math/lp/nla_grobner.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
-namespace nla {
-nla_grobner::nla_grobner(core *c, intervals *s)
+using namespace nla;
+
+grobner::grobner(core *c, intervals *s)
     : common(c, s),
       m_nl_gb_exhausted(false),
       m_dep_manager(m_val_manager, m_alloc),
@@ -29,12 +30,30 @@ nla_grobner::nla_grobner(core *c, intervals *s)
       m_look_for_fixed_vars_in_rows(false)
 {}
 
-bool nla_grobner::internalize_gb_eq(equation* ) {
+void grobner::grobner_lemmas() {
+    c().lp_settings().stats().m_grobner_calls++;
+
+    init();
+
+    ptr_vector<equation> eqs;
+    unsigned next_weight =
+        (unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase. 
+    do {
+        TRACE("grobner", tout << "before:\n"; display(tout););
+        compute_basis();
+        update_statistics();
+        TRACE("grobner", tout << "after:\n"; display(tout););
+        // if (find_conflict(eqs))
+        //     return;
+    } while (push_calculation_forward(eqs, next_weight));
+}
+
+bool grobner::internalize_gb_eq(equation* ) {
     NOT_IMPLEMENTED_YET();
     return false;
 }
 
-void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
+void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
     SASSERT(!c().active_var_set_contains(j) &&  !c().var_is_fixed(j));
     TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";);
     const auto& matrix = c().m_lar_solver.A_r();
@@ -69,7 +88,7 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
     }            
 }
 
-void nla_grobner::find_nl_cluster() {
+void grobner::find_nl_cluster() {
     prepare_rows_and_active_vars();
     std::queue<lpvar> q;
     for (lpvar j : c().m_to_refine) {        
@@ -92,13 +111,13 @@ void nla_grobner::find_nl_cluster() {
     TRACE("grobner", display(tout););
 }
 
-void nla_grobner::prepare_rows_and_active_vars() {
+void grobner::prepare_rows_and_active_vars() {
     m_rows.clear();
     m_rows.resize(c().m_lar_solver.row_count());
     c().clear_and_resize_active_var_set();
 }
 
-void nla_grobner::display_matrix(std::ostream & out) const {
+void grobner::display_matrix(std::ostream & out) const {
     const auto& matrix = c().m_lar_solver.A_r();
     out << m_rows.size() << " rows" <<"\n";
     out << "the matrix\n";
@@ -107,21 +126,21 @@ void nla_grobner::display_matrix(std::ostream & out) const {
         c().print_term(r, out) << std::endl;
     }
 }
-std::ostream & nla_grobner::display(std::ostream & out) const {
+std::ostream & grobner::display(std::ostream & out) const {
     display_equations(out, m_to_superpose, "m_to_superpose:");
     display_equations(out, m_to_simplify, "m_to_simplify:");
     return out;
 }
 
 
-common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
+common::ci_dependency* grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
     ci_dependency * d = nullptr;
     for (auto c : cs)
         d = m_dep_manager.mk_join(d, m_dep_manager.mk_leaf(c));
     return d;
 }
 
-void nla_grobner::add_row(unsigned i) {    
+void grobner::add_row(unsigned i) {    
     const auto& row = c().m_lar_solver.A_r().m_rows[i];    
     TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
           for (auto p : row) {
@@ -135,13 +154,13 @@ void nla_grobner::add_row(unsigned i) {
     assert_eq_0(e, dep);
 }
 
-void nla_grobner::simplify_equations_in_m_to_simplify() {
+void grobner::simplify_equations_in_m_to_simplify() {
     for (equation *eq : m_to_simplify) {
         eq->expr() = m_nex_creator.simplify(eq->expr());
     }
 }
 
-void nla_grobner::init() {
+void grobner::init() {
     m_reported = 0;
     del_equations(0);
     SASSERT(m_equations_to_delete.size() == 0);    
@@ -157,13 +176,13 @@ void nla_grobner::init() {
     simplify_equations_in_m_to_simplify();
 }
 
-bool nla_grobner::is_trivial(equation* eq) const {
-    SASSERT(m_nex_creator.is_simplified(eq->expr()));
+bool grobner::is_trivial(equation* eq) const {
+    SASSERT(m_nex_creator.is_simplified(*eq->expr()));
     return eq->expr()->size() == 0;
 }
 
 // returns true if eq1 is simpler than eq2
-bool nla_grobner::is_simpler(equation * eq1, equation * eq2) {
+bool grobner::is_simpler(equation * eq1, equation * eq2) {
     if (!eq2)
         return true;
     if (is_trivial(eq1))
@@ -173,7 +192,7 @@ bool nla_grobner::is_simpler(equation * eq1, equation * eq2) {
     return m_nex_creator.gt(eq2->expr(), eq1->expr());
 }
 
-void nla_grobner::del_equation(equation * eq) {
+void grobner::del_equation(equation * eq) {
     m_to_superpose.erase(eq);
     m_to_simplify.erase(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
@@ -181,7 +200,7 @@ void nla_grobner::del_equation(equation * eq) {
     dealloc(eq);
 }
 
-nla_grobner::equation* nla_grobner::pick_next() {
+grobner::equation* grobner::pick_next() {
     equation * r = nullptr;
     ptr_buffer<equation> to_delete;
     for (equation * curr : m_to_simplify) {
@@ -200,7 +219,7 @@ nla_grobner::equation* nla_grobner::pick_next() {
     return r;
 }
 
-nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) {
+grobner::equation* grobner::simplify_using_to_superpose(equation* eq) {
     bool result = false;
     bool simplified;
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
@@ -229,7 +248,7 @@ nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) {
     return result ? eq : nullptr;
 }
 
-const nex* nla_grobner::get_highest_monomial(const nex* e) const {
+const nex* grobner::get_highest_monomial(const nex* e) const {
     switch (e->type()) {
     case expr_type::MUL:
         return to_mul(e);
@@ -245,7 +264,7 @@ const nex* nla_grobner::get_highest_monomial(const nex* e) const {
 // source 3f + k + l = 0, so f = (-k - l)/3
 // target 2fg + 3fp + e = 0  
 // target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e
-bool nla_grobner::simplify_target_monomials(equation * source, equation * target) {
+bool grobner::simplify_target_monomials(equation * source, equation * target) {
     auto * high_mon = get_highest_monomial(source->expr());
     if (high_mon == nullptr)
         return false;
@@ -266,7 +285,7 @@ bool nla_grobner::simplify_target_monomials(equation * source, equation * target
     return simplify_target_monomials_sum(source, target, targ_sum, high_mon);   
 }
 
-unsigned nla_grobner::find_divisible(nex_sum* targ_sum,
+unsigned grobner::find_divisible(nex_sum* targ_sum,
                                                            const nex* high_mon) const {
     for (unsigned j = 0; j < targ_sum->size(); j++) {
         auto t = (*targ_sum)[j];
@@ -280,7 +299,7 @@ unsigned nla_grobner::find_divisible(nex_sum* targ_sum,
 }
 
 
-bool nla_grobner::simplify_target_monomials_sum(equation * source,
+bool grobner::simplify_target_monomials_sum(equation * source,
                                                 equation * target, nex_sum* targ_sum,
                                                 const nex* high_mon) {
     unsigned j = find_divisible(targ_sum, high_mon);
@@ -298,16 +317,16 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
     return true;
 }
 
-nex_mul* nla_grobner::divide_ignore_coeffs(nex* ej, const nex* h) {
+nex_mul* grobner::divide_ignore_coeffs(nex* ej, const nex* h) {
     TRACE("grobner", tout << "ej = " << *ej << " , h = " << *h << "\n";);
     if (!divide_ignore_coeffs_check_only(ej, h))
         return nullptr;
     return divide_ignore_coeffs_perform(ej, h);
 }
 
-bool nla_grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const {
+bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const {
     TRACE("grobner", tout << "t = " << *t << ", h=" << *h << "\n";);  
-    SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h));
+    SASSERT(m_nex_creator.is_simplified(*t) && m_nex_creator.is_simplified(*h));
     unsigned j = 0; // points to t
     for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
         lpvar h_var = to_var(h->get_child_exp(k))->var();
@@ -331,7 +350,7 @@ bool nla_grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex
 }
 
 // return true if h divides t
-bool nla_grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
+bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
     if (n->is_mul())
         return divide_ignore_coeffs_check_only_nex_mul(to_mul(n), h);
     if (!n->is_var())
@@ -354,7 +373,7 @@ bool nla_grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
     return false;        
 }
 
-nex_mul * nla_grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) {
+nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) {
     nex_mul * r = m_nex_creator.mk_mul();
     unsigned j = 0; // points to t
     for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
@@ -379,7 +398,7 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const ne
 
 // perform the division t / h, but ignores the coefficients
 // h does not change
-nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
+nex_mul * grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
     if (e->is_mul())
         return divide_ignore_coeffs_perform_nex_mul(to_mul(e), h);
     SASSERT(e->is_var());
@@ -390,7 +409,7 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
 // and  b*high_mon + e = 0, so high_mon = -e/b
 // then targ_sum->children()[j] =  - (c/b) * e*p
 
-void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) {    
+void grobner::simplify_target_monomials_sum_j(equation * source, equation *target, nex_sum* targ_sum, const nex* high_mon, unsigned j) {    
     nex * ej = (*targ_sum)[j];
     TRACE("grobner_d", tout << "high_mon = " << *high_mon << ", ej = " << *ej << "\n";);
     nex_mul * ej_over_high_mon = divide_ignore_coeffs(ej, high_mon);
@@ -409,11 +428,11 @@ void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *t
 }
 
 // return true iff simplified
-bool nla_grobner::simplify_source_target(equation * source, equation * target) {
+bool grobner::simplify_source_target(equation * source, equation * target) {
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
     TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) <<  " using " << *(source->expr()) << "\n";);
-    SASSERT(m_nex_creator.is_simplified(source->expr()));
-    SASSERT(m_nex_creator.is_simplified(target->expr()));
+    SASSERT(m_nex_creator.is_simplified(*source->expr()));
+    SASSERT(m_nex_creator.is_simplified(*target->expr()));
     if (target->expr()->is_scalar()) {
         TRACE("grobner_d", tout << "no simplification\n";);
         return false;
@@ -442,7 +461,7 @@ bool nla_grobner::simplify_source_target(equation * source, equation * target) {
     return false;
 }
  
-void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
+void grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
     if (is_trivial(target)) {
         to_remove.push_back(target);
     } else if (m_changed_leading_term) {
@@ -451,7 +470,7 @@ void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equatio
     }
 }
 
-void nla_grobner::check_eq(equation* target) {
+void grobner::check_eq(equation* target) {
     if(m_intervals->check_nex(target->expr(), target->dep())) {
         TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
               tout << "vars = \n";
@@ -463,7 +482,7 @@ void nla_grobner::check_eq(equation* target) {
     }
 }
 
-bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
+bool grobner::simplify_to_superpose_with_eq(equation* eq) {
     TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) <<  "\n";);
 
     ptr_buffer<equation> to_insert;
@@ -481,7 +500,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
         if (is_trivial(target))
             to_delete.push_back(target);
         else 
-            SASSERT(m_nex_creator.is_simplified(target->expr()));
+            SASSERT(m_nex_creator.is_simplified(*target->expr()));
     }
     for (equation* eq : to_insert) 
         insert_to_superpose(eq);
@@ -495,7 +514,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
 /*
     Use the given equation to simplify m_to_simplify equations
 */
-void  nla_grobner::simplify_m_to_simplify(equation* eq) {
+void  grobner::simplify_m_to_simplify(equation* eq) {
     TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) <<  "\n";);
     ptr_buffer<equation> to_delete;
     for (equation* target : m_to_simplify) {
@@ -509,7 +528,7 @@ void  nla_grobner::simplify_m_to_simplify(equation* eq) {
 // if e is the sum then add to r all children of e multiplied by beta, except the first one
 // which corresponds to the highest monomial,
 // otherwise do nothing
-void nla_grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) {
+void grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c) {
     if (e->is_sum()) {
         nex_sum *es = to_sum(e);
         for (unsigned j = 1; j < es->size(); j++) {
@@ -523,7 +542,7 @@ void nla_grobner::add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, n
 
 
 // let e1: alpha*ab+q=0, and e2: beta*ac+e=0, then beta*qc - alpha*eb = 0
-nex * nla_grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) {
+nex * grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c) {
     TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\n";);    
     nex_sum * r = m_nex_creator.mk_sum();
     rational alpha = - ab->coeff();
@@ -540,7 +559,7 @@ nex * nla_grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac
     return ret;
 }
 // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
-void nla_grobner::superpose(equation * eq1, equation * eq2) {
+void grobner::superpose(equation * eq1, equation * eq2) {
     TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
     const nex * ab = get_highest_monomial(eq1->expr()); 
     const nex * ac = get_highest_monomial(eq2->expr());
@@ -562,13 +581,13 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
 
 }
 
-void nla_grobner::register_report() {
+void grobner::register_report() {
     m_reported++;
     m_conflict = true;
 }
 // Let a be the greatest common divider of ab and bc,
 // then ab/a is stored in b, and ac/a is stored in c
-bool nla_grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
+bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
     if (!find_b_c_check_only(ab, ac))
         return false;
     b = m_nex_creator.mk_mul(); c = m_nex_creator.mk_mul();
@@ -614,10 +633,10 @@ bool nla_grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*&
     return true;
 }
 // Finds out if ab and bc have a non-trivial common divider
-bool nla_grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
+bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
     if (ab == nullptr || ac == nullptr)
         return false;
-    SASSERT(m_nex_creator.is_simplified(ab) && m_nex_creator.is_simplified(ab));
+    SASSERT(m_nex_creator.is_simplified(*ab) && m_nex_creator.is_simplified(*ac));
     unsigned i = 0, j = 0; // i points to ab, j points to ac
     for (;;) {
         const nex* m = ab->get_child_exp(i);
@@ -641,14 +660,14 @@ bool nla_grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
 }
 
 
-void nla_grobner::superpose(equation * eq) {
+void grobner::superpose(equation * eq) {
     for (equation * target : m_to_superpose) {
         superpose(eq, target);
     }
 }
 
 // return true iff cannot pick_next()
-bool nla_grobner::compute_basis_step() {
+bool grobner::compute_basis_step() {
     equation * eq = pick_next();
     if (!eq) {
         TRACE("grobner", tout << "cannot pick an equation\n";);
@@ -671,7 +690,7 @@ bool nla_grobner::compute_basis_step() {
     return false;
 }
 
-void nla_grobner::compute_basis(){
+void grobner::compute_basis(){
     compute_basis_init();
     if (m_rows.size() < 2) {
         TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";);
@@ -690,16 +709,16 @@ void nla_grobner::compute_basis(){
         }
     }
 }
-void nla_grobner::compute_basis_init(){
+void grobner::compute_basis_init(){
     c().lp_settings().stats().m_grobner_basis_computatins++;    
 }        
 
-bool nla_grobner::canceled() const {
+bool grobner::canceled() const {
     return c().lp_settings().get_cancel_flag();
 }
 
 
-bool nla_grobner::done() const {
+bool grobner::done() const {
     if (
         num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold() 
         ||
@@ -725,7 +744,7 @@ bool nla_grobner::done() const {
     return false;
 }
 
-bool nla_grobner::compute_basis_loop(){
+bool grobner::compute_basis_loop(){
     int i = 0;
     while (!done()) {
         if (compute_basis_step()) {
@@ -738,11 +757,11 @@ bool nla_grobner::compute_basis_loop(){
     return false;
 }
 
-void nla_grobner::set_gb_exhausted(){
+void grobner::set_gb_exhausted(){
     m_nl_gb_exhausted = true;
 }
 
-void nla_grobner::update_statistics(){
+void grobner::update_statistics(){
     /* todo : implement
       m_stats.m_gb_simplify      += gb.m_stats.m_simplify;
     m_stats.m_gb_superpose     += gb.m_stats.m_superpose;
@@ -751,36 +770,17 @@ void nla_grobner::update_statistics(){
 }
 
 
-bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
+bool grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
     return  (!m_nl_gb_exhausted) &&
         try_to_modify_eqs(eqs, next_weight);
 }
 
-bool nla_grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) {
+bool grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) {
     //    NOT_IMPLEMENTED_YET();
     return false;
 }
 
-
-void nla_grobner::grobner_lemmas() {
-    c().lp_settings().stats().m_grobner_calls++;
-
-    init();
-    
-    ptr_vector<equation> eqs;
-    unsigned next_weight =
-        (unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase. 
-    do {
-        TRACE("grobner", tout << "before:\n"; display(tout););
-        compute_basis();
-        update_statistics();
-        TRACE("grobner", tout << "after:\n"; display(tout););
-        // if (find_conflict(eqs))
-        //     return;
-    }
-    while(push_calculation_forward(eqs, next_weight));
-}
-void nla_grobner:: del_equations(unsigned old_size) {
+void grobner:: del_equations(unsigned old_size) {
     TRACE("grobner", );
     SASSERT(m_equations_to_delete.size() >= old_size);
     equation_vector::iterator it  = m_equations_to_delete.begin();
@@ -794,18 +794,18 @@ void nla_grobner:: del_equations(unsigned old_size) {
     m_equations_to_delete.shrink(old_size);    
 }
 
-void nla_grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
+void grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
     out << header << "\n";
     for (const equation* e : v) 
         display_equation(out, *e);
 }
 
-std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const {
+std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const {
     out << "expr = " << *eq.expr() << "\n";
     display_dependency(out, eq.dep());
     return out;
 }
-std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
+std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
     auto ret = get_vars_of_expr(e);
     auto & ls = c().m_lar_solver;
     do {
@@ -827,7 +827,7 @@ std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const
     } while (true);
 }
 
-void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
+void grobner::assert_eq_0(nex* e, ci_dependency * dep) {
     if (e == nullptr || is_zero_scalar(e))
         return;
     m_tmp_var_set.clear();
@@ -843,7 +843,7 @@ void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
     insert_to_simplify(eq);
 }
 
-void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
+void grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
     unsigned bidx   = m_equations_to_delete.size();
     eq->m_bidx      = bidx;
     eq->dep()       = dep;
@@ -852,11 +852,11 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
 }
 
-nla_grobner::~nla_grobner() {
+grobner::~grobner() {
     del_equations(0);
 }
 
-std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
+std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
     svector<lp::constraint_index> expl;
     m_dep_manager.linearize(dep, expl);   
     {
@@ -872,5 +872,4 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency*
     
     return out;
 }
-    
-} // end of nla namespace
+   
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 25d989840..f0dac37a5 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -36,13 +36,11 @@ struct grobner_stats {
     grobner_stats() { reset(); }
 };
 
-
-class nla_grobner : common {
+class grobner : common {
     class equation {
         unsigned                   m_bidx;       //!< position at m_equations_to_delete
-
-        nex *                      m_expr;           //  simplified expressionted monomials
-        ci_dependency *            m_dep;           //!< justification for the equality
+        nex *                      m_expr;       //   simplified expressionted monomials
+        ci_dependency *            m_dep;        //!< justification for the equality
     public:
         unsigned get_num_monomials() const {
             switch(m_expr->type()) {
@@ -71,7 +69,7 @@ class nla_grobner : common {
         ci_dependency * dep() const { return m_dep; }
         ci_dependency *& dep() { return m_dep; }
         unsigned hash() const { return m_bidx; }
-        friend class nla_grobner;
+        friend class grobner;
     };
 
     typedef obj_hashtable<equation> equation_set;
@@ -95,9 +93,9 @@ class nla_grobner : common {
     bool                                         m_conflict;
     bool                                         m_look_for_fixed_vars_in_rows;
 public:
-    nla_grobner(core *core, intervals *);
+    grobner(core *, intervals *);
     void grobner_lemmas();
-    ~nla_grobner();
+    ~grobner();
 private:
     void find_nl_cluster();
     void prepare_rows_and_active_vars();
@@ -105,8 +103,6 @@ private:
     void init();
     void compute_basis();
     void update_statistics();
-    bool find_conflict(ptr_vector<equation>& eqs);
-    bool is_inconsistent(equation*);
     bool push_calculation_forward(ptr_vector<equation>& eqs, unsigned&);
     void compute_basis_init();        
     bool compute_basis_loop();
@@ -133,7 +129,6 @@ private:
 
     void display_matrix(std::ostream & out) const;
     std::ostream& display(std::ostream & out) const;
-    void get_equations(ptr_vector<equation>& eqs);
     bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
     bool internalize_gb_eq(equation*);
     void add_row(unsigned);
@@ -146,13 +141,13 @@ private:
         m_to_simplify.insert(eq);
     }
     void insert_to_superpose(equation *eq) {
-        SASSERT(m_nex_creator.is_simplified(eq->expr()));
+        SASSERT(m_nex_creator.is_simplified(*eq->expr()));
         TRACE("nla_grobner", display_equation(tout, *eq););
         m_to_superpose.insert(eq);
     }
     void simplify_equations_in_m_to_simplify();
     const nex * get_highest_monomial(const nex * e) const;
-    ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints);
+    ci_dependency* dep_from_vector(svector<lp::constraint_index> & fixed_vars_constraints);
     bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*);    
     unsigned find_divisible(nex_sum*, const nex*) const;    
     void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned);