mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

#5518

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-31 12:50:24 -07:00
parent 535f442655
commit 0b063f7903
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_egraph.cpp
View file

@ -422,6 +422,11 @@ namespace euf {
set_conflict(n1, n2, j); set_conflict(n1, n2, j);
return; return;
} }
if (r1->value() != r2->value() && r1->value() != l_undef && r2->value() != l_undef) {
SASSERT(m.is_bool(r1->get_expr()));
set_conflict(n1, n2, j);
return;
}
if (!r2->interpreted() && if (!r2->interpreted() &&
(r1->class_size() > r2->class_size() || r1->interpreted() || r1->value() != l_undef)) { (r1->class_size() > r2->class_size() || r1->interpreted() || r1->value() != l_undef)) {
std::swap(r1, r2); std::swap(r1, r2);