diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp
index fd4379954..f3aa33680 100644
--- a/src/math/interval/dep_intervals.cpp
+++ b/src/math/interval/dep_intervals.cpp
@@ -35,27 +35,6 @@ void dep_intervals::set_interval_for_scalar(interval& a, const rational& v) {
     set_upper_is_inf(a, false);
 }
 
-template <e_with_deps wd>
-void dep_intervals::copy_upper_bound(const interval& a, interval& i) const {
-    SASSERT(a.m_upper_inf == false);
-    i.m_upper_inf = false;
-    m_config.set_upper(i, a.m_upper);
-    i.m_upper_open = a.m_upper_open;
-    if (wd == with_deps) {
-        i.m_upper_dep = a.m_upper_dep;
-    }
-}
-
-template <e_with_deps wd>
-void dep_intervals::copy_lower_bound(const interval& a, interval& i) const {
-    SASSERT(a.m_lower_inf == false);
-    i.m_lower_inf = false;
-    m_config.set_lower(i, a.m_lower);
-    i.m_lower_open = a.m_lower_open;
-    if (wd == with_deps) {
-        i.m_lower_dep = a.m_lower_dep;
-    }
-}
 
 
 
@@ -75,88 +54,6 @@ void dep_intervals::set_zero_interval_deps_for_mult(interval& a) {
     a.m_upper_dep = a.m_lower_dep;
 }
 
-template <e_with_deps wd>
-void dep_intervals::mul(const rational& r, const interval& a, interval& b) const {
-    if (r.is_zero()) return;
-    m_imanager.mul(r.to_mpq(), a, b);
-    if (wd == with_deps) {
-        if (r.is_pos()) {
-            b.m_lower_dep = a.m_lower_dep;
-            b.m_upper_dep = a.m_upper_dep;
-        }
-        else {
-            b.m_upper_dep = a.m_lower_dep;
-            b.m_lower_dep = a.m_upper_dep;
-        }
-    }
-}
-
-template <e_with_deps wd>
-dep_intervals::interval dep_intervals::intersect(const interval& a, const interval& b) const {
-    interval i;
-    update_lower_for_intersection<wd>(a, b, i);
-    update_upper_for_intersection<wd>(a, b, i);
-    return i;
-}
-
-template <e_with_deps wd>
-void dep_intervals::update_lower_for_intersection(const interval& a, const interval& b, interval& i) const {
-    if (a.m_lower_inf) {
-        if (b.m_lower_inf)
-            return;
-        copy_lower_bound<wd>(b, i);
-        return;
-    }
-    if (b.m_lower_inf) {
-        SASSERT(!a.m_lower_inf);
-        copy_lower_bound<wd>(a, i);
-        return;
-    }
-    if (m_num_manager.lt(a.m_lower, b.m_lower)) {
-        copy_lower_bound<wd>(b, i);
-        return;
-    }
-    if (m_num_manager.gt(a.m_lower, b.m_lower)) {
-        copy_lower_bound<wd>(a, i);
-        return;
-    }
-    SASSERT(m_num_manager.eq(a.m_lower, b.m_lower));
-    if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here
-        copy_lower_bound<wd>(a, i);
-        return;
-    }
-    copy_lower_bound<wd>(b, i);
-}
-
-template <e_with_deps wd>
-void dep_intervals::update_upper_for_intersection(const interval& a, const interval& b, interval& i) const {
-    if (a.m_upper_inf) {
-        if (b.m_upper_inf)
-            return;
-        copy_upper_bound<wd>(b, i);
-        return;
-    }
-    if (b.m_upper_inf) {
-        SASSERT(!a.m_upper_inf);
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-    if (m_num_manager.gt(a.m_upper, b.m_upper)) {
-        copy_upper_bound<wd>(b, i);
-        return;
-    }
-    if (m_num_manager.lt(a.m_upper, b.m_upper)) {
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-    SASSERT(m_num_manager.eq(a.m_upper, b.m_upper));
-    if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-
-    copy_upper_bound<wd>(b, i);
-}
 
 
 void dep_intervals::add(const rational& r, interval& a) const {
@@ -168,23 +65,6 @@ void dep_intervals::add(const rational& r, interval& a) const {
     }
 }
 
-template <e_with_deps wd>
-dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) {
-    interval b;
-    if (with_deps == wd) {
-        interval_deps_combine_rule combine_rule;
-        m_imanager.power(a, n, b, combine_rule);
-        combine_deps(a, combine_rule, b);
-    }
-    else {
-        m_imanager.power(a, n, b);
-    }
-    TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = ";
-          display(tout, b) << "\n"; );
-    return b;
-}
-
-
 bool dep_intervals::separated_from_zero_on_lower(const interval& i) const {
     if (lower_is_inf(i))
         return false;
diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index 5a7521b53..9d7c5de20 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -132,6 +132,7 @@ private:
         }
     };
 
+public:
     mutable unsynch_mpq_manager         m_num_manager;
     mutable u_dependency_manager        m_dep_manager;
     im_config                           m_config;
@@ -139,14 +140,27 @@ private:
 
     typedef interval_manager<im_config>::interval interval;
 
+    unsynch_mpq_manager& num_manager() { return m_num_manager; }
+    const unsynch_mpq_manager& num_manager() const { return m_num_manager; }
+    
     u_dependency* mk_leaf(unsigned d) { return m_dep_manager.mk_leaf(d); }
     u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); }
 
     template <enum with_deps_t wd>
-    void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const;
-
-    template <enum with_deps_t wd>
-    void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const;
+    void mul(const rational& r, const interval& a, interval& b) const {
+        if (r.is_zero()) return;
+        m_imanager.mul(r.to_mpq(), a, b);
+        if (wd == with_deps) {
+            if (r.is_pos()) {
+                b.m_lower_dep = a.m_lower_dep;
+                b.m_upper_dep = a.m_upper_dep;
+            }
+            else {
+                b.m_upper_dep = a.m_lower_dep;
+                b.m_lower_dep = a.m_upper_dep;
+            }
+        }
+    }
 
     void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
     void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
@@ -179,10 +193,8 @@ public:
     bool is_zero(const interval& a) const { return m_config.is_zero(a); }
     bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
     bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
