mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix a bug in cheap_eqs with table

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-15 09:56:12 -07:00
parent 09516d74f6
commit f882219081
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lp_bound_propagator.h
View file

@ -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);