diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 9de69064d..6c897073d 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -410,7 +410,7 @@ public:
         }
         
         if (b->is_sum() && !to_sum(b)->is_linear()) {
-            nex **ptr_to_a = &((*to_sum(e))[1]);
+            nex **ptr_to_a = &(e->to_sum()[1]);
             push_to_front(front, ptr_to_a);
         }
     }
@@ -419,7 +419,7 @@ public:
         if (b == nullptr) {
             e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a);
             if (!to_sum(a)->is_linear())
-                push_to_front(front, (*to_mul(e))[1].ee());
+                push_to_front(front, e->to_mul()[1].ee());
         } else {
             update_front_with_split_with_non_empty_b(e, j, front, a, b);
         }
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index f1eee286c..14573c769 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -114,17 +114,15 @@ std::ostream& operator<<(std::ostream& out, const nex&);
 
 class nex_var : public nex {
     lpvar m_j;
-public:
-    unsigned number_of_child_powers() const { return 1; }
-    nex_pow get_nex_pow(unsigned j);
+public:    
     nex_var(lpvar j) : m_j(j) {}
-    nex_var() {}
-    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 override { return out << "v" << m_j; }    
 
-    bool contains(lpvar j) const { return j == m_j; }
+    std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }    
+    expr_type type() const override { return expr_type::VAR; }
+    unsigned number_of_child_powers() const override { return 1; }
+    bool contains(lpvar j) const override { return j == m_j; }
     unsigned get_degree() const override { return 1; }
     bool is_linear() const override { return true; }
 };
@@ -133,12 +131,11 @@ class nex_scalar : public nex {
     rational m_v;
 public:
     nex_scalar(const rational& v) : m_v(v) {}
-    nex_scalar() {}
-    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 override { return out << m_v; }
     
+    const rational& value() const {  return m_v; }
+
+    std::ostream& print(std::ostream& out) const override { return out << m_v; }
+    expr_type type() const override { return expr_type::SCALAR; }
     unsigned get_degree() const override { return 0; }
     bool is_linear() const override { return true; }
 };
@@ -146,8 +143,7 @@ public:
 class nex_pow {
     nex* m_e;
     unsigned  m_power;
-public:
-    explicit nex_pow(nex* e): m_e(e), m_power(1) {}
+public:  
     explicit nex_pow(nex* e, unsigned p): m_e(e), m_power(p) {}
     const nex * e() const { return m_e; }
     nex *& e() { return m_e; }
@@ -212,7 +208,7 @@ public:
     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()); }    
+    bool is_pure_monomial() const { return size() == 0 || !m_children[0].e()->is_scalar(); }    
 
     std::ostream & print(std::ostream& out) const override {
         bool first = true;
@@ -247,7 +243,6 @@ public:
         add_child_in_power(p.e(), p.pow());
     }
 
-
     const nex_pow& operator[](unsigned j) const { return m_children[j]; }
     nex_pow& operator[](unsigned j) { return m_children[j]; }
     const nex_pow* begin() const { return m_children.begin(); }
@@ -276,12 +271,11 @@ public:
         TRACE("nla_cn_details", tout << "powers of " << *this << "\n";);
         r.clear();
         for (const auto & c : *this) {
-            if (!c.e()->is_var()) {
-                continue;
+            if (c.e()->is_var()) {
+                lpvar j = c.e()->to_var().var();
+                SASSERT(r.find(j) == r.end());
+                r[j] = c.pow();
             }
-            lpvar j = c.e()->to_var().var();
-            SASSERT(r.find(j) == r.end());
-            r[j] = c.pow();
         }
         TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
     }
@@ -312,12 +306,12 @@ class nex_sum : public nex {
     ptr_vector<nex> m_children;
 public:
     nex_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;}
-    unsigned size() const override { return m_children.size(); }
+    nex_sum(ptr_vector<nex> const& ch) : m_children(ch) {}
 
