diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d60737b3f..761228075 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1652,8 +1652,8 @@ namespace lp { const auto& row = m_e_matrix.m_rows[ei]; auto it = std::find_if (row.begin(), row.end(), [j](const auto& p) {return p.var() == j;} ); if (it == row.end()) return false; - return it->coeff() == mpq(1)&& j_sign == 1 || - it->coeff() == mpq(-1) && j_sign == -1; + return (it->coeff() == mpq(1) && j_sign == 1) || + (it->coeff() == mpq(-1) && j_sign == -1); } // j is the variable to eliminate, it appears in row ei of m_e_matrix with // a coefficient equal to j_sign which is +-1 diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 39ec1baeb..421859ec0 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -34,7 +34,6 @@ namespace lp { int_solver& lia; lar_solver& lra; lar_core_solver& lrac; - dioph_eq m_dio; unsigned m_number_of_calls = 0; lar_term m_t; // the term to return in the cut bool m_upper; // cut is an upper bound @@ -43,13 +42,14 @@ namespace lp { hnf_cutter m_hnf_cutter; unsigned m_hnf_cut_period; unsigned m_dioph_eq_period; + dioph_eq m_dio; int_gcd_test m_gcd; bool column_is_int_inf(unsigned j) const { return lra.column_is_int(j) && (!lia.value_is_int(j)); } - imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_gcd(lia), m_dio(lia) { + imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) { m_hnf_cut_period = settings().hnf_cut_period(); m_dioph_eq_period = settings().m_dioph_eq_period; }