From 553f19ca0577505700302b8154db6522c745a177 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Aug 2026 06:40:54 +0000
Subject: [PATCH] Fix assertion violation in lp_bound_propagator when column
 has non-zero delta

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/math/lp/lp_bound_propagator.h | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 3df2fbf741..4ee29a8efc 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -74,7 +74,7 @@ private:
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
-        if (!only_one_nfixed(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
+        if (!only_one_nfixed(r2, v2) || ival(v1) != ival(v2) || is_int(v1) != is_int(v2)) {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
@@ -331,6 +331,12 @@ public:
         if (column_is_fixed(v_j)) {
             return;
         }
+        // the columns registered in the fixed tables have a zero infinitesimal part,
+        // so v_j cannot be equal to any of them when its delta part is not zero
+        if (!ival(v_j).y.is_zero()) {
+            try_add_equation_with_internal_fixed_tables(row_index);
+            return;
+        }
         unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
             try_add_equation_with_internal_fixed_tables(row_index);