diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 2288cfbee7..ddf6ae516f 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -283,6 +283,8 @@ namespace nla { } bool monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) { + if (c().val(m.var()) == k * c().val(w)) + return false; vector> coeffs; coeffs.push_back({-k, w}); coeffs.push_back({rational::one(), m.var()});