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 58c24f2ca..dfe7227e6 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);