-
-    template <enum with_deps_t wd>
-    void mul(const rational& r, const interval& a, interval& b) const;
-
+    bool lower_is_open(const interval& a) const { return m_config.lower_is_open(a); }
+    bool upper_is_open(const interval& a) const { return m_config.upper_is_open(a); }
     void add(const rational& r, interval& a) const;
     void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
     void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
@@ -197,16 +209,43 @@ public:
     }
 
     template <enum with_deps_t wd>
-    interval power(const interval& a, unsigned n);
+    interval power(const interval& a, unsigned n) {
+        interval b;
+        if (with_deps == wd) {
+            interval_deps_combine_rule combine_rule;
+            m_imanager.power(a, n, b, combine_rule);
+            combine_deps(a, combine_rule, b);
+        }
+        else {
+            m_imanager.power(a, n, b);
+        }
+        TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = ";
+              display(tout, b) << "\n"; );
+        return b;
+    }
 
     template <enum with_deps_t wd>
-    void copy_upper_bound(const interval& a, interval& i) const;
+    void copy_upper_bound(const interval& a, interval& i) const {
+        SASSERT(a.m_upper_inf == false);
+        i.m_upper_inf = false;
+        m_config.set_upper(i, a.m_upper);
+        i.m_upper_open = a.m_upper_open;
+        if (wd == with_deps) {
+            i.m_upper_dep = a.m_upper_dep;
+        }
+    }
 
     template <enum with_deps_t wd>
-    void copy_lower_bound(const interval& a, interval& i) const;
-    
-    template <enum with_deps_t wd>
-    interval intersect(const interval& a, const interval& b) const;
+    void copy_lower_bound(const interval& a, interval& i) const {
+        SASSERT(a.m_lower_inf == false);
+        i.m_lower_inf = false;
+        m_config.set_lower(i, a.m_lower);
+        i.m_lower_open = a.m_lower_open;
+        if (wd == with_deps) {
+            i.m_lower_dep = a.m_lower_dep;
+        }
+    }
+
 
     void set_zero_interval_deps_for_mult(interval&);
     void set_zero_interval(interval&, u_dependency* dep = nullptr) const;
@@ -223,4 +262,75 @@ public:
     mpq const& upper(interval const& a) const { return m_config.upper(a); }
     bool is_empty(interval const& a) const;
     void set_interval_for_scalar(interval&, const rational&);
+    template <typename T> 
+    void linearize(u_dependency* dep, T& expl) const { m_dep_manager.linearize(dep, expl); }
+
+    void reset() { m_dep_manager.reset(); }
+    
+    template <enum with_deps_t wd> interval intersect(const interval& a, const interval& b) const {
+        interval i;
+        update_lower_for_intersection<wd>(a, b, i);
+        update_upper_for_intersection<wd>(a, b, i);
+        return i;
+    }
+
+    template <enum with_deps_t wd>
+    void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const {
+        if (a.m_lower_inf) {
+            if (b.m_lower_inf)
+                return;
+            copy_lower_bound<wd>(b, i);
+            return;
+        }
+        if (b.m_lower_inf) {
+            SASSERT(!a.m_lower_inf);
+            copy_lower_bound<wd>(a, i);
+            return;
+        }
+        if (m_num_manager.lt(a.m_lower, b.m_lower)) {
+            copy_lower_bound<wd>(b, i);
+            return;
+        }
+        if (m_num_manager.gt(a.m_lower, b.m_lower)) {
+            copy_lower_bound<wd>(a, i);
+            return;
+        }
+        SASSERT(m_num_manager.eq(a.m_lower, b.m_lower));
+        if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here
+            copy_lower_bound<wd>(a, i);
+            return;
+        }
+        copy_lower_bound<wd>(b, i);
+    }
+
+    template <enum with_deps_t wd>
+    void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const {
+        if (a.m_upper_inf) {
+            if (b.m_upper_inf)
+                return;
+            copy_upper_bound<wd>(b, i);
+            return;
+        }
+        if (b.m_upper_inf) {
+            SASSERT(!a.m_upper_inf);
+            copy_upper_bound<wd>(a, i);
+            return;
+        }
+        if (m_num_manager.gt(a.m_upper, b.m_upper)) {
+            copy_upper_bound<wd>(b, i);
+            return;
+        }
+        if (m_num_manager.lt(a.m_upper, b.m_upper)) {
+            copy_upper_bound<wd>(a, i);
+            return;
+        }
+        SASSERT(m_num_manager.eq(a.m_upper, b.m_upper));
+        if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here
+            copy_upper_bound<wd>(a, i);
+            return;
+        }
+
+        copy_upper_bound<wd>(b, i);
+    }
+    typedef im_config::interval interv;
 };
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index fdb710f02..208f657d2 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -25,7 +25,7 @@
 
 namespace nla {
 typedef intervals::interval interv;
-horner::horner(core * c, intervals * i) : common(c, i), m_row_sum(m_nex_creator), m_fixed_as_scalars(false) {}
+horner::horner(core * c, intervals * i) : common(c, i), m_row_sum(m_nex_creator) {}
 
 template <typename T>
 bool horner::row_has_monomial_to_refine(const T& row) const {
@@ -72,13 +72,13 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
 template <typename T> 
 bool horner::lemmas_on_row(const T& row) {
     cross_nested cn(
-        [this](const nex* n) { return m_intervals->check_nex(n,  m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); },
+        [this](const nex* n) { return m_intervals->check_nex(n, nullptr); },
         [this](unsigned j)   { return c().var_is_fixed(j); },
         [this]() { return c().random(); }, m_nex_creator);
 
     SASSERT (row_is_interesting(row));
     c().clear_and_resize_active_var_set();
-    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars, nullptr);
+    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, nullptr);
     set_active_vars_weights(); // without this call the comparisons will be incorrect
     nex* e =  m_nex_creator.simplify(m_row_sum.mk());
     TRACE("nla_horner", tout << "e = " << * e << "\n";);
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index 2328d1cd2..352309c5e 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -32,7 +32,6 @@ class core;
 class horner : common {
     nex_creator::sum_factory  m_row_sum;
     unsigned         m_row_index;                      
-    bool             m_fixed_as_scalars;
 public:
     typedef intervals::interval interv;
     horner(core *core, intervals*);
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index c2b485622..6eaee238c 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -123,18 +123,9 @@ unsigned common::random() {
 }
 
 // creates a nex expression for the coeff and var, 
-// replaces the fixed vars with scalars
-nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixed_as_scalars) {
+nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
     SASSERT(!coeff.is_zero());
     if (!c().is_monic_var(j)) {
-        if (fixed_as_scalars && c().var_is_fixed(j)) {
-            auto & b = c().m_lar_solver.get_lower_bound(j).x;
-            if (b.is_zero()) {
-                TRACE("nla_grobner", tout << "[" << j << "] is fixed to zero\n";); 
-                return nullptr;
-            }
-            return cn.mk_scalar(coeff * b);
-        } 
         c().insert_to_active_var_set(j);
         return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
     }
@@ -142,15 +133,6 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
     nex_creator::mul_factory mf(cn);
     mf *= coeff;
     for (lpvar k : m.vars()) {
-        if (fixed_as_scalars && c().var_is_fixed(k)) {
-            auto & b = c().m_lar_solver.get_lower_bound(k).x;
-            if (b.is_zero()) {
-                TRACE("nla_grobner", tout << "[" << k << "] is fixed to zero\n";); 
-                return nullptr;
-            }
-            mf *=  b;
-            continue;
-        }  
         c().insert_to_active_var_set(k);
         mf *= cn.mk_var(k);
         CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
@@ -162,18 +144,17 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
 
 
 template <typename T> u_dependency* common::create_sum_from_row(const T& row,
-                                                                         nex_creator& cn,
-                                                                         nex_creator::sum_factory& sum,
-                                                                         bool fixed_as_scalars,
-                                                                         u_dependency_manager* dep_manager
-                                                                         ) {
+                                                                nex_creator& cn,
+                                                                nex_creator::sum_factory& sum,
+                                                                u_dependency_manager* dep_manager
+                                                                ) {
 
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
     u_dependency * dep = nullptr;
     SASSERT(row.size() > 1);
     sum.reset();
     for (const auto &p : row) {
-        nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars);
+        nex* e = nexvar(p.coeff(), p.var(), cn);
         if (!e)
             continue;
         unsigned lc, uc;
@@ -256,5 +237,4 @@ var_weight common::get_var_weight(lpvar j) const {
 
 
 }
-template u_dependency* nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, u_dependency_manager*);  
-template dependency_manager<scoped_dependency_manager<unsigned int>::config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, scoped_dependency_manager<unsigned int>&);
+template u_dependency* nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency_manager*);  
diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h
index 581c19ef5..9cf6dbe5a 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -116,10 +116,9 @@ struct common {
         typedef lp::constraint_index value;
     };
         
-    //    nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
-    nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool);
+    nex* nexvar(const rational& coeff, lpvar j, nex_creator&);
     template <typename T>
