diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index e77053168..c4199fa49 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -42,43 +42,49 @@ void horner::lemmas_on_expr(nex& e) {
     vector<nex*> front;
     front.push_back(&e);
     cross_nested_of_expr(e, front);
-
 }
 
-void horner::cross_nested_of_expr(nex& e, vector<nex*> & front) {
+void horner::cross_nested_of_expr(nex& e, vector<nex*> front) {
     TRACE("nla_cn", tout << "e = " << e << ", front has " << front.size() << "\n";);
-    if (front.empty()) {
+    while (!front.empty()) {
+        nex& c = *front.back();
+        front.pop_back();
+        cross_nested_of_expr_on_front_elem(e, c, front);        
+    }
+    TRACE("nla_cn", tout << "empty front: e=" << "\n";);
+     
+}
+
+void horner::cross_nested_of_expr_on_front_elem(nex& e, nex& c, vector<nex*> front) {
+    TRACE("nla_cn", tout << "e=" << e << "\nc=" << c << "\n";);
+    SASSERT(c.is_sum());
+    auto occurences = get_mult_occurences(c);
+    if (occurences.empty() && front.empty()) {
+        TRACE("nla_cn", tout << "empty front: e=" << e << "\n";);        
         auto i = interval_of_expr(e);
         m_intervals.check_interval_for_conflict_on_zero(i);
-    }
-    nex & c = *(front.back());
-    front.pop_back();
-    TRACE("nla_cn", tout << "pop from front\n";);
-    cross_nested_of_expr_on_front_elem(e, c, front);    
-}
-
-void horner::cross_nested_of_expr_on_front_elem(nex& e, nex& c, vector<nex*> & front) {
-    SASSERT(c.is_sum());
-    std::unordered_map<unsigned, lpvar> occurences;
-    TRACE("nla_cn", tout << "c = " << c << "\n";);
-    get_occurences_map(c, occurences);
-    nex copy_of_c(c);
-    for(const auto & p : occurences) {
-        TRACE("nla_cn", tout << "v" << p.first << ", " << p.second << "\n";);
-        if (p.second < 2)
-            continue;
-        cross_nested_of_expr_on_sum_and_var(e, c, p.first, front);
-        c = copy_of_c;
+    } else {
+        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 << "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 << "\n";);
+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 << "\n";);
     split_with_var(c, j, front);
-    cross_nested_of_expr(e, front);
+    TRACE("nla_cn", tout << "after split c=" << c << "\n";);    
+    do {
+        nex& c = *front.back();
+        front.pop_back();
+        cross_nested_of_expr_on_front_elem(e, c, front);
+    } while (!front.empty());
 }
 
+
 template <typename T> 
 void horner::lemmas_on_row(const T& row) {
     if (!row_is_interesting(row))
@@ -137,7 +143,8 @@ void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::
 
 
 // j -> the number of expressions j appears in as a multiplier
-void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<lpvar, unsigned>& occurences) const {
+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;
@@ -159,12 +166,18 @@ void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<
             SASSERT(false);
         }
     }
-    TRACE("nla_cn_details",
+    TRACE("nla_cn",
           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;
 }
 
 void horner::split_with_var(nex& e, lpvar j, vector<nex*> & front) {
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index da8b0b7bb..58bb517e4 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -42,8 +42,7 @@ public:
     
     nex nexvar(lpvar j) const;
     nex cross_nested_of_sum(const nex&, lpvar);    
-    void get_occurences_map(const nex& e,
-                            std::unordered_map<unsigned, lpvar>& ) const;
+    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>&);
@@ -51,8 +50,8 @@ public:
     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(nex& , vector<nex*>& front);
-    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);
+    void cross_nested_of_expr(nex& , vector<nex*> front);
+    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);
 }; // end of horner
 }
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index b0fb6a51e..38daa93ac 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -104,6 +104,7 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) {
      svector<lp::constraint_index> expl;
      m_dep_manager.linearize(i.m_lower_dep, expl); 
      _().current_expl().add_expl(expl);
+     TRACE("nla_cn", print_lemma(tout););
      return true;
 }