mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 12:25:51 +00:00
Code Activity

fix a bug in an simplifying interval expressions with terms

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-16 15:19:32 -07:00
parent 363690791a
commit aaf05f18ab
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -282,7 +282,7 @@ bool intervals::interval_from_term(const nex& e, scoped_dep_interval& i) {
lp::lar_term norm_t = expression_to_normalized_term(&e.to_sum(), a, b);
lp::explanation exp;
if (m_core->explain_by_equiv(norm_t, exp)) {
set_zero_interval(i);
m_dep_intervals.set_interval_for_scalar(i, b);
if (wd == e_with_deps::with_deps) {
for (auto p : exp) {
i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.second));