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

add dependencies lost in case of an empty intersection

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-08 15:46:41 -07:00
parent 4621767968
commit c5e08f0444
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -350,6 +350,7 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const
if(! interval_of_sum_no_term<wd>(e, a, f)) { if(! interval_of_sum_no_term<wd>(e, a, f)) {
return false; return false;
} }
TRACE("nla_intervals_details", tout << "a = "; display(tout, a););
if (e.is_a_linear_term()) { if (e.is_a_linear_term()) {
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());
@ -363,6 +364,8 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const
T expl; T expl;
get_dep_intervals().linearize(r.m_upper_dep, expl); get_dep_intervals().linearize(r.m_upper_dep, expl);
get_dep_intervals().linearize(r.m_lower_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); f(expl);
} else { } else {
// need to recalculate the interval with dependencies // 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; return false;
} }
m_dep_intervals.set<wd>(a, r); m_dep_intervals.set<wd>(a, r);
} }
} }
return true; return true;