From c5e08f0444317a338b51097c394807fd09d1542b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 8 Apr 2020 15:46:41 -0700 Subject: [PATCH] add dependencies lost in case of an empty intersection Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 7806a1db6..4477fed15 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -350,6 +350,7 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const if(! interval_of_sum_no_term(e, a, f)) { return false; } + TRACE("nla_intervals_details", tout << "a = "; display(tout, a);); if (e.is_a_linear_term()) { SASSERT(e.is_sum() && e.size() > 1); scoped_dep_interval i_from_term(get_dep_intervals()); @@ -363,6 +364,8 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const T expl; get_dep_intervals().linearize(r.m_upper_dep, expl); get_dep_intervals().linearize(r.m_lower_dep, expl); + get_dep_intervals().linearize(a.get().m_upper_dep, expl); + get_dep_intervals().linearize(a.get().m_lower_dep, expl); f(expl); } else { // need to recalculate the interval with dependencies @@ -372,7 +375,6 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const return false; } m_dep_intervals.set(a, r); - } } return true;