diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 21e01e88a..9541edc60 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1203,7 +1203,7 @@ namespace lp { p.coeff() /= g; } m_sum_of_fixed[ei] = c_g; - // e.m_l *= (1 / g); + // e.m_l /= g for (auto& p : m_l_matrix.m_rows[ei]) { p.coeff() /= g; } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 5ed17be01..8efff27bd 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -132,7 +132,6 @@ struct statistics { unsigned m_offset_eqs = 0; unsigned m_fixed_eqs = 0; unsigned m_dio_calls = 0; - unsigned m_dio_normalize_conflicts = 0; unsigned m_dio_tighten_conflicts = 0; unsigned m_dio_branch_iterations= 0; unsigned m_dio_branching_depth = 0; @@ -176,7 +175,6 @@ struct statistics { st.update("arith-nra-calls", m_nra_calls); st.update("arith-bounds-improvements", m_nla_bounds_improvements); st.update("arith-dio-calls", m_dio_calls); - st.update("arith-dio-normalize-conflicts", m_dio_normalize_conflicts); st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts); st.update("arith-dio-branch-iterations", m_dio_branch_iterations); st.update("arith-dio-branch-depths", m_dio_branching_depth);