mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

remove unnecessary assignments

Browse source
This commit is contained in:
Lev Nachmanson 2023-12-18 18:49:27 -10:00
parent 1b7550483e
commit 9a18628b17
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -242,7 +242,6 @@ public:
// gomory will be t >= k and the current solution has a property t < k // gomory will be t >= k and the current solution has a property t < k
m_k = 1; m_k = 1;
m_t.clear(); m_t.clear();
mpq m_f = fractional_part(get_value(m_inf_col));
TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", ";
tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f << "\n";); tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f << "\n";);
lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int());
@ -257,7 +256,6 @@ public:
} }
m_big_number = m_abs_max.expt(2); m_big_number = m_abs_max.expt(2);
#endif #endif
mpq one_min_m_f = 1 - m_f;
for (const auto & p : m_row) { for (const auto & p : m_row) {
unsigned j = p.var(); unsigned j = p.var();
if (j == m_inf_col) { if (j == m_inf_col) {