mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

check for integrality when adding an equality

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-19 13:15:50 -07:00
parent c4fbe05a96
commit 115ae8fe14
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -356,6 +356,7 @@ public:
if (table.find(val(v), k)) {
TRACE("cheap_eq", tout << "found k " ; k->print(tout) << "\n";);
if (k->column() != v->column() &&
is_int(k->column()) == is_int(v->column()) &&
!is_equal(k->column(), v->column()))
report_eq(k, v);
} else {