mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

use only scoped intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-02 12:05:11 -07:00
parent cf3f06ee26
commit b45311cc7c
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

@ -367,7 +367,7 @@ void intervals::interval_of_mul(const nex_mul& e, scoped_dep_interval& a) {
scoped_dep_interval b(get_dep_intervals()); scoped_dep_interval b(get_dep_intervals());
interval_of_expr<wd>(ep.e(), ep.pow(), b); interval_of_expr<wd>(ep.e(), ep.pow(), b);
TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); ); TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); );
interval c; scoped_dep_interval c(get_dep_intervals());
if (wd == e_with_deps::with_deps) { if (wd == e_with_deps::with_deps) {
interval_deps_combine_rule comb_rule; interval_deps_combine_rule comb_rule;
m_dep_intervals.mul(a, b, c, comb_rule); m_dep_intervals.mul(a, b, c, comb_rule);