mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

fix column patching

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-07 13:39:32 -08:00
parent f45e17c47e
commit 6b01376f51
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -759,7 +759,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";);
if (!a.is_int())
if (column_is_int(i) && !a.is_int())
m = lcm(m, denominator(a));
}
TRACE("random_update", tout << "m = " << m << "\n";);