diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index 55dedf151..8891f495f 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -172,7 +172,10 @@ namespace lp { return false; } - if (least_coeff_is_bounded && !m_least_coeff.is_one() && !ext_gcd_test(A.m_rows[i])) + if (least_coeff_is_bounded && + !m_least_coeff.is_one() && + !lia.get_value(basic_var).is_int() && + !ext_gcd_test(A.m_rows[i])) return false; if (!least_coeff_is_unique)