mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

another memory managment leak fix. Relates to different leak exposed by #3997

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 12:58:42 -07:00
parent 44957894ea
commit f76c6424f2
2 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/interval/dep_intervals.h
View file

@ -297,11 +297,9 @@ public:
void del(interval& i) { m_imanager.del(i); } void del(interval& i) { m_imanager.del(i); }
template <enum with_deps_t wd> interval intersect(const interval& a, const interval& b) const { template <enum with_deps_t wd> void intersect(const interval& a, const interval& b, interval& i) const {
interval i;
update_lower_for_intersection<wd>(a, b, i); update_lower_for_intersection<wd>(a, b, i);
update_upper_for_intersection<wd>(a, b, i); update_upper_for_intersection<wd>(a, b, i);
return i;
} }
template <enum with_deps_t wd> template <enum with_deps_t wd>

7
src/math/lp/nla_intervals.cpp
View file

@ -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); SASSERT(e.is_sum() && e.size() > 1);
scoped_dep_interval i_from_term(get_dep_intervals()); scoped_dep_interval i_from_term(get_dep_intervals());
if (interval_from_term<wd>(e, i_from_term)) { if (interval_from_term<wd>(e, i_from_term)) {
interval r = m_dep_intervals.intersect<wd>(a, i_from_term); scoped_dep_interval r(get_dep_intervals());
m_dep_intervals.intersect<wd>(a, i_from_term, r);
TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";); TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";);
if (m_dep_intervals.is_empty(r)) { 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; T expl;
if (conflict_u_l(a, i_from_term)) { if (conflict_u_l(a, i_from_term)) {
get_dep_intervals().linearize(a.get().m_upper_dep, expl); 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 { } 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); get_dep_intervals().linearize(a.get().m_lower_dep, expl);
} }
f(expl); f(expl);