diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 64c4e67b1..835f563bc 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -160,8 +160,11 @@ public:
             explore_expr_on_front_elem_occs(c, front, occurences);
         }
     }
-    static char ch(unsigned j) {
-        return (char)('a'+j);
+    static std::string ch(unsigned j) {
+        std::stringstream s;
+        s << "v" << j;
+        return s.str();
+        //        return (char)('a'+j);
     }
     // e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form
     void explore_of_expr_on_sum_and_var(nex* c, lpvar j, vector<nex*> front) {
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index 0e7d287c0..52b8c82a1 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -296,11 +296,15 @@ public:
         return r;
     }
 
+    friend nla_expr operator-(const nla_expr& a, const nla_expr&b) {
+        return a + scalar(T(-1))*b;
+    }
     
     nla_expr& operator/=(const nla_expr& b) {
-        TRACE("nla_cn_details", tout << *this <<", " << b << "\n";);
+        TRACE("nla_cn_details", tout << *this <<" / " << b << "\n";);
         if (b.is_var()) {
             *this = (*this) / b.var();
+            TRACE("nla_cn_details", tout << *this << "\n";);
             return *this;
         }
         SASSERT(b.is_mul());
@@ -308,10 +312,12 @@ public:
             for (auto & e : children()) {
                 e /= b;
             }
+            TRACE("nla_cn_details", tout << *this << "\n";);
             return *this;
         }
         if (is_var() || children().size() == 1) {
             *this = scalar(T(1));
+            TRACE("nla_cn_details", tout << *this << "\n";);
             return *this;
         }
         SASSERT(is_mul());
@@ -319,8 +325,16 @@ public:
         unsigned i = 0, k = 0;
         for (; i < children().size(); i++, k++) {
             auto & e = children()[i];
+            TRACE("nla_cn_details", tout << "e=" << e << ",i=" <<i<< ",k=" << k<< "\n";);
+            
             if (!e.is_var()) {
+                SASSERT(e.is_scalar());
+                if (i != k)
+                    children()[k] = children()[i];
+                
+                TRACE("nla_cn_details", tout << "continue\n";);
                 continue;
+
             }
             lpvar j = e.var();
             auto it = powers.find(j);
@@ -332,7 +346,9 @@ public:
                 if (it->second == 0)
                     powers.erase(it);
                 k--;
-            }            
+            }
+            TRACE("nla_cn_details", tout << *this << "\n";);
+            
         }
         SASSERT(powers.size() == 0);
         while(k ++ < i)
@@ -340,6 +356,7 @@ public:
 
         if (children().size() == 0)
             *this = scalar(T(1));
+        TRACE("nla_cn_details", tout << *this << "\n";);
         
         return *this;
     }
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index d523faa1c..25cdd75c3 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -79,13 +79,14 @@ void test_cn_on_expr(horner::nex t) {
 void test_cn() {
     typedef horner::nex nex;
     enable_trace("nla_cn");
-    //  enable_trace("nla_cn_details");
-    nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
+    enable_trace("nla_cn_details");
+    nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4), f = nex::var(5), g = nex::var(6);
     nex min_1 = nex::scalar(rational(-1));
-    test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
+    // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
     TRACE("nla_cn", tout << "done\n";);
    
-    test_cn_on_expr(a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d);
+    test_cn_on_expr(b*c*d -  b*c*g);
+    //    test_cn_on_expr(a*a*d + a*b*c*d + a*a*c*c*d + a*d*d + e*a*e + e*a*c + e*d);
     // 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 b24965b89..3e3eb4600 100644
--- a/src/test/lp/nla_solver_test.cpp
+++ b/src/test/lp/nla_solver_test.cpp
@@ -412,7 +412,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
 
 void test_horner() {
     enable_trace("nla_solver");
-    lp::lar_solver s;
+    /*    lp::lar_solver s;
     unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
         ce = 5, bd = 6, ab = 7, ac = 8, c_min_b = 9;
     
@@ -451,7 +451,7 @@ void test_horner() {
     nla.add_monomial(lp_ac, v.size(), v.begin());
     v.clear();
 
-    
+    */
 
 
 }