diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 51ca8e7f7..88f53db40 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -21,8 +21,9 @@
 #include "math/lp/horner.h"
 #include "math/lp/nla_core.h"
 #include "math/lp/lp_utils.h"
+#include "math/lp/cross_nested.h"
+
 namespace nla {
-typedef nla_expr<rational> nex;
 typedef intervals::interval interv;
 horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {}
 
@@ -50,44 +51,6 @@ nex* pop_back(vector<nex*>& front) {
     return c;
 }
 
-void horner::cross_nested_of_expr_on_front_elem(nex& e, nex* c, vector<nex*>& front) {
-    SASSERT(c->is_sum());
-    vector<lpvar> occurences = get_mult_occurences(*c);
-    TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\noccurences="; print_vector(occurences, tout) << "\nfront:"; print_vector_of_ptrs(front, tout) << "\n";);
-    
-    if (occurences.empty()) {
-        if(front.empty()) {
-            TRACE("nla_cn_cn", tout << "got the cn form: e=" << e << "\n";);
-            SASSERT(!can_be_cross_nested_more(e));
-            auto i = interval_of_expr(e);
-            m_intervals.check_interval_for_conflict_on_zero(i);
-        } else {
-            nex* c = pop_back(front);
-            cross_nested_of_expr_on_front_elem(e, c, front);     
-        }
-    } else {
-        TRACE("nla_cn", tout << "save c=" << *c << "front:"; print_vector_of_ptrs(front, tout) << "\n";);           
-        nex copy_of_c = *c;
-        for(lpvar j : occurences) {
-            cross_nested_of_expr_on_sum_and_var(e, c, j, front);
-            *c = copy_of_c;
-            TRACE("nla_cn", tout << "restore c=" << *c << ", e=" << e << "\n";);   
-        }
-    }
-    TRACE("nla_cn", tout << "exit\n";);
-}
-// e is the global expression, c is the sub expressiond which is going to changed from sum to the cross nested form
-void horner::cross_nested_of_expr_on_sum_and_var(nex& e, nex* c, lpvar j, vector<nex*>& front) {
-    TRACE("nla_cn", tout << "e=" << e << "\nc=" << *c << "\nj = v" << j << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
-    split_with_var(*c, j, front);
-    TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);    
-    do {
-        nex* n = pop_back(front);
-        cross_nested_of_expr_on_front_elem(e, n, front);
-    } while (!front.empty());
-}
-
-
 template <typename T> 
 void horner::lemmas_on_row(const T& row) {
     if (!row_is_interesting(row))
@@ -120,151 +83,6 @@ nex horner::nexvar(lpvar j) const {
     return e;
 }
 
-void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
-    if (seen.find(j) != seen.end()) return;
-    seen.insert(j);
-    auto it = occurences.find(j);
-    if (it == occurences.end())
-        occurences[j] = 1;
-    else
-        it->second ++;
-}
-
-void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
-    SASSERT(e.type() == expr_type::MUL);
-    for (const auto & ce : e.children()) {
-         if (ce.type() ==  expr_type::VAR) {
-            process_var_occurences(ce.var(), seen, occurences);
-        } else if (ce.type() ==  expr_type::MUL){
-            process_mul_occurences(ce, seen, occurences);
-        } 
-    }
-}
-
-
-// j -> the number of expressions j appears in as a multiplier
-vector<lpvar> horner::get_mult_occurences(const nex& e) const {
-    std::unordered_map<lpvar, unsigned> occurences;
-    SASSERT(e.type() == expr_type::SUM);
-    for (const auto & ce : e.children()) {
-        std::unordered_set<lpvar> seen;
-        if (ce.type() == expr_type::MUL) {
-            for (const auto & cce : ce.children()) {
-                if (cce.type() ==  expr_type::VAR) {
-                    process_var_occurences(cce.var(), seen, occurences);
-                } else if (cce.type() == expr_type::MUL) {
-                    process_mul_occurences(cce, seen, occurences);
-                } else {
-                    continue;
-                }
-            }
-        } else if (ce.type() ==  expr_type::VAR) {
-            process_var_occurences(ce.var(), seen, occurences);
-        }
-    }
-    TRACE("nla_cn_details",
-          tout << "{";
-          for(auto p: occurences) {
-              tout << "(v" << p.first << "->" << p.second << ")";
-          }
-          tout << "}" << std::endl;);    
-    vector<lpvar> r;
-    for(auto p: occurences) {
-        if (p.second > 1)
-            r.push_back(p.first);
-    }
-    return r;
-}
-bool horner::can_be_cross_nested_more(const nex& e) const {
-    switch (e.type()) {
-    case expr_type::SCALAR:
-        return false;
-    case expr_type::SUM: {
-        return !get_mult_occurences(e).empty();
-    }
-    case expr_type::MUL:
-        {
-            for (const auto & c: e.children()) {
-                if (can_be_cross_nested_more(c))
-                    return true;
-            }
-            return false;
-        }
-    case expr_type::VAR:
-        return false;
-    default:
-        TRACE("nla_cn_details", tout << e.type() << "\n";);
-        SASSERT(false);
-        return false;
-    }
-}
-void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
-    TRACE("nla_cn_details", tout << "e = " << e << ", j = v" << j << "\n";);
-    if (!e.is_sum())
-        return;
-    nex a, b;
-    for (const nex & ce: e.children()) {
-        if ((ce.is_mul() && ce.contains(j)) || (ce.is_var() && ce.var() == j)) {
-            a.add_child(ce / j);
-        } else {
-            b.add_child(ce);
-        }        
-    }
-    a.type() = expr_type::SUM;
-    TRACE("nla_cn_details", tout << "a = " << a << "\n";);
-    SASSERT(a.children().size() >= 2);
-    
-    if (b.children().size() == 1) {
-        nex t = b.children()[0];
-        b = t;      
-    } else if (b.children().size() > 1) {
-        b.type() = expr_type::SUM;        
-    }
-
-    if (b.is_undef()) {
-        SASSERT(b.children().size() == 0);
-        e = nex(expr_type::MUL);        
-        e.add_child(nex::var(j));
-        e.add_child(a);
-        if (a.size() > 1) {
-            front.push_back(&e.children().back());
-            TRACE("nla_cn_details", tout << "push to front " << e.children().back() << "\n";);
-        }
-      
-    } else {
-        TRACE("nla_cn_details", tout << "b = " << b << "\n";);
-        e = nex::sum(nex::mul(nex::var(j), a), b);
-        if (a.is_sum()) {
-            front.push_back(&(e.children()[0].children()[1]));
-            TRACE("nla_cn_details", tout << "push to front " << e.children()[0].children()[1] << "\n";);
-        }
-        if (b.is_sum()) {
-            front.push_back(&(e.children()[1]));
-            TRACE("nla_cn_details", tout << "push to front " << e.children()[1] << "\n";);
-        }
-    }
-}
-
-nex horner::cross_nested_of_sum(const nex& e, lpvar j) {
-    if (!e.is_sum())
-        return e;
-    /*
-    std::unordered_map<lpvar, unsigned>  occurences;
-    get_occurences_map(e, occurences);
-    lpvar j = random_most_occured_var(occurences);
-    if (j + 1 == 0) return e;
-    TRACE("nla_cn_details",
-          tout << "e = "  << e << "\noccurences ";
-          for (auto p : occurences){
-              tout << "(v"<<p.first << ", "<< p.second<<")";
-          }
-          tout << std::endl << "most occured = v" << j << std::endl;);
-    nex ret = split_with_var(e, j);
-    TRACE("nla_cn_details", tout << "ret =" << ret << "\n";);
-    return ret;*/
-    SASSERT(false);
-    return nex();
-}
 
 template <typename T> nex horner::create_sum_from_row(const T& row) {
     TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
@@ -276,29 +94,6 @@ template <typename T> nex horner::create_sum_from_row(const T& row) {
     return e;
 }
 
-std::set<lpvar> horner::get_vars_of_expr(const nex &e ) const {
-    std::set<lpvar> r;
-    switch (e.type()) {
-    case expr_type::SCALAR:
-        return r;
-    case expr_type::SUM:
-    case expr_type::MUL:
-        {
-            for (const auto & c: e.children())
-                for ( lpvar j : get_vars_of_expr(c))
-                    r.insert(j);
-        }
-        return r;
-    case expr_type::VAR:
-        r.insert(e.var());
-        return r;
-    default:
-        TRACE("nla_cn_details", tout << e.type() << "\n";);
-        SASSERT(false);
-        return r;
-    }
-
-}
 
 void horner::set_interval_for_scalar(interv& a, const rational& v) {
     m_intervals.set_lower(a, v);
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index ef0ead28d..0a1e1eb77 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -41,17 +41,10 @@ public:
     intervals::interval interval_of_expr(const nex& e);
     
     nex nexvar(lpvar j) const;
-    nex cross_nested_of_sum(const nex&, lpvar);    
-    vector<lpvar> get_mult_occurences(const nex& e) const;
-    void split_with_var(nex &, lpvar, vector<nex*> & front);
-    void set_var_interval(lpvar j, intervals::interval&);
     intervals::interval interval_of_sum(const vector<nex>&);
     intervals::interval interval_of_mul(const vector<nex>&);
     void set_interval_for_scalar(intervals::interval&, const rational&);
     std::set<lpvar> get_vars_of_expr(const nex &) const;
     void lemmas_on_expr(nex &);
-    void cross_nested_of_expr_on_front_elem(nex& , nex*, vector<nex*>& front);
-    void cross_nested_of_expr_on_sum_and_var(nex& , nex*, lpvar, vector<nex*>& front);    
-    bool can_be_cross_nested_more(const nex&) const;
 }; // end of horner
 }
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index 2724e6276..f0d46c99e 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -119,7 +119,7 @@ public:
         case expr_type::MUL:
             return print_mul(out);
         case expr_type::VAR:
