diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 7aa5c9c46..f8b123ada 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -184,7 +184,7 @@ public:
     const ptr_vector<nex>* children_ptr() const { return &m_children;}
     ptr_vector<nex>* children_ptr() { return &m_children;}
     // A monomial is 'pure' if does not have a numeric coefficient.
-    bool is_pure_monomial() { return size() == 0 || (!m_children[0]->is_scalar()); }    
+    bool is_pure_monomial() const { return size() == 0 || (!m_children[0]->is_scalar()); }    
     std::ostream & print(std::ostream& out) const {
         bool first = true;
         for (const nex* v : m_children) {            
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 13d37fb8a..3f052d548 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -84,33 +84,33 @@ void test_cn() {
         );
     enable_trace("nla_cn");
     enable_trace("nla_cn_details");
-    nex_var* a = cn.mk_var(0);
-    nex_var* b = cn.mk_var(1);
-    nex_var* c = cn.mk_var(2);
-    nex_var* d = cn.mk_var(3);
-    nex_var* e = cn.mk_var(4);
-    nex_var* g = cn.mk_var(6);
-    nex* min_1 = cn.mk_scalar(rational(-1));
+    nex_var* a = cn.get_nex_creator().mk_var(0);
+    nex_var* b = cn.get_nex_creator().mk_var(1);
+    nex_var* c = cn.get_nex_creator().mk_var(2);
+    nex_var* d = cn.get_nex_creator().mk_var(3);
+    nex_var* e = cn.get_nex_creator().mk_var(4);
+    nex_var* g = cn.get_nex_creator().mk_var(6);
+    nex* min_1 = cn.get_nex_creator().mk_scalar(rational(-1));
     // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
-    nex* bcd = cn.mk_mul(b, c, d);
-    nex_mul* bcg = cn.mk_mul(b, c, g);
+    nex* bcd = cn.get_nex_creator().mk_mul(b, c, d);
+    nex_mul* bcg = cn.get_nex_creator().mk_mul(b, c, g);
     bcg->add_child(min_1);
-    nex_sum* t = cn.mk_sum(bcd, bcg);
+    nex_sum* t = cn.get_nex_creator().mk_sum(bcd, bcg);
     test_cn_on_expr(t, cn);
-    nex* aad = cn.mk_mul(a, a, d);
-    nex* abcd = cn.mk_mul(a, b, c, d);
-    nex* aaccd = cn.mk_mul(a, a, c, c, d);
-    nex* add = cn.mk_mul(a, d, d);
-    nex* eae = cn.mk_mul(e, a, e);
-    nex* eac = cn.mk_mul(e, a, c);
-    nex* ed = cn.mk_mul(e, d);
-    nex* _6aad = cn.mk_mul(cn.mk_scalar(rational(6)), a, a, d);
+    nex* aad = cn.get_nex_creator().mk_mul(a, a, d);
+    nex* abcd = cn.get_nex_creator().mk_mul(a, b, c, d);
+    nex* aaccd = cn.get_nex_creator().mk_mul(a, a, c, c, d);
+    nex* add = cn.get_nex_creator().mk_mul(a, d, d);
+    nex* eae = cn.get_nex_creator().mk_mul(e, a, e);
+    nex* eac = cn.get_nex_creator().mk_mul(e, a, c);
+    nex* ed = cn.get_nex_creator().mk_mul(e, d);
+    nex* _6aad = cn.get_nex_creator().mk_mul(cn.get_nex_creator().mk_scalar(rational(6)), a, a, d);
 #ifdef Z3DEBUG
-    nex * clone = cn.clone(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
+    nex * clone = cn.clone(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
     TRACE("nla_cn", tout << "clone = " << *clone << "\n";);
 #endif
-    //    test_cn_on_expr(cn.mk_sum(aad,  abcd, aaccd, add, eae, eac, ed), cn);
-    test_cn_on_expr(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed), cn);
+    //    test_cn_on_expr(cn.get_nex_creator().mk_sum(aad,  abcd, aaccd, add, eae, eac, ed), cn);
+    test_cn_on_expr(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed), cn);
     // TRACE("nla_cn", tout << "done\n";);
     // test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);
     // TRACE("nla_cn", tout << "done\n";);
diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp
index 3e3eb4600..e2f2f2e27 100644
--- a/src/test/lp/nla_solver_test.cpp
+++ b/src/test/lp/nla_solver_test.cpp
@@ -38,33 +38,33 @@ void create_abcde(solver & nla,
     vec.push_back(lp_d);
     vec.push_back(lp_e);
 
-    nla.add_monomial(lp_abcde, vec.size(), vec.begin());
+    nla.add_monic(lp_abcde, vec.size(), vec.begin());
 
     // create monomial ac
     vec.clear();
     vec.push_back(lp_a);
     vec.push_back(lp_c);
-    nla.add_monomial(lp_ac, vec.size(), vec.begin());
+    nla.add_monic(lp_ac, vec.size(), vec.begin());
 
     // create monomial bde
     vec.clear();
     vec.push_back(lp_b);
     vec.push_back(lp_d);
     vec.push_back(lp_e);
-    nla.add_monomial(lp_bde, vec.size(), vec.begin());
+    nla.add_monic(lp_bde, vec.size(), vec.begin());
 
     // create monomial acd
     vec.clear();
     vec.push_back(lp_a);
     vec.push_back(lp_c);
     vec.push_back(lp_d);
-    nla.add_monomial(lp_acd, vec.size(), vec.begin());
+    nla.add_monic(lp_acd, vec.size(), vec.begin());
 
     // create monomial be
     vec.clear();
     vec.push_back(lp_b);
     vec.push_back(lp_e);
-    nla.add_monomial(lp_be, vec.size(), vec.begin());
+    nla.add_monic(lp_be, vec.size(), vec.begin());
 }
 
 
@@ -88,13 +88,13 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
     params_ref p;
     solver nla(s);
     svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
-    nla.add_monomial(lp_bde, v.size(), v.begin());
+    nla.add_monic(lp_bde, v.size(), v.begin());
     v.clear();
     v.push_back(lp_a);v.push_back(lp_b);v.push_back(lp_c);v.push_back(lp_d);v.push_back(lp_e);
-    nla.add_monomial(lp_abcde, v.size(), v.begin());
+    nla.add_monic(lp_abcde, v.size(), v.begin());
     v.clear();
     v.push_back(lp_a);v.push_back(lp_c);
-    nla.add_monomial(lp_ac, v.size(), v.begin());
+    nla.add_monic(lp_ac, v.size(), v.begin());
      
     vector<lemma> lv;
 
@@ -165,7 +165,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
     params_ref p;
     solver nla(s);
     svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
-    nla.add_monomial(lp_bde, v.size(), v.begin());
+    nla.add_monic(lp_bde, v.size(), v.begin());
 
     vector<lemma> lemma;
 
@@ -301,7 +301,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
     vec.push_back(lp_a);
     vec.push_back(lp_c);
     vec.push_back(lp_d);
-    nla.add_monomial(lp_acd, vec.size(), vec.begin());
+    nla.add_monic(lp_acd, vec.size(), vec.begin());
     
     vector<lemma> lemma;
     s_set_column_value(s, lp_a, rational(1));
@@ -436,19 +436,19 @@ void test_horner() {
     solver nla(s);
     vector<lpvar> v;
     v.push_back(a); v.push_back(b);
-    nla.add_monomial(lp_ab, v.size(), v.begin());
+    nla.add_monic(lp_ab, v.size(), v.begin());
     v.clear();
 
     v.push_back(c); v.push_back(e);
-    nla.add_monomial(lp_ce, v.size(), v.begin());
+    nla.add_monic(lp_ce, v.size(), v.begin());
     v.clear();
 
     v.push_back(b); v.push_back(d);
-    nla.add_monomial(lp_bd, v.size(), v.begin());
+    nla.add_monic(lp_bd, v.size(), v.begin());
     v.clear();
 
     v.push_back(a); v.push_back(c);
-    nla.add_monomial(lp_ac, v.size(), v.begin());
+    nla.add_monic(lp_ac, v.size(), v.begin());
     v.clear();
 
     */
@@ -478,14 +478,14 @@ void test_basic_sign_lemma() {
     vec.push_back(lp_d);
     vec.push_back(lp_e);
 
-    nla.add_monomial(lp_bde, vec.size(), vec.begin());
+    nla.add_monic(lp_bde, vec.size(), vec.begin());
     vec.clear();
 
     vec.push_back(lp_a);
     vec.push_back(lp_c);
     vec.push_back(lp_d);
 
-    nla.add_monomial(lp_acd, vec.size(), vec.begin());
+    nla.add_monic(lp_acd, vec.size(), vec.begin());
 
     // set the values of the factors so it should be bde = -acd according to the model
     
@@ -550,17 +550,17 @@ void test_order_lemma_params(bool var_equiv, int sign) {
     vector<unsigned> vec;
     vec.push_back(lp_a);
     vec.push_back(lp_b);
-    int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
+    int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     // create monomial cd
     vec.clear();
     vec.push_back(lp_c);
     vec.push_back(lp_d);
-    int mon_cd = nla.add_monomial(lp_cd, vec.size(), vec.begin());
+    int mon_cd = nla.add_monic(lp_cd, vec.size(), vec.begin());
     // create monomial ef
     vec.clear();
     vec.push_back(lp_e);
     vec.push_back(lp_f);
-    int mon_ef = nla.add_monomial(lp_ef, vec.size(), vec.begin());
+    int mon_ef = nla.add_monic(lp_ef, vec.size(), vec.begin());
     // create monomial ij
     vec.clear();
     vec.push_back(lp_i);
@@ -568,7 +568,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
         vec.push_back(lp_k);
     else
         vec.push_back(lp_j);
-    int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
+    int mon_ij = nla.add_monic(lp_ij, vec.size(), vec.begin());
 
     if (var_equiv) { // make k equivalent to j
         lp::lar_term t;
@@ -585,7 +585,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
     vec.push_back(lp_a);
     vec.push_back(lp_b);
     vec.push_back(lp_f);
-    nla.add_monomial(lp_abef, vec.size(), vec.begin());
+    nla.add_monic(lp_abef, vec.size(), vec.begin());
 
     //create monomial (cd)(ij)
     vec.clear();
@@ -593,7 +593,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
     vec.push_back(lp_j);
     vec.push_back(lp_c);
     vec.push_back(lp_d);
-    auto mon_cdij = nla.add_monomial(lp_cdij, vec.size(), vec.begin());
+    auto mon_cdij = nla.add_monic(lp_cdij, vec.size(), vec.begin());
 
     // set i == e
     s_set_column_value(s, lp_e, s.get_column_value(lp_i));
@@ -681,22 +681,22 @@ void test_monotone_lemma() {
     vector<unsigned> vec;
     vec.push_back(lp_a);
     vec.push_back(lp_b);
-    int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
+    int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     // create monomial cd
     vec.clear();
     vec.push_back(lp_c);
     vec.push_back(lp_d);
-    int mon_cd = nla.add_monomial(lp_cd, vec.size(), vec.begin());
+    int mon_cd = nla.add_monic(lp_cd, vec.size(), vec.begin());
     // create monomial ef
     vec.clear();
     vec.push_back(lp_e);
     vec.push_back(lp_f);
-    nla.add_monomial(lp_ef, vec.size(), vec.begin());
+    nla.add_monic(lp_ef, vec.size(), vec.begin());
     // create monomial ij
     vec.clear();
     vec.push_back(lp_i);
     vec.push_back(lp_j);
-    int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
+    int mon_ij = nla.add_monic(lp_ij, vec.size(), vec.begin());
 
     // set e == i + 1
     s_set_column_value(s, lp_e, s.get_column_value(lp_i) + lp::impq(rational(1)));
@@ -745,7 +745,7 @@ void test_tangent_lemma_reg() {
     vector<unsigned> vec;
     vec.push_back(lp_a);
     vec.push_back(lp_b);
-    int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
+    int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     
     s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
     vector<lemma> lemma;
@@ -791,7 +791,7 @@ void test_tangent_lemma_equiv() {
     vector<unsigned> vec;
     vec.push_back(lp_a);
     vec.push_back(lp_b);
-    int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
+    int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
     
     s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
     vector<lemma> lemma;