diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 647687b04..77c7422e5 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -28,6 +28,7 @@ z3_add_component(lp
     nla_basics_lemmas.cpp
     nla_common.cpp
     nla_core.cpp
+    nla_intervals.cpp
     nla_monotone_lemmas.cpp
     nla_order_lemmas.cpp
     nla_solver.cpp
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 9512ccb26..b6024187e 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1,4 +1,4 @@
-/*++
+ /*++
 Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
@@ -19,6 +19,7 @@ Revision History:
 --*/
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
+#include "math/lp/nla_expr.h"
 namespace nla {
 
 core::core(lp::lar_solver& s, reslimit & lim) :
@@ -1356,16 +1357,68 @@ lbool core::test_check(
     return check(l);
 }
 
+nla_expr<rational> core::mk_expr(lpvar j)  const {
+    return nla_expr<rational>::var(j);
+}
+
+nla_expr<rational> core::mk_expr(const rational &a, lpvar j)  const {
+    if (a == 1)
+        return mk_expr(j);
+    nla_expr<rational> r(expr_type::MUL);
+    r.add_child(nla_expr<rational>::scalar(a));
+    r.add_child(nla_expr<rational>::var(j));
+    return r;            
+}
+
+nla_expr<rational> core::mk_expr(const rational &a, const svector<lpvar>& vs) const {
+    nla_expr<rational> r(expr_type::MUL);
+    r.add_child(nla_expr<rational>::scalar(a));
+    for (lpvar j : vs)
+        r.add_child(nla_expr<rational>::var(j));
+    return r;            
+}
+nla_expr<rational> core::mk_expr(const lp::lar_term& t) const {
+    auto coeffs = t.coeffs_as_vector();
+    if (coeffs.size() == 1) {
+        return mk_expr(coeffs[0].first, coeffs[0].second);
+    }
+    nla_expr<rational> r(expr_type::SUM);
+    for (const auto & p : coeffs) {
+        lpvar j = p.second;
+        if (is_monomial_var(j))
+            r.add_child(mk_expr(p.first, m_emons[j].vars()));
+        else
+            r.add_child(mk_expr(p.first, j));
+    }
+    return r;
+}
+
 std::ostream& core::print_terms(std::ostream& out) const {
-    for (auto t: m_lar_solver.m_terms)
-        print_term(*t, out) << "\n";
+    for (unsigned i=0; i< m_lar_solver.m_terms.size(); i++) {
+        unsigned ext = i + m_lar_solver.terms_start_index();
+        if (!m_lar_solver.var_is_registered(ext)) {
+            out << "term is not registered\n";
+            continue;
+        }
+        
+        const lp::lar_term & t = *m_lar_solver.m_terms[i];
+        print_term(t, out) << std::endl;        
+        lpvar j = m_lar_solver.external_to_local(ext);
+        SASSERT(j + 1);
+        SASSERT(value(t) == val(j));
+        print_var(j, out);
+        out << "term again "; print_term(t, out) << std::endl;        
+        auto e = mk_expr(t);
+        out << "e= " << e << "\n";        
+    }
     return out;
 }
 std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
     return lp::print_linear_combination_customized(
         t.coeffs_as_vector(),
         [this](lpvar j) {
-            return is_monomial_var(j)? product_indices_str(m_emons[j].vars()) : (std::string("v") + lp::T_to_string(j));
+            return is_monomial_var(j)?
+                (product_indices_str(m_emons[j].vars()) + (check_monomial(m_emons[j])? "": "_")) : (std::string("v") + lp::T_to_string(j));
         },
         out);
 }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index cd8e2ed30..04ccfbca2 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -27,6 +27,7 @@
 #include "math/lp/nla_monotone_lemmas.h"
 #include "math/lp/emonomials.h"
 #include "math/lp/nla_settings.h"
+#include "math/lp/nla_expr.h"
 namespace nla {
 
 template <typename A, typename B>
@@ -344,7 +345,12 @@ public:
     lbool  test_check(vector<lemma>& l);
     lpvar map_to_root(lpvar) const;
     std::ostream& print_terms(std::ostream&) const;
-    std::ostream& print_term( const lp::lar_term&, std::ostream&) const;    
+    std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
+    nla_expr<rational> mk_expr(lpvar j) const;
+    nla_expr<rational> mk_expr(const rational &a, lpvar j) const;
+
+    nla_expr<rational> mk_expr(const rational &a, const svector<lpvar>& vs) const;
+    nla_expr<rational> mk_expr(const lp::lar_term& t) const;
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
new file mode 100644
index 000000000..31b04873b
--- /dev/null
+++ b/src/math/lp/nla_expr.h
@@ -0,0 +1,150 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
+#pragma once
+#include "math/lp/nla_defs.h"
+namespace nla {
+enum class expr_type { SUM, MUL, VAR, SCALAR };
+// This class is needed in horner calculation with intervals
+template <typename T>
+class nla_expr {
+    expr_type       m_type;
+    lpvar           m_j;
+    T             m_v; // for the scalar
+    vector<nla_expr> m_children;
+public:
+    std::string str() const { std::stringstream ss; ss << *this; return ss.str(); }
+    std::ostream & print_sum(std::ostream& out) const {
+        bool first = true;
+        for (const nla_expr& v : m_children) {
+            std::string s = v.str();
+            if (first) {
+                first = false;
+                if (v.is_simple())
+                    out << v;
+                else 
+                    out << "(" << s << ")";                            
+            } else {
+                if (v.is_simple()) {
+                    if (s[0] == '-') {
+                        out << s;
+                    } else {
+                        out << "+" << s;
+                    }
+                } else {
+                    out << "+" <<  "(" << s << ")";
+                }
+            }
+        }
+        return out;
+    }
+    std::ostream & print_mul(std::ostream& out) const {
+        bool first = true;
+        for (const nla_expr& v : m_children) {
+            std::string s = v.str();
+            if (first) {
+                first = false;
+                if (v.is_simple())
+                    out << s;
+                else 
+                    out << "(" << s << ")";                            
+            } else {
+                if (v.is_simple()) {
+                    if (s[0] == '-') {
+                        out << "*(" << s << ")";
+                    } else {
+                        out << "*" << s;
+                    }
+                } else {
+                    out << "*(" << s << ")";
+                }
+            }
+        }
+        return out;
+    }
+    std::ostream & print(std::ostream& out) const {
+        switch(m_type) {
+        case expr_type::SUM:
+            return print_sum(out);
+        case expr_type::MUL:
+            return print_mul(out);
+        case expr_type::VAR:
+            out << "v" << m_j;
+            return out;
+        case expr_type::SCALAR:
+            out << m_v;
+            return out;
+        default:
+            return out;
+        }
+    }
+
+    bool is_simple() const {
+        switch(m_type) {
+        case expr_type::SUM:
+        case expr_type::MUL:
+            return m_children.size() <= 1;
+        
+        default:
+            return true;
+        }
+    }
+
+    nla_expr(expr_type t): m_type(t) {}
+    
+    void add_child(const nla_expr& e) {
+        SASSERT(m_type == expr_type::SUM || m_type == expr_type::MUL);
+        m_children.push_back(e);
+    }
+
+    
+    static nla_expr sum(const nla_expr& v, const nla_expr & w) {
+        nla_expr r(expr_type::SUM);
+        r.add_child(v);
+        r.add_child(w);
+        return r;
+    }
+    static nla_expr mul(const nla_expr& v, const nla_expr & w) {
+        nla_expr r(expr_type::MUL);
+        r.add_child(v);
+        r.add_child(w);
+        return r;
+    }
+
+    static nla_expr scalar(const T& v)  {
+        nla_expr r(expr_type::SCALAR);
+        r.m_v = v;
+        return r;
+    }
+
+    static nla_expr var(lpvar j)  {
+        nla_expr r(expr_type::VAR);
+        r.m_j = j;
+        return r;
+    }
+    
+    
+};
+template <typename T>
+std::ostream& operator<<(std::ostream& out, const nla_expr<T>& e ) {
+    return e.print(out);
+}
+
+
+}
+    
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
new file mode 100644
index 000000000..52a3cd375
--- /dev/null
+++ b/src/math/lp/nla_intervals.cpp
@@ -0,0 +1,315 @@
+#include "math/lp/nla_core.h"
+#include "math/interval/interval_def.h"
+#include "math/lp/nla_intervals.h"
+
+namespace nla {
+
+bool intervals::get_lemmas() {
+    m_region.reset();
+    bool ret = false;
+    for (auto const& k : c().m_to_refine) {
+        if (get_lemma(c().emons()[k])) {
+            ret = true;
+        }
+        if (c().done())
+            break;
+    }
+    return ret;
+}
+// create a product of interval signs together with the depencies
+intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) const {
+    interval a, b, c;
+    m_imanager.set(a, mpq(1));
+    for (lpvar v : vars) {
+        set_var_interval_signs_with_deps(v, b);
+        interval_deps deps;
+        m_imanager.mul(a, b, c, deps);
+        m_imanager.set(a, c);
+        m_config.add_deps(a, b, deps, a);
+        if (m_imanager.is_zero(a))
+            return a;
+    }
+    return a;    
+}
+
+void intervals::get_lemma_for_zero_interval(monomial const& m) {
+    if (val(m).is_zero()) return;
+    interval signs_a = mul_signs_with_deps(m.vars());
+    add_empty_lemma();
+    svector<lp::constraint_index> expl;
+    m_dep_manager.linearize(signs_a.m_lower_dep, expl);
+    TRACE("nla_solver", print_vector(expl, tout) << "\n";);
+    _().current_expl().add_expl(expl);
+    mk_ineq(m.var(), llc::EQ);
+    TRACE("nla_solver", _().print_lemma(tout); );
+}
+
+bool intervals::get_lemma_for_lower(const monomial& m, const interval& a) {
+    if (m_vars_pushed_up[m.var()] > 10)
+        return false;
+    lp::impq lb(rational(a.m_lower));
+    if (m_config.lower_is_open(a))
+        lb.y = 1;
+
+    lp::impq v(val(m.var()));        
+    if (v < lb) {
+        m_vars_pushed_up[m.var()] = m_vars_pushed_up[m.var()] + 1;
+        interval signs_a = mul_signs_with_deps(m.vars());
+        add_empty_lemma();
+        svector<lp::constraint_index> expl;
+        m_dep_manager.linearize(signs_a.m_lower_dep, expl); 
+        _().current_expl().add_expl(expl);
+        llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE;
+        mk_ineq(m.var(), cmp,  lb.x);
+        TRACE("nla_solver", _().print_lemma(tout); );
+        return true;
+    }
+    return false;
+}
+
+bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) {
+    if (m_vars_pushed_down[m.var()] > 10)
+        return false;
+    lp::impq ub(rational(a.m_upper));
+    if (m_config.upper_is_open(a))
+        ub.y = 1;
+    lp::impq v(val(m.var()));
+    if (v > ub) {
+        m_vars_pushed_down[m.var()] = m_vars_pushed_down[m.var()] + 1;
+        interval signs_a = mul_signs_with_deps(m.vars());
+        add_empty_lemma();
+        svector<lp::constraint_index> expl;
+        m_dep_manager.linearize(signs_a.m_upper_dep, expl); 
+        _().current_expl().add_expl(expl);
+        llc cmp = m_config.upper_is_open(a)? llc::LT: llc::LE;
+        mk_ineq(m.var(), cmp,  ub.x);
+        TRACE("nla_solver", _().print_lemma(tout); );
+        return true;
+    }
+    return false;
+}
+bool intervals::get_lemma(monomial const& m) {
+    interval  b, c, d;
+    interval a = mul(m.vars());
+    if (m_imanager.is_zero(a)) {
+        get_lemma_for_zero_interval(m);
+        return true;
+    }
+    if (!m_imanager.lower_is_inf(a)) {
+        return get_lemma_for_lower(m, a);
+    }
+
+    if (!m_imanager.upper_is_inf(a)) {
+        return get_lemma_for_upper(m, a);
+    }
+    return false;
+} 
+void intervals::set_var_interval(lpvar v, interval& b) const {
+    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);
+    }
+    else {
+        m_config.set_lower_is_open(b, true);
+        m_config.set_lower_is_inf(b, true);
+    }
+    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);
+    }
+    else {
+        m_config.set_upper_is_open(b, true);
+        m_config.set_upper_is_inf(b, true);
+    }
+}
+
+rational sign(const rational& v) { return v.is_zero()? v : (rational(v.is_pos()? 1 : -1)); }
+
+void intervals::set_var_interval_signs(lpvar v, interval& b) const {
+    lp::constraint_index ci;
+    rational val;
+    bool is_strict;
+    if (ls().has_lower_bound(v, ci, val, is_strict)) {            
+        m_config.set_lower(b, sign(val));
+        m_config.set_lower_is_open(b, is_strict);
+        m_config.set_lower_is_inf(b, false);
+    }
+    else {
+        m_config.set_lower_is_open(b, true);
+        m_config.set_lower_is_inf(b, true);
+    }
+    if (ls().has_upper_bound(v, ci, val, is_strict)) {
+        m_config.set_upper(b, sign(val));
+        m_config.set_upper_is_open(b, is_strict);
+        m_config.set_upper_is_inf(b, false);
+    }
+    else {
+        m_config.set_upper_is_open(b, true);
+        m_config.set_upper_is_inf(b, true);
+    }
+}
+
+void intervals::set_var_interval_signs_with_deps(lpvar v, interval& b) const {
+    lp::constraint_index ci;
+    rational val;
+    bool is_strict;
+    if (ls().has_lower_bound(v, ci, val, is_strict)) {            
+        m_config.set_lower(b, sign(val));
+        m_config.set_lower_is_open(b, is_strict);
+        m_config.set_lower_is_inf(b, false);
+        b.m_lower_dep = mk_dep(ci);
+    }
+    else {
+        m_config.set_lower_is_open(b, true);
+        m_config.set_lower_is_inf(b, true);
+        b.m_lower_dep = nullptr;
+    }
+    if (ls().has_upper_bound(v, ci, val, is_strict)) {
+        m_config.set_upper(b, sign(val));
+        m_config.set_upper_is_open(b, is_strict);
+        m_config.set_upper_is_inf(b, false);
+        b.m_upper_dep = mk_dep(ci);
+    }
+    else {
+        m_config.set_upper_is_open(b, true);
+        m_config.set_upper_is_inf(b, true);
+        b.m_upper_dep = nullptr;
+    }
+}
+    
+intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {
+    return m_dep_manager.mk_leaf(ci);
+}
+    
+lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
+    const monomial& m = m_core->emons()[j];
+    interval a = mul(m.vars());
+    SASSERT(!m_imanager.upper_is_inf(a));
+    auto r = lp::impq(a.m_upper);
+    if (a.m_upper_open)
+        r.y = -1;
+    TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";);
+    return r;
+}
+lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
+    const monomial& m = m_core->emons()[j];
+    interval a = mul(m.vars());
+    SASSERT(!a.m_lower_inf);    
+    auto r = lp::impq(a.m_lower);
+    if (a.m_lower_open)
+        r.y = 1;
+    TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";);
+    return r;
+}
+
+std::ostream& intervals::display(std::ostream& out, const interval& i) const {
+    if (m_imanager.lower_is_inf(i)) {
+        out << "(-oo";
+    } else {
+        out << (m_imanager.lower_is_open(i)? "(":"[") << rational(m_imanager.lower(i));        
+    }
+    out << ",";
+    if (m_imanager.upper_is_inf(i)) {
+        out << "oo)";
+    } else {
+        out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");         
+    }
+    return out;
+}
+
+
+intervals::interval intervals::mul(const svector<lpvar>& vars) const {
+    interval a;
+    m_imanager.set(a, mpq(1));
+    
+    for (lpvar j : vars) {
+        interval b, c;
+        set_var_interval(j, b);
+        if (m_imanager.is_zero(b)) {
+            return b;
+        }
+        m_imanager.mul(a, b, c);
+        m_imanager.set(a, c);
+    }
+    return a;
+}
+
+intervals::interval intervals::mul_signs(const svector<lpvar>& vars) const {
+    interval a;
+    m_imanager.set(a, mpq(1));
+    
+    for (lpvar j : vars) {
+        interval b, c;
+        set_var_interval_signs(j, b);
+        if (m_imanager.is_zero(b)) {
+            return b;
+        }
+        m_imanager.mul(a, b, c);
+        m_imanager.set(a, c);
+    }
+    return a;
+}
+
+bool intervals::product_has_upper_bound(int sign, const svector<lpvar>& vars) const {
+    interval a = mul_signs(vars);
+    SASSERT(sign == 1 || sign == -1);
+    return sign == 1 ? !m_imanager.upper_is_inf(a) : !m_imanager.lower_is_inf(a);
+}
+
+bool intervals::monomial_has_lower_bound(lpvar j) const {
+    const monomial& m = m_core->emons()[j];
+    return product_has_upper_bound(-1, m.vars());
+}
+
+bool intervals::monomial_has_upper_bound(lpvar j) const {
+    const monomial& m = m_core->emons()[j];
+    return product_has_upper_bound(1, m.vars());
+}
+lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
+
+const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
+
+std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
+    out << "interv expl:\n ";
+    for (auto ci : expl)
+        m_core->m_lar_solver.print_constraint_indices_only(ci, out);
+    return out;
+}
+
+void intervals::get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const {
+    interval a = mul_signs_with_deps(m_core->emons()[j].vars());
+    m_dep_manager.linearize(a.m_upper_dep, expl);
+    TRACE("nla_intervals", print_explanations(expl, tout););
+}
+void intervals::get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const{
+    interval a = mul_signs_with_deps(m_core->emons()[j].vars());
+    m_dep_manager.linearize(a.m_lower_dep, expl);    
+    TRACE("nla_intervals", print_explanations(expl, tout););
+    //    return m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl ) 
+}
+void intervals::push() {
+    m_vars_pushed_up.push();
+    m_vars_pushed_down.push();
+}
+void intervals::pop(unsigned k) {
+    m_vars_pushed_up.pop(k);
+    m_vars_pushed_down.pop(k);
+}
+
+void intervals::init() {
+    SASSERT(m_vars_pushed_down.size() == m_vars_pushed_up.size());
+    unsigned n = c().m_lar_solver.number_of_vars();
+    while (m_vars_pushed_up.size() < n) {
+        m_vars_pushed_up.push_back(0);
+        m_vars_pushed_down.push_back(0);
+    }
+}
+}
+
+// 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
new file mode 100644
index 000000000..a720183f9
--- /dev/null
+++ b/src/math/lp/nla_intervals.h
@@ -0,0 +1,191 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#pragma once
+#include "util/dependency.h"
+#include "util/small_object_allocator.h"
+#include "math/lp/nla_common.h"
+#include "math/lp/lar_solver.h"
+#include "math/interval/interval.h"
+
+
+namespace nla {
+class core;
+
+class intervals : common {
+    // fields to throttle the propagation on intervals
+    lp::stacked_vector<unsigned> m_vars_pushed_up;
+    lp::stacked_vector<unsigned> m_vars_pushed_down;
+
+    class ci_value_manager {
+    public:
+        void inc_ref(lp::constraint_index const & v) {
+        }
+
+        void dec_ref(lp::constraint_index const & v) {
+        }
+    };
+
+    struct ci_dependency_config {
+        typedef ci_value_manager        value_manager;
+        typedef small_object_allocator  allocator;
+        static const bool ref_count = false;
+        typedef lp::constraint_index value;
+    };
+        
+    typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
+
+    typedef ci_dependency_manager::dependency ci_dependency;
+
+    class im_config {
+        unsynch_mpq_manager&        m_manager;
+        ci_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;
+            ci_dependency * m_lower_dep; // justification for the lower bound
+            ci_dependency * m_upper_dep; // justification for the upper bound
+        };
+
+
+        void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const {
+            ci_dependency* lo = mk_dependency(a, b, deps.m_lower_deps);
+            ci_dependency* hi = mk_dependency(a, b, deps.m_upper_deps);
+            i.m_lower_dep = lo;
+            i.m_upper_dep = hi;
+        }
+            
+        // 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_zero(interval const & a) const {
+            return 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, ci_dependency_manager& d):m_manager(m), m_dep_manager(d) {}
+    private:
+        ci_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const {
+            ci_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;
+        }
+    };
+
+    small_object_allocator      m_alloc;
+    ci_value_manager            m_val_manager;
+    unsynch_mpq_manager         m_num_manager;
+    mutable ci_dependency_manager       m_dep_manager;
+    im_config                   m_config;
+    mutable interval_manager<im_config> m_imanager;
+    region                      m_region;
+
+public:
+    typedef interval_manager<im_config>::interval interval;
+private:
+    void set_var_interval(lpvar v, interval & b) const;
+
+    void set_var_interval_signs(lpvar v, interval & b) const;
+
+    void set_var_interval_signs_with_deps(lpvar v, interval & b) const;
+
+    ci_dependency* mk_dep(lp::constraint_index ci) const;
+
+    lp::lar_solver& ls();
+    const lp::lar_solver& ls() const;
+public:
+    intervals(core* c, reslimit& lim) :
+        common(c),
+        m_alloc("intervals"),
+        m_dep_manager(m_val_manager, m_alloc),
+        m_config(m_num_manager, m_dep_manager),
+        m_imanager(lim, im_config(m_num_manager, m_dep_manager))
+    {}
+    bool get_lemmas();
+    bool get_lemma(monomial const& m);
+    void get_lemma_for_zero_interval(monomial const& m);
+    bool get_lemma_for_lower(monomial const& m, const interval& );
+    bool get_lemma_for_upper(monomial const& m, const interval &);
+    bool monomial_has_lower_bound(lpvar j) const;
+    bool monomial_has_upper_bound(lpvar j) const;
+    bool product_has_upper_bound(int sign, const svector<lpvar>&) const;
+    lp::impq get_upper_bound_of_monomial(lpvar j) const;
+    lp::impq get_lower_bound_of_monomial(lpvar j) const;
+    interval mul(const svector<lpvar>&) const;
+    interval mul_signs(const svector<lpvar>&) const;
+    interval mul_signs_with_deps(const svector<lpvar>&) const;
+    void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
+    void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
+    std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
+    void push();
+    void pop(unsigned k);
+    void init();
+    std::ostream& display(std::ostream& out, const intervals::interval& i) const;
+};
+
+} // end of namespace nla