From 6b01376f51ed91dde5daa20d2465cc76f19175c0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 7 Feb 2020 13:39:32 -0800 Subject: [PATCH] fix column patching Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index f658553ea..ff0bb4d44 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -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";);