-            out << "v" << m_j;
+            out << static_cast<char>('a'+m_j);
             return out;
         case expr_type::SCALAR:
             out << m_v;
@@ -223,6 +223,51 @@ public:
         return false;
     }    
 };
+template <typename T> 
+nla_expr<T> operator+(const nla_expr<T>& a, const nla_expr<T>& b) {
+    if (a.is_sum()) {
+        nla_expr<T> r(expr_type::SUM);
+        r.children() = a.children();
+        if (b.is_sum()) {
+            for (auto& e: b.children())
+                r.add_child(e);
+        } else {
+            r.add_child(b);
+        }
+        return r;
+    }
+    if (b.is_sum()) {
+        nla_expr<T> r(expr_type::SUM);
+        r.children() = b.children();
+        r.add_child(a);
+        return r;
+    }
+    return nla_expr<T>::sum(a, b);
+}
+
+template <typename T> 
+nla_expr<T> operator*(const nla_expr<T>& a, const nla_expr<T>& b) {
+    if (a.is_mul()) {
+        nla_expr<T> r(expr_type::MUL);
+        r.children() = a.children();
+        if (b.is_mul()) {
+            for (auto& e: b.children())
+                r.add_child(e);
+        } else {
+            r.add_child(b);
+        }
+        return r;
+    }
+    if (b.is_mul()) {
+        nla_expr<T> r(expr_type::MUL);
+        r.children() = b.children();
+        r.add_child(a);
+        return r;
+    }
+    return nla_expr<T>::mul(a, b);
+}
+
+
 template <typename T> 
 nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
     SASSERT((a.is_mul() && a.contains(j)) || (a.is_var() && a.var() == j));
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 12b02ae3f..07a997351 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -69,11 +69,10 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
 void test_cn() {
     typedef horner::nex nex;
     enable_trace("nla_cn");
-
+    // (a(a+(b+c)c+d)d + e(a(e+c)+d)
     nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
-    nex aad = nex::mul(a, a, d);
-    
-    
+    nex t = a*a*d + a*b*c*d + a*c*c*d + e*a*e + e*a*c + e*d;
+    TRACE("nla_cn", tout << "t=" << t << '\n';);
 }
 
 }