diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index fce8086a0..d146671ac 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -161,10 +161,12 @@ interv horner::interval_of_mul(const nex& e) { TRACE("nla_horner_details", tout << "got zero\n"; ); return b; } - TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals.display(tout, b); ); + TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << ", "; m_intervals.display(tout, b); ); interv c; m_intervals.mul(a, b, c, comb_rule); - m_intervals.combine_deps(a, b, comb_rule, a); + m_intervals.combine_deps(a, b, comb_rule, c); + TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a) << "\n";); + TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c) << "\n";); m_intervals.set(a, c); TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a) << "\n";); } @@ -195,7 +197,7 @@ interv horner::interval_of_sum(const nex& e) { interval_deps_combine_rule combine_rule; TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";); m_intervals.add(a, b, c, combine_rule); - m_intervals.combine_deps(a, b, combine_rule, a); + m_intervals.combine_deps(a, b, combine_rule, c); m_intervals.set(a, c); TRACE("nla_horner_details_sum", tout << es[k] << ", "; m_intervals.display(tout, a); tout << "\n";); diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index e63b00bbe..50c5d0f0a 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -86,7 +86,7 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const { if (m_imanager.upper_is_inf(i)) { out << "oo)"; } else { - out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]"); + out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]"); } svector expl; m_dep_manager.linearize(i.m_lower_dep, expl); diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 348fc8abc..e60884fcb 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -174,9 +174,14 @@ public: void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); } void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); } void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } - void set(interval& a, const interval& b) { m_imanager.set(a, b); } + void set(interval& a, const interval& b) { + m_imanager.set(a, b); + a.m_lower_dep = b.m_lower_dep; + a.m_upper_dep = b.m_upper_dep; + } void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); } void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { + SASSERT(&a != &i && &b != &i); m_config.add_deps(a, b, deps, i); }