diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index b38eab508..ebd1dd66b 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -83,7 +83,7 @@ public:
         TRACE("nla_cn", tout << "c=" << *c << "\n"; tout << "occs:"; dump_occurences(tout, m_nex_creator.occurences_map()) << "\n";);
         unsigned size = c->size();
         bool have_factor = false;
-        for(const auto & p : m_nex_creator.occurences_map()) {
+        for (const auto & p : m_nex_creator.occurences_map()) {
             if (p.second.m_occs == size) {
                 have_factor = true;
                 break;
@@ -91,7 +91,7 @@ public:
         }
         if (have_factor == false) return nullptr;
         nex_mul* f = m_nex_creator.mk_mul();
-        for(const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo
+        for (const auto & p : m_nex_creator.occurences_map()) { // randomize here: todo
             if (p.second.m_occs == size) {
                 f->add_child_in_power(m_nex_creator.mk_var(p.first), p.second.m_power);
             }
@@ -105,7 +105,7 @@ public:
         auto common_vars = get_vars_of_expr(ch[0]);
         for (lpvar j : common_vars) {
             bool divides_the_rest = true;
-            for(unsigned i = 1; i < ch.size() && divides_the_rest; i++) {
+            for (unsigned i = 1; i < ch.size() && divides_the_rest; i++) {
                 if (!ch[i]->contains(j))
                     divides_the_rest = false;
             }
@@ -163,7 +163,7 @@ public:
         nex* copy_of_c = *c;
         auto copy_of_front = copy_front(front);
         int alloc_size = m_nex_creator.size();
-        for(lpvar j : vars) {
+        for (lpvar j : vars) {
             if (m_var_is_fixed(j)) {
                 // it does not make sense to explore fixed multupliers
                 // because the interval products do not become smaller
@@ -184,9 +184,8 @@ public:
     template <typename T>
     static std::ostream& dump_occurences(std::ostream& out, const T& occurences) {
         out << "{";
-        for(const auto& p: occurences) {
-            const occ& o = p.second;
-            out << "(v" << p.first << "->" << o << ")";
+        for (const auto& p: occurences) {
+            out << "(v" << p.first << "->" << p.second << ")";
         }
         out << "}" << std::endl;
         return out;
@@ -252,7 +251,7 @@ public:
               print_vector(vars, tout) << "; front:"; print_front(front, tout) << "\n";);
     
         if (vars.empty()) {
-            if(front.empty()) {
+            if (front.empty()) {
                 TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
                 m_done = m_call_on_result(m_e) || ++m_reported > 100;
  #ifdef Z3DEBUG
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 265c83ead..7e973baad 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -108,8 +108,7 @@ public:
     lpvar& var() {  return m_j; } // the setter
     std::ostream & print(std::ostream& out) const {
         //        out <<  (char)('a' + m_j);
-        out << "v" << m_j;
-        return out;
+        return out << "v" << m_j;
     }    
 
     bool contains(lpvar j) const { return j == m_j; }
@@ -125,10 +124,7 @@ 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 {
-        out << m_v;
-        return out;
-    }
+    std::ostream& print(std::ostream& out) const { return out << m_v; }
     
     int get_degree() const { return 0; }
     bool is_linear() const { return true; }
@@ -136,7 +132,6 @@ public:
 
 const nex_scalar * to_scalar(const nex* a);
 class nex_sum;
-const nex_sum* to_sum(const nex*a);
 
 class nex_pow {
     nex* m_e;
@@ -149,25 +144,30 @@ public:
     
     nex ** ee() { return & m_e; }
     int pow() const { return m_power; }
-    int& pow() { return m_power; }
-    std::string to_string() const {
-        std::stringstream s;
+
+    std::ostream& print(std::ostream& s) const {
         if (pow() == 1) {
             if (e()->is_elementary()) {
                 s << *e();
             } else {
                 s <<"(" <<  *e() << ")";
             }
-        } else {
+        } 
+        else {
             if (e()->is_elementary()){
                 s << "(" << *e() << "^" << pow() << ")";
             } else {
                 s << "((" << *e() << ")^" << pow() << ")";
             }
         }
+        return s;
+    }
+    std::string to_string() const {
+        std::stringstream s;
+        print(s);
         return s.str();
     }
-    friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; }
+    friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { return p.print(out); }
 };
 
 inline unsigned get_degree_children(const vector<nex_pow>& children) {
@@ -206,20 +206,19 @@ public:
     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 {        
         bool first = true;
         if (!m_coeff.is_one()) {
             out << m_coeff;
             first = false;
         }
         for (const nex_pow& v : m_children) {            
-            std::string s = v.to_string();
             if (first) {
                 first = false;
-                out << s;
+                out << v;
             } else {
-                out << "*" << s;                        
+                out << "*" << v;                        
             }
         }
         return out;
@@ -252,9 +251,10 @@ public:
     void add_child_in_power(nex* e, int power) {        
         if (e->is_scalar()) {
             m_coeff *= (to_scalar(e)->value()).expt(power);
-            return;
         }
-        m_children.push_back(nex_pow(e, power));
+        else {
+            m_children.push_back(nex_pow(e, power));
+        }
     }
 
     bool contains(lpvar j) const {
@@ -335,8 +335,7 @@ public:
         for (auto  e : *this) {
             int d = e->get_degree();
             if (d == 0) continue;
-            if (d > 1) return false;
-            
+            if (d > 1) return false;            
             number_of_non_scalars++;
         }
         TRACE("nex_details", tout << (number_of_non_scalars > 1?"linear":"non-linear") << "\n";); 
@@ -398,7 +397,7 @@ public:
 #endif
 };
 
-inline const nex_sum* to_sum(const nex*a) {
+inline const nex_sum* to_sum(const nex* a) {
     SASSERT(a->is_sum());
     return static_cast<const nex_sum*>(a);
 }
@@ -407,7 +406,6 @@ inline nex_sum* to_sum(nex * a) {
     SASSERT(a->is_sum());
     return static_cast<nex_sum*>(a);
 }
-
     
 inline const nex_var* to_var(const nex*a)  {
     SASSERT(a->is_var());
@@ -447,22 +445,20 @@ inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var
     switch (e->type()) {
     case expr_type::SCALAR:
         return to_scalar(e)->value();
-    case expr_type::SUM:
-        {
-            rational r(0);
-            for (auto c: *to_sum(e)) {
-                r += get_nex_val(c, var_val);
-            }
-            return r;
-        }
-    case expr_type::MUL:
-        {
-            const nex_mul * m = to_mul(e);
-            rational t = m->coeff();
-            for (auto& c: *m)
-                t *= get_nex_val(c.e(), var_val).expt(c.pow());
-            return t;
+    case expr_type::SUM: {
+        rational r(0);
+        for (auto c: *to_sum(e)) {
+            r += get_nex_val(c, var_val);
         }
+        return r;
+    }
+    case expr_type::MUL: {
+        auto & m = *to_mul(e);
+        rational t = m.coeff();
+        for (auto& 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());
     default:
@@ -477,20 +473,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))
-                for ( lpvar j : get_vars_of_expr(c))
-                    r.insert(j);
-        }
+    case expr_type::SUM: {
+        for (auto c: *to_sum(e))
+            for ( lpvar j : get_vars_of_expr(c))
+                r.insert(j);
         return r;
-    case expr_type::MUL:
-        {
-            for (auto &c: *to_mul(e))
-                for ( lpvar j : get_vars_of_expr(c.e()))
-                    r.insert(j);
-        }
+    }
+    case expr_type::MUL: {
+        for (auto &c: *to_mul(e))
+            for ( lpvar j : get_vars_of_expr(c.e()))
+                r.insert(j);
         return r;
+    }
     case expr_type::VAR:
         r.insert(to_var(e)->var());
         return r;
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 7c8cbc70d..8ac9f8214 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -17,9 +17,9 @@
 
 
   --*/
+#include "util/lbool.h"
 #include "math/lp/nex_creator.h"
 #include <map>
-#include <vector>
 
 namespace nla {
 
@@ -30,8 +30,8 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
         return mk_scalar(rational(1));
     vector<nex_pow> bv; 
     bool seenj = false;
-    auto ma = to_mul(a);
-    for (auto& p : *ma) {
+    auto ma = *to_mul(a);
+    for (auto& p : ma) {
         const nex * c = p.e();
         int pow = p.pow();
         if (!seenj && c->contains(j)) {
@@ -51,24 +51,24 @@ nex * nex_creator::mk_div(const nex* a, lpvar j) {
             bv.push_back(nex_pow(clone(c), pow));
         }
     }
-    if (bv.size() == 1 && bv.begin()->pow() == 1 && ma->coeff().is_one()) {
+    if (bv.size() == 1 && bv.begin()->pow() == 1 && ma.coeff().is_one()) {
         return bv.begin()->e();
     }
-    if (bv.size() == 0) {
-        return mk_scalar(rational(ma->coeff()));
+    if (bv.empty()) {
+        return mk_scalar(rational(ma.coeff()));
     }
     
     auto m = mk_mul(bv);
-    m->coeff() = ma->coeff();
+    m->coeff() = ma.coeff();
     return m;
 
 }
 
 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());
-        if (m->size() == 0) {
-            const rational& coeff = m->coeff();
+        const nex_mul & m = *to_mul(p.e());
+        if (m.size() == 0) {
+            const rational& coeff = m.coeff();
             if (coeff.is_one())
                 return true;
             r *= coeff.expt(p.pow() * pow);
@@ -90,7 +90,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
     TRACE("grobner_d", print_vector(children, tout););
     vector<nex_pow> to_promote;
     int skipped = 0;
-    for(unsigned j = 0; j < children.size(); j++) {        
+    for (unsigned j = 0; j < children.size(); j++) {        
         nex_pow& p = children[j];
         if (eat_scalar_pow(coeff, p, 1)) {
             skipped++;
@@ -112,49 +112,48 @@ 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 = *to_mul(p.e());
+        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);
     
     TRACE("grobner_d", print_vector(children, tout););    
 }
-bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul* b) const {
+bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul& b) const {
     bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
     bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
     auto it_a  = a.begin();
-    auto it_b  = b->begin();
+    auto it_b  = b.begin();
     auto a_end = a.end();
-    auto b_end = b->end();
+    auto b_end = b.end();
     unsigned a_pow, b_pow;
-    int ret = - 1;
-    do {
+    lbool ret = l_undef;
+    while (true) {
         if (!inside_a_p) { a_pow = it_a->pow(); }
         if (!inside_b_p) { b_pow = it_b->pow(); }
         if (lt(it_a->e(), it_b->e())){
-            ret = true;
+            ret = l_true;
             break;
         }
         if (lt(it_b->e(), it_a->e())) {
-            ret = false;
+            ret = l_false;
             break;
         }
-
         if (a_pow == b_pow) {
             inside_a_p = inside_b_p = false;
             it_a++; it_b++;
             if (it_a == a_end) {
-                ret = false;
+                ret = l_false;
                 break;
             }
             if (it_b == b_end) { // it_a is not at the end
-                ret = false;
+                ret = l_false;
                 break;
             }
             // no iterator reached the end
@@ -163,7 +162,7 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a,
         if (a_pow > b_pow) {
             it_a++;
             if (it_a == a_end) {
-                ret = true;
+                ret = l_true;
                 break;
             }
             inside_a_p = false;
@@ -174,54 +173,51 @@ bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a,
             a_pow -= b_pow;
             it_b++;
             if (it_b == b_end) {
-                ret = false;
+                ret = l_false;
                 break;
             }
             inside_a_p = true;
             inside_b_p = false;
         }
-    } while (true);
-    if (ret == -1)
-        ret = true;
-    TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";);
-    return ret;
+    }
+    TRACE("nex_less", tout << "a = "; print_vector(a, tout) << (ret != l_false?" < ":" >= ") << b << "\n";);
+    return ret != l_false;
 }
 
-bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {
+bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const {
     bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
     bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
-    auto it_a  = a->begin();
-    auto it_b  = b->begin();
-    auto a_end = a->end();
-    auto b_end = b->end();
+    auto it_a  = a.begin();
+    auto it_b  = b.begin();
+    auto a_end = a.end();
+    auto b_end = b.end();
     unsigned a_pow, b_pow;
-    int ret = - 1;
-    do {
+    lbool ret = l_undef;
+    while (true) {
         if (!inside_a_p) { a_pow = it_a->pow(); }
         if (!inside_b_p) { b_pow = it_b->pow(); }
         if (lt(it_a->e(), it_b->e())){
-            ret = true;
+            ret = l_true;
             break;
         }
         if (lt(it_b->e(), it_a->e())) {
-            ret = false;
+            ret = l_false;
             break;
         }
-
         if (a_pow == b_pow) {
             inside_a_p = inside_b_p = false;
             it_a++; it_b++;
             if (it_a == a_end) {
                 if (it_b != b_end) {
-                    ret = false;
+                    ret = l_false;
                     break;
                 }
                 SASSERT(it_a == a_end && it_b == b_end);
-                ret = a->coeff() > b->coeff();
+                ret = to_lbool(a.coeff() > b.coeff());
                 break;
             }
             if (it_b == b_end) { // it_a is not at the end
-                ret = false;
+                ret = l_false;
                 break;
             }
             // no iterator reached the end
@@ -230,7 +226,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
         if (a_pow > b_pow) {
             it_a++;
             if (it_a == a_end) {
-                ret = true;
+                ret = l_true;
                 break;
             }
             inside_a_p = false;
@@ -241,17 +237,15 @@ bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_m
             a_pow -= b_pow;
             it_b++;
             if (it_b == b_end) {
-                ret = false;
+                ret = l_false;
                 break;
             }
             inside_a_p = true;
             inside_b_p = false;
         }
-    } while (true);
-    if (ret == -1)
-        ret = true;
-    TRACE("grobner_d", tout << "a = " << *a << (ret == 1?" < ":" >= ") << *b << "\n";);
-    return ret;
+    } 
+    TRACE("grobner_d", tout << "a = " << a << (ret != l_false?" < ":" >= ") << b << "\n";);
+    return ret != l_false;
 }
 
 bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
@@ -260,60 +254,34 @@ bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const
             return false;
     return true;
 }
-bool nex_creator::less_than_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));
+
+bool nex_creator::less_than_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));
     unsigned a_deg = get_degree_children(children);
-    unsigned b_deg = b->get_degree();
-    bool ret;
-    if (a_deg > b_deg) {
-        ret = true;
-    } else if (a_deg < b_deg) {
-        ret = false;
-    } else {
-        ret = less_than_on_powers_mul_same_degree(children, b);
-    }
-    return ret;
+    unsigned b_deg = b.get_degree();
 
+    return a_deg == b_deg ? less_than_on_powers_mul_same_degree(children, b) : a_deg > b_deg;
 }
 
-
-bool nex_creator::less_than_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));
-    unsigned a_deg = a->get_degree();
-    unsigned b_deg = b->get_degree();
-    bool ret;
-    if (a_deg > b_deg) {
-        ret = true;
-    } else if (a_deg < b_deg) {
-        ret = false;
-    } else {
-        ret = less_than_on_mul_mul_same_degree(a, b);
-    }
-    return ret;
-
+bool nex_creator::less_than_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));
+    unsigned a_deg = a.get_degree();
+    unsigned b_deg = b.get_degree();
+    return a_deg == b_deg ? less_than_on_mul_mul_same_degree(a, b) : a_deg > b_deg;
 }
 
-
 bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
-    switch(b->type()) {
-    case expr_type::SCALAR: return true;
+    switch (b->type()) {
+    case expr_type::SCALAR: 
+        return true;
     case expr_type::VAR:            
         return less_than(a->var() , to_var(b)->var());
-    case expr_type::MUL:
-        {
-            if (b->get_degree() > 1)
-                return false;
-            auto it = to_mul(b)->begin();
-            const nex_pow & c  = *it;
-            const nex * f = c.e();
-            return less_than_on_var_nex(a, f);
-        }
+    case expr_type::MUL: 
+        return b->get_degree() <= 1 && less_than_on_var_nex(a, (*to_mul(b))[0].e());
     case expr_type::SUM:
-        {
-            return !lt((*to_sum(b))[0], a);
-        }
+        return !lt((*to_sum(b))[0], a);        
     default:
         UNREACHABLE();
         return false;
@@ -321,21 +289,20 @@ bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
 }
 
 bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) const {
-    switch(b->type()) {
-    case expr_type::SCALAR: return false;
-    case expr_type::VAR:            
-        {
-            if (get_degree_children(children) > 1)
-                return true;
-            auto it = children.begin();
-            const nex_pow & c  = *it;
-            SASSERT(c.pow() == 1);
-            const nex * f = c.e();
-            SASSERT(!f->is_scalar());
-            return lt(f, b);
-        }
+    switch (b->type()) {
+    case expr_type::SCALAR: 
+        return false;
+    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 lt(f, b);
+    }
     case expr_type::MUL:
-        return less_than_on_powers_mul(children, to_mul(b));            
+        return less_than_on_powers_mul(children, *to_mul(b));            
     case expr_type::SUM:
         return lt_nex_powers(children, (*to_sum(b))[0]);
     default:
@@ -344,23 +311,21 @@ bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) c
     }    
 }
 
-
 bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
-    switch(b->type()) {
-    case expr_type::SCALAR: return false;
-    case expr_type::VAR:            
-        {
-            if (a->get_degree() > 1)
-                return true;
-            auto it = a->begin();
-            const nex_pow & c  = *it;
-            SASSERT(c.pow() == 1);
-            const nex * f = c.e();
-            SASSERT(!f->is_scalar());
-            return lt(f, b);
-        }
+    switch (b->type()) {
+    case expr_type::SCALAR: 
+        return false;
+    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 lt(f, b);
+    }
     case expr_type::MUL:
-        return less_than_on_mul_mul(a, to_mul(b));            
+        return less_than_on_mul_mul(*a, *to_mul(b));            
     case expr_type::SUM:
         return lt(a, (*to_sum(b))[0]);
     default:
@@ -391,22 +356,19 @@ bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const {
     case expr_type::VAR: 
         ret = less_than_on_var_nex(to_var(a), b);
         break;
-    case expr_type::SCALAR: {
+    case expr_type::SCALAR: 
         if (b->is_scalar())
             ret = to_scalar(a)->value() > to_scalar(b)->value();
         else
             ret = false; // the scalars are the largest
         break;
-    }        
-    case expr_type::MUL: {
+    case expr_type::MUL: 
         ret = lt_nex_powers(to_mul(a)->children(), b);
         break;
-    }
-    case expr_type::SUM: {
+    case expr_type::SUM: 
         if (b->is_sum())
             return less_than_on_sum_sum(to_sum(a), to_sum(b));
         return lt((*to_sum(a))[0], b);
-    }
     default:
         UNREACHABLE();
         return false;
@@ -424,22 +386,17 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
     case expr_type::VAR: 
         ret = less_than_on_var_nex(to_var(a), b);
         break;
-    case expr_type::SCALAR: {
-        if (b->is_scalar())
-            ret = to_scalar(a)->value() > to_scalar(b)->value();
-        else
-            ret = false; // the scalars are the largest
+    case expr_type::SCALAR: 
+        ret = b->is_scalar() && to_scalar(a)->value() > to_scalar(b)->value();
+        // the scalars are the largest
         break;
-    }        
-    case expr_type::MUL: {
+    case expr_type::MUL: 
         ret = less_than_on_mul_nex(to_mul(a), b);
         break;
-    }
-    case expr_type::SUM: {
+    case expr_type::SUM: 
         if (b->is_sum())
             return less_than_on_sum_sum(to_sum(a), to_sum(b));
         return lt((*to_sum(a))[0], b);
-    }
     default:
         UNREACHABLE();
         return false;
@@ -460,9 +417,6 @@ 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) {
@@ -562,14 +516,14 @@ bool nex_creator::sum_is_simplified(const nex_sum* e) const {
 }
 
 void nex_creator::mul_to_powers(vector<nex_pow>& children) {
-    std::map<nex*, int, nex_lt> m([this](const nex* a, const nex* b) {return lt(a, b); });
+    std::map<nex*, int, nex_lt> m([this](const nex* a, const nex* b) { return lt(a, b); });
 
     for (auto & p : children) {
         auto it = m.find(p.e());
         if (it == m.end()) {
             m[p.e()] = p.pow();
         } else {
-            it->second+= p.pow();
+            it->second += p.pow();
         }
     }
     children.clear();
@@ -607,12 +561,11 @@ nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
         }
         em->add_child(mk_scalar(coeff));
         std::sort(em->begin(), em->end(), [this](const nex_pow& a,
-                                                                       const nex_pow& b) {return less_than_on_nex_pow(a, b);});
+                                                 const nex_pow& b) {return less_than_on_nex_pow(a, b); });
         return em;
     }
-    case expr_type::SUM: {
+    case expr_type::SUM: 
         return mk_mul(mk_scalar(coeff), e);
-    }
     default:
         UNREACHABLE();
         return nullptr;
@@ -634,10 +587,11 @@ bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, ne
     }
 }
 
-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) {
+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;
     bool simplified = false;
     for (auto e : children) {
@@ -690,7 +644,7 @@ 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;
     int skipped = 0;
-    for(unsigned j = 0; j < children.size(); j++) {
+    for (unsigned j = 0; j < children.size(); j++) {
         nex* e = children[j] = simplify(children[j]);
         if (e->is_sum()) {
             to_promote.push_back(e);
@@ -828,6 +782,7 @@ nex* nex_creator::simplify(nex* e) {
     SASSERT(is_simplified(es));
     return es;
 }
+
 // adds to children the corrected expression and also adds to allocated the new expressions
 void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>& allocated_nexs) {
     TRACE("grobner_d", tout << "e=" << *e << " , coeff= " << coeff << "\n";);
@@ -870,6 +825,7 @@ unsigned nex_creator::find_sum_in_mul(const nex_mul* a) const {
 
     return -1;
 }
+
 nex* nex_creator::canonize_mul(nex_mul *a) {    
     TRACE("grobner_d", tout << "a = " << *a << "\n";);
     unsigned j = find_sum_in_mul(a);
@@ -897,7 +853,6 @@ nex* nex_creator::canonize_mul(nex_mul *a) {
     return canonize(r);
 }
 
-
 nex* nex_creator::canonize(const nex *a) {
     if (a->is_elementary())
         return clone(a);
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 8192b613f..d6e0b3c83 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -29,22 +29,21 @@ struct occ {
     occ(unsigned k, unsigned p) : m_occs(k), m_power(p) {}
     // use the "name injection rule here"
     friend std::ostream& operator<<(std::ostream& out, const occ& c) {
-        out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")";
-        return out;
+        return out << "(occs:" << c.m_occs <<", pow:" << c.m_power << ")";
     }
 };
 
-enum class var_weight {
-            FIXED = 0,
-            QUOTED_FIXED =  1,
-            BOUNDED    =    2,
-            QUOTED_BOUNDED = 3,
-            NOT_FREE      =  4,
-            QUOTED_NOT_FREE = 5,
-            FREE          =   6,
-            QUOTED_FREE    = 7,
-            MAX_DEFAULT_WEIGHT = 7
-            };
+enum var_weight {
+    FIXED = 0,
+    QUOTED_FIXED =  1,
+    BOUNDED    =    2,
+    QUOTED_BOUNDED = 3,
+    NOT_FREE      =  4,
+    QUOTED_NOT_FREE = 5,
+    FREE          =   6,
+    QUOTED_FREE    = 7,
+    MAX_DEFAULT_WEIGHT = 7
+};
 
 
 // the purpose of this class is to create nex objects, keep them,
@@ -54,14 +53,13 @@ class nex_creator {
     ptr_vector<nex>                              m_allocated;
     std::unordered_map<lpvar, occ>               m_occurences_map;
     std::unordered_map<lpvar, unsigned>          m_powers;
-    svector<unsigned>                            m_active_vars_weights;
+    unsigned_vector                              m_active_vars_weights;
 
 public:
     static std::string ch(unsigned j) {
         std::stringstream s;
         s << "v" << j;        
         return s.str();
-          // return (char)('a'+j);
     }
 
     // assuming that every lpvar is less than this number
@@ -72,11 +70,11 @@ public:
     unsigned get_number_of_vars() const {
         return m_active_vars_weights.size();
     }
-
     
     void set_var_weight(unsigned j, unsigned weight) {
         m_active_vars_weights[j] = weight;
     }
+
 private:
     svector<unsigned>& active_vars_weights() { return m_active_vars_weights;}
     const svector<unsigned>& active_vars_weights() const { return m_active_vars_weights;}
@@ -84,8 +82,8 @@ public:
     nex* simplify(nex* e);
     
     bool less_than(lpvar j, lpvar k) const{
-        unsigned wj = (unsigned)m_active_vars_weights[j];
-        unsigned wk = (unsigned)m_active_vars_weights[k];
+        unsigned wj = m_active_vars_weights[j];
+        unsigned wk = m_active_vars_weights[k];
         return wj != wk ? wj > wk : j > k;
     }
 
@@ -97,15 +95,10 @@ public:
 
     nex * clone(const nex* a) {        
         switch (a->type()) {
-        case expr_type::VAR: {
-            auto v = to_var(a);
-            return mk_var(v->var());
-        }
-            
-        case expr_type::SCALAR: {
-            auto v = to_scalar(a);
-            return mk_scalar(v->value());
-        }
+        case expr_type::VAR: 
+            return mk_var(to_var(a)->var());
+        case expr_type::SCALAR: 
+            return mk_scalar(to_scalar(a)->value());
         case expr_type::MUL: {
             auto m = to_mul(a);
             auto r = mk_mul();
@@ -116,9 +109,8 @@ public:
             return r;
         }
         case expr_type::SUM: {
-            auto m = to_sum(a);
             auto r = mk_sum();
-            for (nex * e : m->children()) {
+            for (nex * e : *to_sum(a)) {
                 r->add_child(clone(e));
             }
             return r;
@@ -181,7 +173,6 @@ public:
         r->children() = v;
         return r;
     }
-
     
     template <typename K, typename...Args>
     nex_sum* mk_sum(K e, Args... es) {
@@ -191,6 +182,7 @@ public:
         add_children(r, es...);
         return r;
     }
+
     nex_var* mk_var(lpvar j) {
         auto r = new nex_var(j);
         add_to_allocated(r);
@@ -239,8 +231,8 @@ public:
 
     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,
+                               std::map<nex*, rational, nex_lt>& map,
+                               std::unordered_set<nex*>& existing_nex,
                                nex_scalar*& common_scalar);
     bool register_in_join_map(std::map<nex*, rational, nex_lt>&, nex*, const rational&) const;
 
@@ -252,11 +244,11 @@ public:
     bool children_are_simplified(const vector<nex_pow>& children) const;
     bool lt(const nex* a, const nex* b) const;    
     bool lt_nex_powers(const vector<nex_pow>&, const nex* b) const;    
-    bool less_than_on_powers_mul(const vector<nex_pow>&, const nex_mul* b) const;    
-    bool less_than_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul* b) const;    
+    bool less_than_on_powers_mul(const vector<nex_pow>&, const nex_mul& b) const;    
+    bool less_than_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul& b) const;    
     bool lt_for_sort_join_sum(const nex* a, const nex* b) const;    
-    bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const;
-    bool less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const;
+    bool less_than_on_mul_mul(const nex_mul& a, const nex_mul& b) const;
+    bool less_than_on_mul_mul_same_degree(const nex_mul& a, const nex_mul& b) const;
     bool less_than_on_var_nex(const nex_var* a, const nex* b) const;
     bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const;
     bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const;
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index d201ed949..4538e9227 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -178,7 +178,7 @@ void nla_grobner::del_equation(equation * eq) {
     m_to_superpose.erase(eq);
     m_to_simplify.erase(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
-    m_equations_to_delete[eq->m_bidx] = 0;
+    m_equations_to_delete[eq->m_bidx] = nullptr;
     dealloc(eq);
 }