+    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; }    
+    unsigned size() const override { return m_children.size(); }
 
     bool is_linear() const override {
         TRACE("nex_details", tout << *this << "\n";);
@@ -379,8 +373,6 @@ public:
     nex*& operator[](unsigned j) { return m_children[j]; }
     const ptr_vector<nex>::const_iterator begin() const { return m_children.begin(); }
     const ptr_vector<nex>::const_iterator end() const { return m_children.end(); }
-    ptr_vector<nex>::iterator begin() { return m_children.begin(); }
-    ptr_vector<nex>::iterator end() { return m_children.end(); }
 
     void add_child(nex* e) { m_children.push_back(e); }
 #ifdef Z3DEBUG
@@ -432,20 +424,20 @@ inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var
         return to_scalar(e)->value();
     case expr_type::SUM: {
         rational r(0);
-        for (auto c: *to_sum(e)) {
+        for (nex* c: e->to_sum()) {
             r += get_nex_val(c, var_val);
         }
         return r;
     }
     case expr_type::MUL: {
-        auto & m = *to_mul(e);
+        auto & m = e->to_mul();
         rational t = m.coeff();
-        for (auto& c: m)
+        for (nex_pow const& c: m)
             t *= get_nex_val(c.e(), var_val).expt(c.pow());
         return t;
     }
     case expr_type::VAR:
-        return var_val(to_var(e)->var());
+        return var_val(e->to_var().var());
     default:
         TRACE("nla_cn_details", tout << e->type() << "\n";);
         SASSERT(false);
@@ -458,20 +450,18 @@ inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
     switch (e->type()) {
     case expr_type::SCALAR:
         return r;
-    case expr_type::SUM: {
-        for (auto c: *to_sum(e))
+    case expr_type::SUM: 
+        for (auto c: e->to_sum())
             for ( lpvar j : get_vars_of_expr(c))
                 r.insert(j);
-        return r;
-    }
-    case expr_type::MUL: {
-        for (auto &c: *to_mul(e))
+        return r;    
+    case expr_type::MUL: 
+        for (auto &c: e->to_mul())
             for ( lpvar j : get_vars_of_expr(c.e()))
                 r.insert(j);
-        return r;
-    }
+        return r;    
     case expr_type::VAR:
-        r.insert(to_var(e)->var());
+        r.insert(e->to_var().var());
         return r;
     default:
         TRACE("nla_cn_details", tout << e->type() << "\n";);
@@ -481,7 +471,7 @@ inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
 }
 
 inline bool is_zero_scalar(nex *e) {
-    return e->is_scalar() && to_scalar(e)->value().is_zero();
+    return e->is_scalar() && e->to_scalar().value().is_zero();
 }
 }
     
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index e27e2af78..7dd6b4dd0 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -39,7 +39,7 @@ nex * nex_creator::mk_div(const nex& a, lpvar j) {
         if (!seenj && c->contains(j)) {
             SASSERT(!c->is_var() || c->to_var().var() == j);
             if (!c->is_var()) {
-                bv.push_back(nex_pow(mk_div(*c, j)));
+                bv.push_back(nex_pow(mk_div(*c, j), 1));
             }
             if (pow != 1) {
                 bv.push_back(nex_pow(clone(c), pow - 1));
@@ -437,42 +437,6 @@ void nex_creator::mul_to_powers(vector<nex_pow>& children) {
                                                 });
 }
 
-nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
-                                                  const rational& coeff) {
-    TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";);
-    if (coeff.is_one())
-        return e;
-    SASSERT(is_simplified(*e));
-    switch (e->type()) {
-    case expr_type::VAR: {
-        if (coeff.is_one())
-            return e;
-        return mk_mul(mk_scalar(coeff), e);
-    }
-    case expr_type::SCALAR: {
-        return mk_scalar(coeff);
-    }        
-    case expr_type::MUL: {
-        nex_mul * em = to_mul(e);
-        nex_pow *np = em->begin();
-        if (np->e()->is_scalar()) {
-            SASSERT(np->pow() == 1);
-            to_scalar(np->e())->value() = coeff;
-            return e;
-        }
-        em->add_child(mk_scalar(coeff));
-        std::sort(em->begin(), em->end(), [this](const nex_pow& a,
-                                                 const nex_pow& b) {return gt_on_nex_pow(a, b); });
-        return em;
-    }
-    case expr_type::SUM: 
-        return mk_mul(mk_scalar(coeff), e);
-    default:
-        UNREACHABLE();
-        return nullptr;
-    }
-        
-}
 // returns true if the key exists already
 bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, nex* e, const rational& r) const{
     TRACE("grobner_d",  tout << *e << ", r = " << r << std::endl;);
@@ -492,18 +456,12 @@ bool nex_creator::fill_join_map_for_sum(
     ptr_vector<nex> & children,
     std::map<nex*, rational, nex_lt>& map,
     std::unordered_set<nex*>& existing_nex,
-    nex_scalar*& common_scalar) {
-    common_scalar = nullptr;
+    rational& common_scalar) {
     bool simplified = false;
     for (auto e : children) {
         if (e->is_scalar()) {
-            nex_scalar * es = to_scalar(e);
-            if (common_scalar == nullptr) {
-                common_scalar = es;
-            } else {
-                simplified = true;
-                common_scalar->value() += es->value();
-            }
+            simplified = true;
+            common_scalar += e->to_scalar().value();           
             continue;
         }
         existing_nex.insert(e);
@@ -523,7 +481,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 = nullptr;
+    rational common_scalar(0);
     fill_join_map_for_sum(children, map, allocated_nexs, common_scalar);
 
     TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
@@ -531,8 +489,8 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
     for (auto& p : map) {
         process_map_pair(p.first, p.second, children, allocated_nexs);
     }
-    if (common_scalar && !common_scalar->value().is_zero()) {
-        children.push_back(common_scalar);
+    if (!common_scalar.is_zero()) {
+        children.push_back(mk_scalar(common_scalar));
     }
     TRACE("grobner_d",
           tout << "map=";
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 7f38c3fe7..b24348668 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -162,9 +162,8 @@ public:
     }
 
     nex_sum* mk_sum(const ptr_vector<nex>& v) {
-        auto r = new nex_sum();
+        auto r = new nex_sum(v);
         add_to_allocated(r);
-        r->children() = v;
         return r;
     }
 
@@ -227,20 +226,17 @@ public:
     
     void mul_to_powers(vector<nex_pow>& children);
     
-    nex* create_child_from_nex_and_coeff(nex *e,
-                                         const rational& coeff) ;
 
     void sort_join_sum(ptr_vector<nex> & children);
     bool fill_join_map_for_sum(ptr_vector<nex> & children,
                                std::map<nex*, rational, nex_lt>& map,
                                std::unordered_set<nex*>& existing_nex,
-                               nex_scalar*& common_scalar);
+                               rational& common_scalar);
     bool register_in_join_map(std::map<nex*, rational, nex_lt>&, nex*, const rational&) const;
 
     void simplify_children_of_sum(ptr_vector<nex> & children);
     
     bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned);
-    void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars, std::function<nex_scalar*()> mk_scalar);
 
     bool children_are_simplified(const vector<nex_pow>& children) const;
     bool gt(const nex* a, const nex* b) const;    
@@ -253,7 +249,6 @@ public:
     bool gt_on_var_nex(const nex_var* a, const nex* b) const;
     bool gt_on_mul_nex(const nex_mul* a, const nex* b) const;
     bool gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const;
-    void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
     void process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>&);
 #ifdef Z3DEBUG
     static
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 44da9303a..6a766efe0 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -62,7 +62,7 @@ void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::qu
     for (auto & s : matrix.m_columns[j]) {
         unsigned row = s.var();
         if (m_rows.contains(row)) continue;
-        if (false && c().var_is_free(core_slv.m_r_basis[row])) {
+        if (c().var_is_free(core_slv.m_r_basis[row])) {
              TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";); 
              continue; // mimic the behavior of the legacy solver
         }
@@ -345,7 +345,7 @@ bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
 
 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 and k runs over h
+    unsigned j = 0; // j points to t and k runs over h
     for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
         lpvar h_var = to_var(h->get_child_exp(k))->var();
         for (; j < t->size(); j++) {
@@ -701,15 +701,14 @@ bool grobner::done() const {
 }
 
 bool grobner::compute_basis_loop(){
-    int i = 0;
     while (!done()) {
         if (compute_basis_step()) {
             TRACE("grobner", tout << "progress in compute_basis_step\n";);
             return true;
         }
-        TRACE("grobner", tout << "continue compute_basis_loop i= " << ++i << "\n";);
+        TRACE("grobner", tout << "continue compute_basis_loop\n";);
     }
-    TRACE("grobner", tout << "return false from compute_basis_loop i= " << i << "\n";);
+    TRACE("grobner", tout << "return false from compute_basis_loop\n";);
     return false;
 }
 
@@ -793,8 +792,7 @@ void grobner::assert_eq_0(nex* e, ci_dependency * dep) {
           display_equation(tout, *eq);
           tout << "\nvars\n";
           for (unsigned j : get_vars_of_expr_with_opening_terms(e)) {
-              tout << "(";
-              c().print_var(j, tout) << ")\n";
+              c().print_var(j, tout << "(") << ")\n";
           });
     insert_to_simplify(eq);
 }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index f3e0786ab..b8c63f497 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -52,7 +52,7 @@ class grobner : common {
             }
         }
         // can return not a nex_mul
-        nex* get_monomial(unsigned idx) const {
+        nex const* get_monomial(unsigned idx) const {
             switch(m_expr->type()) {
             case expr_type::VAR:
             case expr_type::SCALAR: UNREACHABLE();;
@@ -60,7 +60,7 @@ class grobner : common {
                 SASSERT(idx == 0);
                 return m_expr;
             case expr_type::SUM:
-                return (*to_sum(m_expr))[idx];
+                return m_expr->to_sum()[idx];
             default: return 0;
             }
         }