mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

remove unncesseray checks in get_freedom_interval_for_column()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-12-05 09:57:58 -08:00
parent ad98c2df8e
commit 6770ed85e3
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/int_solver.cpp
View file

@ -365,8 +365,6 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
m = lcm(m, denominator(a));
if (!inf_l && !inf_u) {
if (l > u)
break;
if (l == u)
continue;
}
@ -384,7 +382,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i]));
}
}
VERIFY(l <= zero_of_type<impq>() && zero_of_type<impq>() <= u);
l += xj;
u += xj;
@ -399,7 +397,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
tout << "val = " << get_value(j) << "\n";
tout << "return " << (inf_l || inf_u || l <= u);
);
return (inf_l || inf_u || l <= u);
return true;
}