From e0f978f7cdf0a6eebefd3c3a3ed97314ff6d31de Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Jul 2026 09:43:32 -0700
Subject: [PATCH] omit adding rows for affine relations if it is true in the
 current model

---
 src/math/lp/monomial_bounds.cpp | 2 ++
 1 file changed, 2 insertions(+)

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<std::pair<lp::mpq, unsigned>> coeffs;        
         coeffs.push_back({-k, w});
         coeffs.push_back({rational::one(), m.var()});