diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 355edbc79..3d021cc3a 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -63,6 +63,8 @@ public:
         m_e = e;
 #ifdef Z3DEBUG
         m_e_clone = m_nex_creator.clone(m_e);
+        TRACE("nla_cn", tout << "m_e_clone = " <<  * m_e_clone << "\n";);
+        
 #endif
         vector<nex**> front;
         explore_expr_on_front_elem(&m_e, front);
@@ -254,7 +256,7 @@ public:
                 TRACE("nla_cn", tout << "got the cn form: =" << *m_e << "\n";);
                 m_done = m_call_on_result(m_e) || ++m_reported > 100;
  #ifdef Z3DEBUG
-                TRACE("nla_cn", tout << "m_e_clone" << *m_e_clone << "\n";);
+                TRACE("nla_cn", tout << "m_e_clone " << *m_e_clone << "\n";);
                 SASSERT(nex_creator::equal(m_e, m_e_clone));
  #endif
             } else {
@@ -280,7 +282,11 @@ public:
             return;
         TRACE("nla_cn", tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
         if (front.empty()) {
+            TRACE("nla_cn", tout << "got the cn form: =" << *m_e <<  ", clone = " << *m_e_clone << "\n";);
             m_done = m_call_on_result(m_e) || ++m_reported > 100;
+#ifdef Z3DEBUG
+            SASSERT(nex_creator::equal(m_e, m_e_clone));
+#endif
             return;
         }
         auto n = pop_front(front);
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 06019990e..16b37d10b 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -71,16 +71,16 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
 
 
 bool horner::check_cross_nested_expr(const nex* n) {
-    TRACE("nla_horner", tout << "cross-nested n = " << *n << "\n";);
+    TRACE("nla_horner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
     c().lp_settings().stats().m_cross_nested_forms++;
 
-    auto i = interval_of_expr(n);
+    auto i = interval_of_expr(n, 1);
     TRACE("nla_horner", tout << "callback n = " << *n << "\ni="; m_intervals.display(tout, i) << "\n";);
     if (!m_intervals.separated_from_zero(i)) {
         m_intervals.reset();
         return false;
     }
-    auto id = interval_of_expr_with_deps(n);
+    auto id = interval_of_expr_with_deps(n, 1);
     TRACE("nla_horner", tout << "conflict: id = "; m_intervals.display(tout, id ) << *n << "\n";);
     m_intervals.check_interval_for_conflict_on_zero(id);
     m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
@@ -144,18 +144,32 @@ void horner::set_interval_for_scalar(interv& a, const rational& v) {
     m_intervals.set_upper_is_inf(a, false);
 }
 
-interv horner::interval_of_expr_with_deps(const nex* e) {
+interv horner::interval_of_expr_with_deps(const nex* e, unsigned power) {
     interv a;
     switch (e->type()) {
     case expr_type::SCALAR:
         set_interval_for_scalar(a, to_scalar(e)->value());
+        if (power != 1)
+            NOT_IMPLEMENTED_YET();
         return a;
     case expr_type::SUM:
-        return interval_of_sum_with_deps(to_sum(e));
+        {
+        interv b = interval_of_sum_with_deps(to_sum(e));
+        if (power != 1)
+            NOT_IMPLEMENTED_YET();
+        return b;
+        }
     case expr_type::MUL:
-        return interval_of_mul_with_deps(to_mul(e));
-    case expr_type::VAR:
+        {
+        interv b = interval_of_mul_with_deps(to_mul(e));
+        if (power != 1)
+            NOT_IMPLEMENTED_YET();
+        return b;        
+    }
+    case expr_type::VAR: 
         set_var_interval_with_deps(to_var(e)->var(), a);
+        if (power != 1)
+            NOT_IMPLEMENTED_YET();
         return a;
     default:
         TRACE("nla_horner_details", tout << e->type() << "\n";);
@@ -164,43 +178,60 @@ interv horner::interval_of_expr_with_deps(const nex* e) {
     }
 }
 
-interv horner::interval_of_expr(const nex* e) {
+interv horner::interval_of_expr(const nex* e, unsigned power) {
+    TRACE("nla_horner_details", tout << "e = " << *e << "\n";);
     interv a;
     switch (e->type()) {
     case expr_type::SCALAR:
         set_interval_for_scalar(a, to_scalar(e)->value());
-        return a;
+        break;
     case expr_type::SUM:
-        return interval_of_sum(to_sum(e));
+        {
+            interv b = interval_of_sum(to_sum(e));
+            if (power != 1) {
+                NOT_IMPLEMENTED_YET();
+            }
+            return b;
+        }
     case expr_type::MUL:
-        return interval_of_mul(to_mul(e));
+        {
+        interv b  = interval_of_mul(to_mul(e));
+         if (power != 1) {
+                NOT_IMPLEMENTED_YET();
+         }
+         return b;
+    }
     case expr_type::VAR:
         set_var_interval(to_var(e)->var(), a);
-        return a;
+        break;
     default:
         TRACE("nla_horner_details", tout << e->type() << "\n";);
         SASSERT(false);
         return interv();
     }
+    if (power != 1) {
+        NOT_IMPLEMENTED_YET();
+    }
+    return a;
 }
 
 
 interv horner::interval_of_mul_with_deps(const nex_mul* e) {
     const nex * zero_interval_child = get_zero_interval_child(e);
     if (zero_interval_child) {
-        interv a = interval_of_expr_with_deps(zero_interval_child);
+        interv a = interval_of_expr_with_deps(zero_interval_child, 1);
         m_intervals.set_zero_interval_deps_for_mult(a);
         TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); );
         return a;   
     } 
         
     SASSERT(e->is_mul());
-    auto & es = to_mul(e)->children();
-    interv a = interval_of_expr_with_deps(es[0].e());
-    TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
-    for (unsigned k = 1; k < es.size(); k++) {
-        interv b = interval_of_expr_with_deps(es[k].e());
-        TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
+    interv a;
+    set_interval_for_scalar(a, e->coeff());
+    TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); );
+    for (const auto & ep : *e) {
+        interv b = interval_of_expr_with_deps(ep.e(), ep.pow());
+        TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); );
         interv c;
         interval_deps_combine_rule comb_rule;
         m_intervals.mul(a, b, c, comb_rule);
@@ -217,21 +248,22 @@ interv horner::interval_of_mul_with_deps(const nex_mul* e) {
 }
 
 interv horner::interval_of_mul(const nex_mul* e) {
+    TRACE("nla_horner_details", tout << "e = " << *e <<  "\n";);
     const nex * zero_interval_child = get_zero_interval_child(e);
     if (zero_interval_child) {
-        interv a = interval_of_expr(zero_interval_child);
+        interv a = interval_of_expr(zero_interval_child, 1);
         m_intervals.set_zero_interval_deps_for_mult(a);
         TRACE("nla_horner_details", tout << "zero_interval_child = "<< *zero_interval_child << std::endl << "a = "; m_intervals.display(tout, a); );
         return a;   
     } 
         
-    SASSERT(e->is_mul());
-    auto & es = to_mul(e)->children();
-    interv a = interval_of_expr(es[0].e());
-    TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
-    for (unsigned k = 1; k < es.size(); k++) {
-        interv b = interval_of_expr(es[k].e());
-        TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
+    interv a;
+    
+    set_interval_for_scalar(a, e->coeff());
+    TRACE("nla_horner_details", tout << "a = "; m_intervals.display(tout, a); );
+    for (const auto & ep : *e) {
+        interv b = interval_of_expr(ep.e(), ep.pow() );
+        TRACE("nla_horner_details", tout << "ep = " << ep << ", "; m_intervals.display(tout, b); );
         interv c;
         interval_deps_combine_rule comb_rule;
         m_intervals.mul(a, b, c, comb_rule);
@@ -248,38 +280,20 @@ interv horner::interval_of_mul(const nex_mul* e) {
 }
 
 
-void horner::add_mul_to_vector(const nex_mul* e, vector<std::pair<rational, lpvar>> &v) {
+void horner::add_mul_of_degree_one_to_vector(const nex_mul* e, vector<std::pair<rational, lpvar>> &v) {
     TRACE("nla_horner_details", tout << *e << "\n";);
-    SASSERT(e->size() > 0);
-    if (e->size() == 1) {
-        add_linear_to_vector(e->children().begin()->e(), v);
-        return;
-    }
-    rational r;
-    lpvar j = -1;
-    for (const auto & p: e->children()) {
-        const nex * c = p.e();
-        switch (c->type()) {
-        case expr_type::SCALAR:
-            r = to_scalar(c)->value();
-            break;
-        case expr_type::VAR:
-            j = to_var(c)->var();
-            break;
-        default:
-            TRACE("nla_horner_details", tout << e->type() << "\n";);
-            SASSERT(false);
-        }
-    }
-    SASSERT((j + 1) && !(r.is_zero() || r.is_one()));
-    v.push_back(std::make_pair(r, j));
+    SASSERT(e->size() == 1);
+    SASSERT((*e)[0].pow() == 1);
+    const nex *ev = (*e)[0].e();
+    lpvar j = to_var(ev)->var();
+    v.push_back(std::make_pair(e->coeff(), j));
 }
 
 void horner::add_linear_to_vector(const nex* e, vector<std::pair<rational, lpvar>> &v) {
     TRACE("nla_horner_details", tout << *e << "\n";);
     switch (e->type()) {
     case expr_type::MUL:
-        add_mul_to_vector(to_mul(e), v);
+        add_mul_of_degree_one_to_vector(to_mul(e), v);
         break; 
     case expr_type::VAR:
         v.push_back(std::make_pair(rational(1), to_var(e)->var()));
@@ -402,10 +416,10 @@ interv horner::interval_of_sum_no_term_with_deps(const nex_sum* e) {
         return interv();
     }
     auto & es = e->children(); 
-    interv a = interval_of_expr_with_deps(es[0]);
+    interv a = interval_of_expr_with_deps(es[0], 1);
     for (unsigned k = 1; k < es.size(); k++) {
         TRACE("nla_horner_details_sum", tout <<  "es[" << k << "]= " << *es[k] << "\n";);
-        interv b = interval_of_expr_with_deps(es[k]);
+        interv b = interval_of_expr_with_deps(es[k], 1);
         interv c;
         interval_deps_combine_rule combine_rule;
         TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
@@ -426,10 +440,10 @@ interv horner::interval_of_sum_no_term(const nex_sum* e) {
         return interv();
     }
     auto & es = e->children(); 
-    interv a = interval_of_expr(es[0]);
+    interv a = interval_of_expr(es[0], 1);
     for (unsigned k = 1; k < es.size(); k++) {
         TRACE("nla_horner_details_sum", tout <<  "es[" << k << "]= " << *es[k] << "\n";);
-        interv b = interval_of_expr(es[k]);
+        interv b = interval_of_expr(es[k], 1);
         interv c;
         interval_deps_combine_rule combine_rule;
         TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index d636cdfaa..167ae82db 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -39,8 +39,8 @@ public:
     template <typename T> // T has an iterator of (coeff(), var())
     bool lemmas_on_row(const T&);
     template <typename T>  bool row_is_interesting(const T&) const;
-    intervals::interval interval_of_expr_with_deps(const nex* e);
-    intervals::interval interval_of_expr(const nex* e);
+    intervals::interval interval_of_expr_with_deps(const nex* e, unsigned power);
+    intervals::interval interval_of_expr(const nex* e, unsigned power);
     intervals::interval interval_of_sum(const nex_sum*);
     intervals::interval interval_of_sum_no_term(const nex_sum*);
     intervals::interval interval_of_mul(const nex_mul*);
@@ -60,7 +60,7 @@ public:
     lpvar find_term_column(const lp::lar_term &, rational & a) const;
     static lp::lar_term expression_to_normalized_term(const nex_sum*, rational& a, rational & b);
     static void add_linear_to_vector(const nex*, vector<std::pair<rational, lpvar>> &);
-    static void add_mul_to_vector(const nex_mul*, vector<std::pair<rational, lpvar>> &);
+    static void add_mul_of_degree_one_to_vector(const nex_mul*, vector<std::pair<rational, lpvar>> &);
     bool interval_from_term_with_deps(const nex* e, interv&) const;
     const nex* get_zero_interval_child(const nex_mul*) const;
     const nex* get_inf_interval_child(const nex_sum*) const;
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 2e25f570a..16d4e3768 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -266,6 +266,8 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
 
 bool nex_creator::lt(const nex* a, const nex* b) const {
     TRACE("nla_cn_details_", tout << *a << " ? " << *b <<  "\n";);
+    if (a == b)
+        return false;
     bool ret;
     switch (a->type()) {
     case expr_type::VAR: