diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index fd5040b24..b6f141c52 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -116,7 +116,7 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children) {
     TRACE("nla_cn_details", print_vector(children, tout););    
 }
 
-bool nex_creator::mul_simplify_lt(const nex_mul* a, const nex_mul* b) {
+bool nex_creator::less_than_on_mul(const nex_mul* a, const nex_mul* b) {
     NOT_IMPLEMENTED_YET();
 }
 
@@ -135,7 +135,7 @@ bool nex_creator::sum_simplify_lt(const nex* a, const nex* b) {
         return to_scalar(a)->value() < to_scalar(b)->value();
     }        
     case expr_type::MUL: {
-        return mul_simplify_lt(to_mul(a), to_mul(b));
+        return less_than_on_mul(to_mul(a), to_mul(b));
     }
     case expr_type::SUM: {
         UNREACHABLE();
@@ -229,7 +229,7 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
     return e;
 }
 
-bool nex_creator::sum_is_simplified(nex_sum* e) const {
+bool nex_creator::sum_is_simplified(const nex_sum* e) const {
     if (e->size() < 2) return false;
     for (nex * ee : e->children()) {
         if (ee->is_sum())
@@ -470,4 +470,20 @@ nex * nex_creator::mk_div(const nex* a, const nex* b) {
     return mk_div_by_mul(a, to_mul(b));
 }
 
+nex* nex_creator::simplify(nex* e) {
+    if (e->is_mul())
+        return simplify_mul(to_mul(e));
+    if (e->is_sum())
+        return simplify_sum(to_sum(e));
+    return e;
+}
+
+bool nex_creator::is_simplified(const nex *e) const 
+{
+    if (e->is_mul())
+        return mul_is_simplified(to_mul(e));
+    if (e->is_sum())
+        return sum_is_simplified(to_sum(e));
+    return true;
+}
 }
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 61d6d617f..adca07e4b 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -60,17 +60,11 @@ public:
     svector<var_weight>& active_vars_weights() { return m_active_vars_weights;}
     const svector<var_weight>& active_vars_weights() const { return m_active_vars_weights;}
 
-    nex* simplify(nex* e) {
-        NOT_IMPLEMENTED_YET();
-    }
+    nex* simplify(nex* e);
 
     rational extract_coeff_from_mul(const nex_mul* m);
     rational extract_coeff(const nex*);
     
-    bool is_simplified(const nex *e) {
-        NOT_IMPLEMENTED_YET();
-    }
-    
     bool less_than(lpvar j, lpvar k) const{
         unsigned wj = (unsigned)m_active_vars_weights[j];
         unsigned wk = (unsigned)m_active_vars_weights[k];
@@ -210,11 +204,12 @@ public:
     
     nex * simplify_mul(nex_mul *e);    
     bool is_sorted(const nex_mul * e) const;    
-    bool mul_is_simplified(const nex_mul*e ) const;
 
     nex* simplify_sum(nex_sum *e);    
 
-    bool sum_is_simplified(nex_sum* 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);
     
@@ -230,7 +225,7 @@ public:
 
     bool sum_simplify_lt(const nex* a, const nex* b);
     
-    bool mul_simplify_lt(const nex_mul* a, const nex_mul* b);
+    bool less_than_on_mul(const nex_mul* a, const nex_mul* b);
     void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
 };
 }
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index cf31713b7..7faaa8da5 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -86,6 +86,9 @@ void test_simplify() {
     enable_trace("nla_cn");
     enable_trace("nla_cn_details");
     nex_creator & r = cn.get_nex_creator();
+    r.active_vars_weights().resize(3);
+    for (unsigned j = 0; j < r.active_vars_weights().size(); j++)
+        r.active_vars_weights()[j] = static_cast<var_weight>(5 - j);
     nex_var* a = r.mk_var(0);
     nex_var* b = r.mk_var(1);
     nex_var* c = r.mk_var(2);