-    u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, u_dependency_manager*);
+    u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, u_dependency_manager*);
     template <typename T>
     u_dependency* get_fixed_vars_dep_from_row(const T&, u_dependency_manager& dep_manager);
     void set_active_vars_weights();
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 374a64c6e..bab20d050 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -24,8 +24,7 @@ using namespace nla;
 
 grobner::grobner(core *c, intervals *s)
     : common(c, s),
-      m_gc(m_nex_creator, c->m_reslim),
-      m_look_for_fixed_vars_in_rows(false) {
+      m_gc(m_nex_creator, c->m_reslim) {
     std::function<void (lp::explanation const& e, std::ostream & out)> de;
     de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); };
     grobner_core::params p;
@@ -174,7 +173,7 @@ void grobner::add_row(unsigned i) {
     TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
           for (auto p : row) c().print_var(p.var(), tout) << "\n"; );
     nex_creator::sum_factory sf(m_nex_creator);
-    u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep());
+    u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, &m_gc.dep());
     nex* e = m_nex_creator.simplify(sf.mk());
     TRACE("grobner", tout << "e = " << *e << "\n";);
     m_gc.assert_eq_0(e, dep);
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 894f5495d..b8896eb6e 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -206,7 +206,6 @@ class grobner : common {
     grobner_core m_gc;
     unsigned     m_reported;
     lp::int_set  m_rows;
-    bool         m_look_for_fixed_vars_in_rows;
 public:
     grobner(core *, intervals *);
     void grobner_lemmas();
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 9174bded0..d5aa9f05b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -4,19 +4,7 @@
 #include "util/mpq.h"
 
 namespace nla {
-
-
-typedef intervals::interval interv;
-typedef enum intervals::with_deps_t e_with_deps;
-
-void intervals::set_interval_for_scalar(interv& a, const rational& v) {
-    set_lower(a, v);
-    set_upper(a, v);
-    set_lower_is_open(a, false);
-    set_lower_is_inf(a, false);
-    set_upper_is_open(a, false);
-    set_upper_is_inf(a, false);
-}
+typedef enum dep_intervals::with_deps_t e_with_deps;
 
 const nex* intervals::get_inf_interval_child(const nex_sum& e) const {
     for (auto * c : e) {
@@ -68,7 +56,7 @@ const nex* intervals::get_zero_interval_child(const nex_mul& e) const {
 
 std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream& out) const {
     svector<lp::constraint_index> expl;
-    m_dep_manager.linearize(deps, expl);
+    m_dep_intervals.linearize(deps, expl);
     {
         lp::explanation e(expl);
         if (!expl.empty()) {
@@ -84,15 +72,15 @@ std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream&
 // return true iff the interval of n is does not contain 0
 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<without_deps>(n, 1);
-    if (!separated_from_zero(i)) {
-        reset();
+    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<with_deps>(n, 1);
+    auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
     TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
-    check_interval_for_conflict_on_zero(interv_wd, initial_deps);
-    reset(); // clean the memory allocated by the interval bound dependencies
+    m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps);
+    m_dep_intervals.reset(); // clean the memory allocated by the interval bound dependencies
     return true;
 }
 
@@ -175,113 +163,59 @@ lpvar intervals::find_term_column(const lp::lar_term & norm_t, rational& a) cons
     return -1;
 }
 
-void intervals::set_zero_interval_with_explanation(interval& i, const lp::explanation& exp) const {
+void intervals::set_zero_interval_with_explanation(interval& i, const lp::explanation& exp) {
     auto val = rational(0);
-    m_config.set_lower(i, val);
-    m_config.set_lower_is_open(i, false);
-    m_config.set_lower_is_inf(i, false);
-    m_config.set_upper(i, val);
-    m_config.set_upper_is_open(i, false);
-    m_config.set_upper_is_inf(i, false);
+    m_dep_intervals.set_lower(i, val);
+    m_dep_intervals.set_lower_is_open(i, false);
+    m_dep_intervals.set_lower_is_inf(i, false);
+    m_dep_intervals.set_upper(i, val);
+    m_dep_intervals.set_upper_is_open(i, false);
+    m_dep_intervals.set_upper_is_inf(i, false);
     i.m_lower_dep = i.m_upper_dep = mk_dep(exp);
 }
 
-void intervals::set_zero_interval(interval& i) const {
+void intervals::set_zero_interval(interval& i) {
     auto val = rational(0);
-    m_config.set_lower(i, val);
-    m_config.set_lower_is_open(i, false);
-    m_config.set_lower_is_inf(i, false);
-    m_config.set_upper(i, val);
-    m_config.set_upper_is_open(i, false);
-    m_config.set_upper_is_inf(i, false);
+    m_dep_intervals.set_lower(i, val);
+    m_dep_intervals.set_lower_is_open(i, false);
+    m_dep_intervals.set_lower_is_inf(i, false);
+    m_dep_intervals.set_upper(i, val);
+    m_dep_intervals.set_upper_is_open(i, false);
+    m_dep_intervals.set_upper_is_inf(i, false);
 }
 
 void intervals::set_zero_interval_deps_for_mult(interval& a) {
-    a.m_lower_dep = m_dep_manager.mk_join(a.m_lower_dep, a.m_upper_dep);
+    a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep);
     a.m_upper_dep = a.m_lower_dep;
 }
 
-bool intervals::separated_from_zero_on_lower(const interval& i) const {
-    if (lower_is_inf(i))
-        return false;
-    if (unsynch_mpq_manager::is_neg(lower(i)))
-        return false;
-    if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i))
-        return false;
-    return true;
+u_dependency *intervals::mk_dep(lp::constraint_index ci) {
+    return m_dep_intervals.mk_leaf(ci);
 }
 
-bool intervals::separated_from_zero_on_upper(const interval& i) const {
-    if (upper_is_inf(i))
-        return false;
-    if (unsynch_mpq_manager::is_pos(upper(i)))
-        return false;
-    if (unsynch_mpq_manager::is_zero(upper(i)) && !m_config.upper_is_open(i))
-        return false;
-    return true;
-}
-
-bool intervals::check_interval_for_conflict_on_zero(const interval & i, u_dependency* dep) {
-    return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep);
-}
-
-bool intervals::check_interval_for_conflict_on_zero_upper(
-    const interval & i,
-    u_dependency* dep) {
-    if (!separated_from_zero_on_upper(i))
-        return false;
-
-    TRACE("grobner", display(tout, i););
-    m_core->add_empty_lemma();
-    svector<lp::constraint_index> expl;
-    dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
-    m_dep_manager.linearize(dep, expl); 
-    m_core->current_expl().add_expl(expl);
-    TRACE("nla_solver", m_core->print_lemma(tout););
-    return true;
-}
-
-bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency* dep) {
-    if (!separated_from_zero_on_lower(i)) {
-        return false;
-    }
-    TRACE("grobner", display(tout, i););
-    m_core->add_empty_lemma();
-    svector<lp::constraint_index> expl;
-    dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
-    m_dep_manager.linearize(dep, expl); 
-    m_core->current_expl().add_expl(expl);
-    TRACE("nla_solver", m_core->print_lemma(tout););
-    return true;
-}
-
-u_dependency *intervals::mk_dep(lp::constraint_index ci) const {
-    return m_dep_manager.mk_leaf(ci);
-}
-
-u_dependency *intervals::mk_dep(const lp::explanation& expl) const {
+u_dependency *intervals::mk_dep(const lp::explanation& expl) {
     u_dependency * r = nullptr;
     for (auto p : expl) {
         if (r == nullptr) {
-            r = m_dep_manager.mk_leaf(p.second);
+            r = m_dep_intervals.mk_leaf(p.second);
         } else {
-            r = m_dep_manager.mk_join(r, m_dep_manager.mk_leaf(p.second));
+            r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.second));
         }
     }
     return r;
 }
 
 std::ostream& intervals::display(std::ostream& out, const interval& i) const {
-    if (m_imanager.lower_is_inf(i)) {
+    if (m_dep_intervals.lower_is_inf(i)) {
         out << "(-oo";
     } else {
-        out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));        
+        out << (m_dep_intervals.lower_is_open(i)? "(":"[") << rational(m_dep_intervals.lower(i));        
     }
     out << ",";
-    if (m_imanager.upper_is_inf(i)) {
+    if (m_dep_intervals.upper_is_inf(i)) {
         out << "oo)";
     } else {
-        out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]");         
+        out << rational(m_dep_intervals.upper(i)) << (m_dep_intervals.upper_is_open(i)? ")":"]");         
     }
     svector<lp::constraint_index> expl;
     if (i.m_lower_dep) {
@@ -296,37 +230,37 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
 }
 
 template <e_with_deps wd>
-void intervals::set_var_interval(lpvar v, interval& b) const {
+void intervals::set_var_interval(lpvar v, interval& b) {
     TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";);
     lp::constraint_index ci;
     rational val;
     bool is_strict;
     if (ls().has_lower_bound(v, ci, val, is_strict)) {
-        m_config.set_lower(b, val);
-        m_config.set_lower_is_open(b, is_strict);
-        m_config.set_lower_is_inf(b, false);
-        if (wd == with_deps) b.m_lower_dep = mk_dep(ci);
+        m_dep_intervals.set_lower(b, val);
+        m_dep_intervals.set_lower_is_open(b, is_strict);
+        m_dep_intervals.set_lower_is_inf(b, false);
+        if (wd == e_with_deps::with_deps) b.m_lower_dep = mk_dep(ci);
     }
     else {
-        m_config.set_lower_is_open(b, true);
-        m_config.set_lower_is_inf(b, true);
-        if (wd == with_deps) b.m_lower_dep = nullptr;
+        m_dep_intervals.set_lower_is_open(b, true);
+        m_dep_intervals.set_lower_is_inf(b, true);
+        if (wd == e_with_deps::with_deps) b.m_lower_dep = nullptr;
     }
     if (ls().has_upper_bound(v, ci, val, is_strict)) {
-        m_config.set_upper(b, val);
-        m_config.set_upper_is_open(b, is_strict);
-        m_config.set_upper_is_inf(b, false);
-        if (wd == with_deps) b.m_upper_dep = mk_dep(ci);
+        m_dep_intervals.set_upper(b, val);
+        m_dep_intervals.set_upper_is_open(b, is_strict);
+        m_dep_intervals.set_upper_is_inf(b, false);
+        if (wd == e_with_deps::with_deps) b.m_upper_dep = mk_dep(ci);
     }
     else {
-        m_config.set_upper_is_open(b, true);
-        m_config.set_upper_is_inf(b, true);
-        if (wd == with_deps) b.m_upper_dep = nullptr;
+        m_dep_intervals.set_upper_is_open(b, true);
+        m_dep_intervals.set_upper_is_inf(b, true);
+        if (wd == e_with_deps::with_deps) b.m_upper_dep = nullptr;
     }
 }
 
 template <e_with_deps wd>
-bool intervals::interval_from_term(const nex& e, interv& i) const {
+bool intervals::interval_from_term(const nex& e, interval& i) {
     rational a, b;
     lp::lar_term norm_t = expression_to_normalized_term(&e.to_sum(), a, b);
     lp::explanation exp;
@@ -339,11 +273,11 @@ bool intervals::interval_from_term(const nex& e, interv& i) const {
     if (j + 1 == 0)
         return false;
 
-    set_var_interval<without_deps>(j, i);
-    interv bi;
-    mul<wd>(a, i, bi);
-    add(b, bi);
-    set<wd>(i, bi);
+    set_var_interval<e_with_deps::without_deps>(j, i);
+    interval bi;
+    m_dep_intervals.mul<wd>(a, i, bi);
+    m_dep_intervals.add(b, bi);
+    m_dep_intervals.set<wd>(i, bi);
 
     TRACE("nla_intervals",
           m_core->m_lar_solver.print_column_info(j, tout) << "\n";
@@ -353,27 +287,27 @@ bool intervals::interval_from_term(const nex& e, interv& i) const {
 }
 
 template <e_with_deps wd>
-interv intervals::interval_of_sum_no_term(const nex_sum& e) {
+intervals::interval intervals::interval_of_sum_no_term(const nex_sum& e) {
     const nex* inf_e = get_inf_interval_child(e);
     if (inf_e) {
-        return interv();
+        return interval();
     }
-    interv a = interval_of_expr<wd>(e[0], 1);
+    interval a = interval_of_expr<wd>(e[0], 1);
     for (unsigned k = 1; k < e.size(); k++) {
         TRACE("nla_intervals_details_sum", tout << "e[" << k << "]= " << *e[k] << "\n";);
-        interv b = interval_of_expr<wd>(e[k], 1);
-        interv c;
+        interval b = interval_of_expr<wd>(e[k], 1);
+        interval c;
 
         TRACE("nla_intervals_details_sum", tout << "a = "; display(tout, a) << "\nb = "; display(tout, b) << "\n";);
-        if (wd == with_deps) {
+        if (wd == e_with_deps::with_deps) {
             interval_deps_combine_rule combine_rule;
-            add(a, b, c, combine_rule);
-            combine_deps(a, b, combine_rule, c);
+            m_dep_intervals.add(a, b, c, combine_rule);
+            m_dep_intervals.combine_deps(a, b, combine_rule, c);
         }
         else {
-            add(a, b, c);
+            m_dep_intervals.add(a, b, c);
         }
-        set<wd>(a, c);
+        m_dep_intervals.set<wd>(a, c);
         TRACE("nla_intervals_details_sum", tout << *e[k] << ", ";
               display(tout, a); tout << "\n";);
     }
@@ -383,46 +317,16 @@ interv intervals::interval_of_sum_no_term(const nex_sum& e) {
 }
 
 template <e_with_deps wd>
-void intervals::update_upper_for_intersection(const interval& a, const interval& b, interval& i) const {
-    if (a.m_upper_inf) {
-        if (b.m_upper_inf)
-            return;
-        copy_upper_bound<wd>(b, i);
-        return;
-    }
-    if (b.m_upper_inf) {
-        SASSERT(!a.m_upper_inf);
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-    if (m_num_manager.gt(a.m_upper, b.m_upper)) {
-        copy_upper_bound<wd>(b, i);
-        return;
-    }
-    if (m_num_manager.lt(a.m_upper, b.m_upper)) {
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-    SASSERT(m_num_manager.eq(a.m_upper, b.m_upper));
-    if (a.m_upper_open) { // we might consider to look at b.m_upper_open too here
-        copy_upper_bound<wd>(a, i);
-        return;
-    }
-
-    copy_upper_bound<wd>(b, i);
-}
-
-template <e_with_deps wd>
-interv intervals::interval_of_sum(const nex_sum& e) {
+intervals::interval intervals::interval_of_sum(const nex_sum& e) {
     TRACE("nla_intervals_details", tout << "e=" << e << "\n";);
-    interv i_e = interval_of_sum_no_term<wd>(e);
+    interval i_e = interval_of_sum_no_term<wd>(e);
     if (e.is_a_linear_term()) {
         SASSERT(e.is_sum() && e.size() > 1);
-        interv i_from_term;
+        interval i_from_term;
         if (interval_from_term<wd>(e, i_from_term)) {
-            interv r = intersect<wd>(i_e, i_from_term);
+            interval r = m_dep_intervals.intersect<wd>(i_e, i_from_term);
             TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";);
-            if (is_empty(r)) {
+            if (m_dep_intervals.is_empty(r)) {
                 SASSERT(false); // not implemented
             }
             return r;
@@ -433,35 +337,35 @@ interv intervals::interval_of_sum(const nex_sum& e) {
 }
 
 template <e_with_deps wd>
-interv intervals::interval_of_mul(const nex_mul& e) {
+intervals::interval intervals::interval_of_mul(const nex_mul& e) {
     TRACE("nla_intervals_details", tout << "e = " << e << "\n";);
     const nex* zero_interval_child = get_zero_interval_child(e);
     if (zero_interval_child) {
-        interv a = interval_of_expr<wd>(zero_interval_child, 1);
-        if(wd == with_deps)
+        interval a = interval_of_expr<wd>(zero_interval_child, 1);
+        if(wd == e_with_deps::with_deps)
             set_zero_interval_deps_for_mult(a);
         TRACE("nla_intervals_details", tout << "zero_interval_child = " << *zero_interval_child << std::endl << "a = "; display(tout, a); );
         return a;
     }
 
-    interv a;
-    set_interval_for_scalar(a, e.coeff());
+    interval a;
+    m_dep_intervals.set_interval_for_scalar(a, e.coeff());
     TRACE("nla_intervals_details", tout << "a = "; display(tout, a); );
     for (const auto& ep : e) {
-        interv b = interval_of_expr<wd>(ep.e(), ep.pow());
+        interval b = interval_of_expr<wd>(ep.e(), ep.pow());
         TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); );
-        interv c;
-        if (wd == with_deps) {
+        interval c;
+        if (wd == e_with_deps::with_deps) {
             interval_deps_combine_rule comb_rule;
-            mul_two_intervals(a, b, c, comb_rule);
+            m_dep_intervals.mul(a, b, c, comb_rule);
             TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c););
-            combine_deps(a, b, comb_rule, c);
+            m_dep_intervals.combine_deps(a, b, comb_rule, c);
         } else {
-            mul_two_intervals(a, b, c);
+            m_dep_intervals.mul(a, b, c);
         }
         TRACE("nla_intervals_details", tout << "a "; display(tout, a););
         TRACE("nla_intervals_details", tout << "c "; display(tout, c););
-        set<wd>(a, c);
+        m_dep_intervals.set<wd>(a, c);
         TRACE("nla_intervals_details", tout << "part mult "; display(tout, a););
     }
     TRACE("nla_intervals_details", tout << "e=" << e << "\n";
@@ -470,31 +374,31 @@ interv intervals::interval_of_mul(const nex_mul& e) {
 }
 
 template <e_with_deps wd>
-interv intervals::interval_of_expr(const nex* e, unsigned p) {
-    interv a;
+intervals::interval intervals::interval_of_expr(const nex* e, unsigned p) {
+    interval a;
     switch (e->type()) {
     case expr_type::SCALAR:
-        set_interval_for_scalar(a, to_scalar(e)->value());
+        m_dep_intervals.set_interval_for_scalar(a, to_scalar(e)->value());
         if (p != 1) {
-            return power<wd>(a, p);
+            return m_dep_intervals.power<wd>(a, p);
         }
         return a;
     case expr_type::SUM: {
-        interv b = interval_of_sum<wd>(e->to_sum());
+        interval b = interval_of_sum<wd>(e->to_sum());
         if (p != 1)
-            return power<wd>(b, p);
+            return m_dep_intervals.power<wd>(b, p);
         return b;
     }
     case expr_type::MUL: {
-        interv b = interval_of_mul<wd>(e->to_mul());
+        interval b = interval_of_mul<wd>(e->to_mul());
         if (p != 1)
-            return power<wd>(b, p);
+            return m_dep_intervals.power<wd>(b, p);
         return b;
     }
     case expr_type::VAR:
         set_var_interval<wd>(e->to_var().var(), a);
         if (p != 1)
-            return power<wd>(a, p);;
+            return m_dep_intervals.power<wd>(a, p);;
         return a;
     default:
         TRACE("nla_intervals_details", tout << e->type() << "\n";);
@@ -511,5 +415,3 @@ const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
 
 } // end of nla namespace
 
-// instantiate the template
-template class interval_manager<nla::intervals::im_config>;
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 5f3e89823..43e6f2ba8 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -23,344 +23,69 @@
 #include "math/lp/nla_common.h"
 #include "math/lp/lar_solver.h"
 #include "math/interval/interval.h"
+#include "math/interval/dep_intervals.h"
 #include "util/dependency.h"
 
 namespace nla {
 class core;
 
 class intervals {
-    class im_config {
-        unsynch_mpq_manager& m_manager;
-        u_dependency_manager& m_dep_manager;
-
-    public:
-        typedef unsynch_mpq_manager numeral_manager;
-
-
-        struct interval {
-            interval() :
-                m_lower(), m_upper(),
-                m_lower_open(1), m_upper_open(1),
-                m_lower_inf(1), m_upper_inf(1),
-                m_lower_dep(nullptr), m_upper_dep(nullptr) {}
-            mpq   m_lower;
-            mpq   m_upper;
-            unsigned  m_lower_open : 1;
-            unsigned  m_upper_open : 1;
-            unsigned  m_lower_inf : 1;
-            unsigned  m_upper_inf : 1;
-            u_dependency* m_lower_dep; // justification for the lower bound
-            u_dependency* m_upper_dep; // justification for the upper bound
-        };
-
-        void add_deps(interval const& a, interval const& b,
-            interval_deps_combine_rule const& deps, interval& i) const {
-            i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine);
-            i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
-        }
-
-        void add_deps(interval const& a,
-            interval_deps_combine_rule const& deps, interval& i) const {
-            i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
-            i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
-        }
-
-
-        // Should be NOOPs for precise mpq types.
-        // For imprecise types (e.g., floats) it should set the rounding mode.
-        void round_to_minus_inf() {}
-        void round_to_plus_inf() {}
-        void set_rounding(bool to_plus_inf) {}
-
-        // Getters
-        mpq const& lower(interval const& a) const { return a.m_lower; }
-        mpq const& upper(interval const& a) const { return a.m_upper; }
-        mpq& lower(interval& a) { return a.m_lower; }
-        mpq& upper(interval& a) { return a.m_upper; }
-        bool lower_is_open(interval const& a) const { return a.m_lower_open; }
-        bool upper_is_open(interval const& a) const { return a.m_upper_open; }
-        bool lower_is_inf(interval const& a) const { return a.m_lower_inf; }
-        bool upper_is_inf(interval const& a) const { return a.m_upper_inf; }
-        bool is_inf(interval const& a) const { return upper_is_inf(a) && lower_is_inf(a); }
-        bool is_zero(interval const& a) const {
-            return (!lower_is_inf(a)) && (!upper_is_inf(a)) &&
-                (!lower_is_open(a)) && (!upper_is_open(a)) &&
-                unsynch_mpq_manager::is_zero(a.m_lower) &&
-                unsynch_mpq_manager::is_zero(a.m_upper);
-        }
-
-        // Setters
-        void set_lower(interval& a, mpq const& n) const { m_manager.set(a.m_lower, n); }
-        void set_upper(interval& a, mpq const& n) const { m_manager.set(a.m_upper, n); }
-        void set_lower(interval& a, rational const& n) const { set_lower(a, n.to_mpq()); }
-        void set_upper(interval& a, rational const& n) const { set_upper(a, n.to_mpq()); }
-        void set_lower_is_open(interval& a, bool v) const { a.m_lower_open = v; }
-        void set_upper_is_open(interval& a, bool v) const { a.m_upper_open = v; }
-        void set_lower_is_inf(interval& a, bool v) const { a.m_lower_inf = v; }
-        void set_upper_is_inf(interval& a, bool v) const { a.m_upper_inf = v; }
-
-        // Reference to numeral manager
-        numeral_manager& m() const { return m_manager; }
-
-        im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {}
-    private:
-        u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const {
-            u_dependency* dep = nullptr;
-            if (dep_in_lower1(bd)) {
-                dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
-            }
-            if (dep_in_lower2(bd)) {
-                dep = m_dep_manager.mk_join(dep, b.m_lower_dep);
-            }
-            if (dep_in_upper1(bd)) {
-                dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
-            }
-            if (dep_in_upper2(bd)) {
-                dep = m_dep_manager.mk_join(dep, b.m_upper_dep);
-            }
-            return dep;
-        }
-
-        u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const {
-            u_dependency* dep = nullptr;
-            if (dep_in_lower1(bd)) {
-                dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
-            }
-            if (dep_in_upper1(bd)) {
-                dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
-            }
-            return dep;
-        }
-
-    };
-
-    region                              m_alloc;
-    mutable unsynch_mpq_manager         m_num_manager;
-    mutable u_dependency_manager        m_dep_manager;
-    im_config                           m_config;
-    mutable interval_manager<im_config> m_imanager;
-    core* m_core;
-
+    mutable dep_intervals     m_dep_intervals;
+    core*                     m_core;
+    
 public:
-    u_dependency_manager& dep_manager() { return m_dep_manager; }
-    typedef interval_manager<im_config>::interval interval;
+    typedef dep_intervals::interv interval;
 private:
-    u_dependency* mk_dep(lp::constraint_index ci) const;
-    u_dependency* mk_dep(lp::explanation const&) const;
+    u_dependency* mk_dep(lp::constraint_index ci);
+    u_dependency* mk_dep(lp::explanation const&);
     lp::lar_solver& ls();
     const lp::lar_solver& ls() const;
 public:
-    enum with_deps_t { with_deps, without_deps };
 
     intervals(core* c, reslimit& lim) :
-        m_alloc(),
-        m_dep_manager(),
-        m_config(m_num_manager, m_dep_manager),
-        m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
+        m_dep_intervals(lim),
         m_core(c)
     {}
-    u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); }
-    u_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci); }
+    u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_intervals.mk_join(a, b); }
+    u_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_intervals.mk_leaf(ci); }
 
     std::ostream& print_dependencies(u_dependency*, std::ostream&) const;
     std::ostream& display(std::ostream& out, const intervals::interval& i) const;
-    void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); }
-    void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); }
-    void set_lower_is_open(interval& a, bool strict) { m_config.set_lower_is_open(a, strict); }
-    void set_lower_is_inf(interval& a, bool inf) { m_config.set_lower_is_inf(a, inf); }
-    void set_upper_is_open(interval& a, bool strict) { m_config.set_upper_is_open(a, strict); }
-    void set_upper_is_inf(interval& a, bool inf) { m_config.set_upper_is_inf(a, inf); }
-    bool is_zero(const interval& a) const { return m_config.is_zero(a); }
+    void set_lower(interval& a, rational const& n) const { m_dep_intervals.set_lower(a, n.to_mpq()); }
+    void set_upper(interval& a, rational const& n) const { m_dep_intervals.set_upper(a, n.to_mpq()); }
+    void set_lower_is_open(interval& a, bool strict) { m_dep_intervals.set_lower_is_open(a, strict); }
+    void set_lower_is_inf(interval& a, bool inf) { m_dep_intervals.set_lower_is_inf(a, inf); }
+    void set_upper_is_open(interval& a, bool strict) { m_dep_intervals.set_upper_is_open(a, strict); }
+    void set_upper_is_inf(interval& a, bool inf) { m_dep_intervals.set_upper_is_inf(a, inf); }
+    bool is_zero(const interval& a) const { return m_dep_intervals.is_zero(a); }
+
+    template <dep_intervals::with_deps_t wd>
+    void set_var_interval(lpvar v, interval& b);
+
+    template <dep_intervals::with_deps_t wd>
+    bool interval_from_term(const nex& e, interval& i); 
 
 
-    template <enum with_deps_t wd>
-    void mul(const rational& r, const interval& a, interval& b) const {
-        m_imanager.mul(r.to_mpq(), a, b);
-        if (wd == with_deps) {
-            if (r.is_pos()) {
-                b.m_lower_dep = a.m_lower_dep;
-                b.m_upper_dep = a.m_upper_dep;
-            }
-            else {
-                SASSERT(r.is_neg());
-                b.m_upper_dep = a.m_lower_dep;
-                b.m_lower_dep = a.m_upper_dep;
-            }
-        }
-    }
-
-    void add(const rational& r, interval& a) const {
-        if (!a.m_lower_inf) {
-            m_config.set_lower(a, a.m_lower + r);
-        }
-        if (!a.m_upper_inf) {
-            m_config.set_upper(a, a.m_upper + r);
-        }
-    }
-
-    void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
-    void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }
-    void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
-
-    template <enum with_deps_t wd>
-    void set(interval& a, const interval& b) const {
-        m_imanager.set(a, b);
-        if (wd == with_deps) {
-            a.m_lower_dep = b.m_lower_dep;
-            a.m_upper_dep = b.m_upper_dep;
-        }
-    }
-
-    void mul_two_intervals(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
-
-    void mul_two_intervals(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
-
-    
-    void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
-        SASSERT(&a != &i && &b != &i);
-        m_config.add_deps(a, b, deps, i);
-    }
-
-    void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
-        SASSERT(&a != &i);
-        m_config.add_deps(a, deps, i);
-    }
-
-    template <enum with_deps_t wd>
-    interval power(const interval& a, unsigned n) {
-        interv b;
-        if (with_deps == wd) {
-            interval_deps_combine_rule combine_rule;
-            m_imanager.power(a, n, b, combine_rule);
-            combine_deps(a, combine_rule, b);
-        }
-        else {
-            m_imanager.power(a, n, b);
-        }
-        TRACE("nla_horner_details", tout << "power of "; display(tout, a) << " = ";
-        display(tout, b) << "\n"; );
-        return b;
-    }
-
-    template <enum with_deps_t wd>
-    void update_lower_for_intersection(const interval& a, const interval& b, interval& i) const {
-        if (a.m_lower_inf) {
-            if (b.m_lower_inf)
-                return;
-            copy_lower_bound<wd>(b, i);
-            return;
-        }
-        if (b.m_lower_inf) {
-            SASSERT(!a.m_lower_inf);
-            copy_lower_bound<wd>(a, i);
-            return;
-        }
-        if (m_num_manager.lt(a.m_lower, b.m_lower)) {
-            copy_lower_bound<wd>(b, i);
-            return;
-        }
-        if (m_num_manager.gt(a.m_lower, b.m_lower)) {
-            copy_lower_bound<wd>(a, i);
-            return;
-        }
-        SASSERT(m_num_manager.eq(a.m_lower, b.m_lower));
-        if (a.m_lower_open) { // we might consider to look at b.m_lower_open too here
-            copy_lower_bound<wd>(a, i);
-            return;
-        }
-
-        copy_lower_bound<wd>(b, i);
-    }
-
-    template <enum with_deps_t wd>
-    void copy_upper_bound(const interval& a, interval& i) const {
-        SASSERT(a.m_upper_inf == false);
-        i.m_upper_inf = false;
-        m_config.set_upper(i, a.m_upper);
-        i.m_upper_open = a.m_upper_open;
-        if (wd == with_deps) {
-            i.m_upper_dep = a.m_upper_dep;
-        }
-    }
-
-    template <enum with_deps_t wd>
-    void copy_lower_bound(const interval& a, interval& i) const {
-        SASSERT(a.m_lower_inf == false);
-        i.m_lower_inf = false;
-        m_config.set_lower(i, a.m_lower);
-        i.m_lower_open = a.m_lower_open;
-        if (wd == with_deps) {
-            i.m_lower_dep = a.m_lower_dep;
-        }
-
-    }
-
-    template <enum with_deps_t wd>
-    void set_var_interval(lpvar v, interval& b) const;
-
-    template <enum with_deps_t wd>
-    void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const;
-    
-    template <enum with_deps_t wd>
-    interval intersect(const interval& a, const interval& b) const {
-        interval i;
-        TRACE("nla_interval_compare", tout << "a="; display(tout, a) << "\nb="; display(tout, b););
-        update_lower_for_intersection<wd>(a, b, i);
-        TRACE("nla_interval_compare", tout << "i="; display(tout, i) << "\n";);
-        update_upper_for_intersection<wd>(a, b, i);
-        TRACE("nla_interval_compare", tout << "i="; display(tout, i) << "\n";);
-        return i;
-    }
-
-    template <enum with_deps_t wd>
-
-    bool interval_from_term(const nex& e, interval& i) const; 
-
-
-    template <enum with_deps_t wd>
+    template <dep_intervals::with_deps_t wd>
     interval interval_of_sum_no_term(const nex_sum& e);
 
-    template <enum with_deps_t wd>
+    template <dep_intervals::with_deps_t wd>
     interval interval_of_sum(const nex_sum& e);
 
-    template <enum with_deps_t wd>
+    template <dep_intervals::with_deps_t wd>
     interval interval_of_mul(const nex_mul& e); 
 
-    template <enum with_deps_t wd>
+    template <dep_intervals::with_deps_t wd>
     interval interval_of_expr(const nex* e, unsigned p); 
-    bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
-    bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
+    bool upper_is_inf(const interval& a) const { return m_dep_intervals.upper_is_inf(a); }
+    bool lower_is_inf(const interval& a) const { return m_dep_intervals.lower_is_inf(a); }
 
     void set_zero_interval_deps_for_mult(interval&);
-    void set_zero_interval_with_explanation(interval&, const lp::explanation& exp) const;
-    void set_zero_interval(interval&) const;
-    bool is_inf(const interval& i) const { return m_config.is_inf(i); }
-    bool separated_from_zero_on_lower(const interval&) const;
-    bool separated_from_zero_on_upper(const interval&) const;
-    inline  bool separated_from_zero(const interval& i) const {
-        return separated_from_zero_on_upper(i) ||
-            separated_from_zero_on_lower(i);
-    }
-    bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*);
-    bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*);
-    bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*);
-    mpq const& lower(interval const& a) const { return m_config.lower(a); }
-    mpq const& upper(interval const& a) const { return m_config.upper(a); }
-    inline bool is_empty(interval const& a) const {
-        if (a.m_lower_inf || a.m_upper_inf)
-            return false;
-        if (m_num_manager.gt(a.m_lower, a.m_upper))
-            return true;
-        if (m_num_manager.lt(a.m_lower, a.m_upper))
-            return false;
-        if (a.m_lower_open || a.m_upper_open)
-            return true;
-        return false;
-    }
-    void reset() { m_alloc.reset(); }
+    void set_zero_interval_with_explanation(interval&, const lp::explanation& exp);
+    void set_zero_interval(interval&);
+    bool is_inf(const interval& i) const { return m_dep_intervals.is_inf(i); }
+
     bool check_nex(const nex*, u_dependency*);
-    typedef interval interv;
-    void set_interval_for_scalar(interv&, const rational&);
     const nex* get_zero_interval_child(const nex_mul&) const;
     const nex* get_inf_interval_child(const nex_sum&) const;
     bool has_zero_interval(const nex&) const;