mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix in init_int_int_set

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2017-07-06 20:46:17 -07:00
parent 0e0e9c7041
commit 9b1b096a16
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/int_solver.cpp
View file

@ -745,7 +745,7 @@ void int_solver::display_column(std::ostream & out, unsigned j) const {
bool int_solver::inf_int_set_is_correct() const { bool int_solver::inf_int_set_is_correct() const {
for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) { for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) {
if (m_inf_int_set.contains(j) != is_int(j) && (!value_is_int(j))) if (m_inf_int_set.contains(j) != (is_int(j) && (!value_is_int(j))))
return false; return false;
} }
return true; return true;
@ -758,7 +758,7 @@ bool int_solver::column_is_int_inf(unsigned j) const {
void int_solver::init_inf_int_set() { void int_solver::init_inf_int_set() {
m_inf_int_set.clear(); m_inf_int_set.clear();
m_inf_int_set.resize(m_lar_solver->A_r().column_count()); m_inf_int_set.resize(m_lar_solver->A_r().column_count());
for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_basis) { for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) {
if (column_is_int_inf(j)) if (column_is_int_inf(j))
m_inf_int_set.insert(j); m_inf_int_set.insert(j);
} }