diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 92613579a..8cb420ee1 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -239,6 +239,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator &
         int a_sign = is_pos(a)? 1: -1;
         int sign = j_sign * a_sign;
         const ul_pair & ul =  m_columns_to_ul_pairs[j];
+        // todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
         auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
         lp_assert(is_valid(witness));
         bp.consume(a, witness);
diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp
index d8b02e45d..d63b4ff2d 100644
--- a/src/math/lp/lp_bound_propagator.cpp
+++ b/src/math/lp/lp_bound_propagator.cpp
@@ -57,8 +57,9 @@ impq lp_bound_propagator::get_lower_bound(unsigned j) const {
         const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j];
         if (!(m_nla_solver && m_nla_solver->is_monomial_var(j)))
             return l;
-        if (! m_nla_solver->monomial_has_lower_bound(j))
+        if (m_nla_solver->monomial_has_lower_bound(j))
             return std::max(l,  m_nla_solver->get_lower_bound(j));
+        return l;
     }
     return m_nla_solver->get_lower_bound(j);
 }
@@ -67,10 +68,11 @@ impq lp_bound_propagator::get_upper_bound(unsigned j) const {
     lp_assert(upper_bound_is_available(j));
     if (upper_bound_is_available_for_column(j)) {
         const impq& l = m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j];
-        if (!(m_nla_solver && m_nla_solver->is_monomial_var(j)))
+        if (!(m_nla_solver && m_nla_solver->is_monomial_var(j))) 
             return l;
-        if (! m_nla_solver->monomial_has_upper_bound(j))
+        if (m_nla_solver->monomial_has_upper_bound(j))
             return std::min(l, m_nla_solver->get_upper_bound(j));
+        return l;
     }
     return m_nla_solver->get_upper_bound(j);
 }
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 45f65fe66..ff17216d7 100755
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -137,33 +137,44 @@ bool intervals::check(lp::lar_term const& t) {
 }
 
 lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
-    SASSERT(false);
-    throw;
+    const monomial& m = m_core->emons()[j];
+    interval a = mul(1, m.vars());
+    
+    auto r = lp::impq(a.m_upper);
+    if (a.m_upper_open)
+        r.y = -1;
+    return r;
 }
-
 lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
-    SASSERT(false);
-    throw;
+    const monomial& m = m_core->emons()[j];
+    interval a = mul(1, m.vars());
+    
+    auto r = lp::impq(a.m_lower);
+    if (a.m_lower_open)
+        r.y = 1;
+    return r;
 }
 
-bool intervals::product_has_upper_bound(int sign, const svector<lpvar>& vars) const {
+intervals::interval intervals::mul(int sign, const svector<lpvar>& vars) const {
     interval a;
     m_imanager.set(a, rational(sign).to_mpq());
     
     for (lpvar j : vars) {
         interval b, c;
-        set_interval_signs(j, b);
+        set_interval(j, b);
         m_imanager.mul(a, b, c);
         if (m_imanager.is_zero(c)) {
             TRACE("nla_intervals", tout << "sign = " << sign << "\nproduct = ";
                   m_core->print_product_with_vars(vars, tout) << "collapsed to zero\n";);
-            return true;
+            return c;
         }
         m_imanager.set(a, c);
     }
-    TRACE("nla_intervals", tout << "sign = " << sign << "\nproduct = ";
-          m_core->print_product_with_vars(vars, tout) << "has lower bound = " << 
-          !m_imanager.upper_is_inf(a) << "\n";);
+    return a;
+}
+
+bool intervals::product_has_upper_bound(int sign, const svector<lpvar>& vars) const {
+    interval a = mul(sign, vars);
     return !m_imanager.upper_is_inf(a);
 }
 
@@ -174,7 +185,7 @@ bool intervals::monomial_has_lower_bound(lpvar j) const {
 
 bool intervals::monomial_has_upper_bound(lpvar j) const {
     const monomial& m = m_core->emons()[j];
-    return product_has_upper_bound(-1, m.vars());
+    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; }
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index e40ca19e1..819e8fe1d 100755
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -172,5 +172,6 @@ namespace nla {
         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(int sign, const svector<lpvar>&) const;
     };
 } // end of namespace nla