From aaf05f18ab1773818209454676592b35fabac0cb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 16 May 2020 15:19:32 -0700 Subject: [PATCH] fix a bug in an simplifying interval expressions with terms Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index ad8c62be0..2eb10801d 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -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));