diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index ff38b217f..5d1a9dcce 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -87,7 +87,10 @@ bool horner::lemmas_on_row(const T& row) {
         [this, dep](const nex* n) { return m_intervals->check_nex(n, dep); },
         [this](unsigned j)   { return c().var_is_fixed(j); },
         [this]() { return c().random(); }, m_nex_creator);
-    return lemmas_on_expr(cn, to_sum(e));
+    bool ret = lemmas_on_expr(cn, to_sum(e));
+    c().m_intervals.get_dep_intervals().reset(); // clean the memory allocated by the interval bound dependencies
+    return ret;
+
 }
 
 bool horner::horner_lemmas() {
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 71f3e1b37..8e38a34ad 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -138,13 +138,6 @@ bool nex_creator::gt_on_powers_mul_same_degree(const T& a, const nex_mul& b) con
     return ret;
 }
 
-bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
-    for (auto c : children) 
-        if (!is_simplified(*c.e()) || c.pow() == 0)
-            return false;
-    return true;
-}
-
 bool nex_creator::gt_on_mul_mul(const nex_mul& a, const nex_mul& b) const {
     TRACE("grobner_d", tout << "a = " << a << " , b = " << b << "\n";);
     SASSERT(is_simplified(a) && is_simplified(b));
@@ -479,14 +472,6 @@ void nex_creator::simplify_children_of_sum(nex_sum& s) {
     sort_join_sum(s);
 }
 
-
-static bool have_no_scalars(const nex_mul& a) {
-    for (auto & p : a)
-        if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
-            return false;
-    return true;
-}
-
 bool nex_mul::all_factors_are_elementary() const {
     for (auto & p : *this)
         if (!p.e()->is_elementary())
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 80fa7158e..4c28fb655 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -279,8 +279,6 @@ public:
     void simplify_children_of_sum(nex_sum & sum);
     
     bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned);
-
-    bool children_are_simplified(const vector<nex_pow>& children) const;
     bool gt(const nex& a, const nex& b) const; 
     bool gt(const nex* a, const nex* b) const { return gt(*a, *b); }
     template <typename T>
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index f524137e6..488a402b8 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -74,7 +74,6 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
     m_core->lp_settings().stats().m_cross_nested_forms++;
     auto i = interval_of_expr<e_with_deps::without_deps>(n, 1);
     if (!m_dep_intervals.separated_from_zero(i)) {
-        m_dep_intervals.reset();
         return false;
     }
     auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
@@ -84,7 +83,6 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
                                                          m_core->current_expl().add(e);
                                                      };
     m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps, f);
-    m_dep_intervals.reset(); // clean the memory allocated by the interval bound dependencies
     return true;
 }