diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index 9d0f69882..fa294c9ba 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -297,11 +297,9 @@ public: void del(interval& i) { m_imanager.del(i); } - template interval intersect(const interval& a, const interval& b) const { - interval i; + template void intersect(const interval& a, const interval& b, interval& i) const { update_lower_for_intersection(a, b, i); update_upper_for_intersection(a, b, i); - return i; } template diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 4d131b798..53917390b 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -375,7 +375,8 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const SASSERT(e.is_sum() && e.size() > 1); scoped_dep_interval i_from_term(get_dep_intervals()); if (interval_from_term(e, i_from_term)) { - interval r = m_dep_intervals.intersect(a, i_from_term); + scoped_dep_interval r(get_dep_intervals()); + m_dep_intervals.intersect(a, i_from_term, r); TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";); if (m_dep_intervals.is_empty(r)) { @@ -384,9 +385,9 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const T expl; if (conflict_u_l(a, i_from_term)) { get_dep_intervals().linearize(a.get().m_upper_dep, expl); - get_dep_intervals().linearize(r.m_lower_dep, expl); + get_dep_intervals().linearize(r.get().m_lower_dep, expl); } else { - get_dep_intervals().linearize(r.m_upper_dep, expl); + get_dep_intervals().linearize(r.get().m_upper_dep, expl); get_dep_intervals().linearize(a.get().m_lower_dep, expl); } f(expl);