From 3c16edc8d3d87e2c4237d2f25e40521996a111ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Nov 2021 09:11:17 -0800
Subject: [PATCH] check for v1 == v2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/lp_bound_propagator.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 58c24f2ca3b..dfe7227e6c0 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -134,7 +134,9 @@ class lp_bound_propagator {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
-
+        if (v1 == v2)
+            return;
+        
         explanation ex;
         explain_fixed_in_row(r1, ex);
         explain_fixed_in_row(r2, ex);