check for v1 == v2

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Nov 12, 2021 · 3c16edc · 3c16edc
1 parent 63ac2ee
commit 3c16edc
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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);