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

remove an unnecessary if

Browse source
This commit is contained in:
Lev Nachmanson 2023-11-30 08:59:05 -10:00
parent d540d881ef
commit 5784c2da79
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -72,14 +72,13 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
if (t < j_nz) { if (t < j_nz) {
j_nz = t; j_nz = t;
entering_iter = non_basis_iter; entering_iter = non_basis_iter;
if (number_of_benefitial_columns_to_go_over) number_of_benefitial_columns_to_go_over--;
number_of_benefitial_columns_to_go_over--;
n = 1; n = 1;
} }
else if (t == j_nz && this->m_settings.random_next(++n) == 0) { else if (t == j_nz && this->m_settings.random_next(++n) == 0) {
entering_iter = non_basis_iter; entering_iter = non_basis_iter;
} }
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb); }
if (entering_iter == m_non_basis_list.end()) if (entering_iter == m_non_basis_list.end())
return -1; return -1;
unsigned entering = *entering_iter; unsigned entering = *entering_iter;