mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

shortcut in merge

Browse source
This commit is contained in:
Jakob Rath 2023-07-20 17:28:37 +02:00
parent 3e23742bcf
commit ef337f3a3f
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/slicing.cpp
View file

@ -581,6 +581,22 @@ namespace polysat {
enode* y = ys.back(); enode* y = ys.back();
xs.pop_back(); xs.pop_back();
ys.pop_back(); ys.pop_back();
if (x == y)
continue;
if (x->get_root() == y->get_root()) {
DEBUG_CODE({
// parents merged => base slices merged
enode_vector x_base;
enode_vector y_base;
get_base(x, x_base);
get_base(y, y_base);
SASSERT_EQ(x_base.size(), y_base.size());
for (unsigned i = x_base.size(); i-- > 0; ) {
SASSERT_EQ(x_base[i]->get_root(), y_base[i]->get_root());
}
});
continue;
}
if (has_sub(x)) { if (has_sub(x)) {
get_base(x, xs); get_base(x, xs);
x = xs.back(); x = xs.back();