From f8822190818a0e56ec5e24529ca9b12de4172445 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 15 Jun 2020 09:56:12 -0700 Subject: [PATCH] fix a bug in cheap_eqs with table Signed-off-by: Lev Nachmanson --- src/math/lp/lp_bound_propagator.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index bb376dfe4..bd13a6bf1 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -325,8 +325,9 @@ public: if (y == null_lpvar) { // x is an implied fixed var at k. unsigned x2; - if (lp().fixed_var_table().find(k, x2) && !is_equal(x, x2)) { - SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k && is_int(x) == is_int(x2)); + if (lp().fixed_var_table().find(k, x2) && + !is_equal(x, x2) && is_int(x) == is_int(x2)) { + SASSERT(lp().column_is_fixed(x2) && get_lower_bound_rational(x2) == k); explanation ex; constraint_index lc, uc; lp().get_bound_constraint_witnesses_for_column(x2, lc, uc);