mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

explain_equal: jumping to root without explanation is wrong

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 11:46:09 +02:00
parent 53dc31989a
commit 08928d041a
1 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -543,6 +543,7 @@ namespace polysat {
void slicing::explain_equal(enode* x, enode* y, ptr_vector<void>& out_deps) { void slicing::explain_equal(enode* x, enode* y, ptr_vector<void>& out_deps) {
SASSERT(is_equal(x, y)); SASSERT(is_equal(x, y));
SASSERT_EQ(width(x), width(y));
enode_vector& xs = m_tmp2; enode_vector& xs = m_tmp2;
enode_vector& ys = m_tmp3; enode_vector& ys = m_tmp3;
SASSERT(xs.empty()); SASSERT(xs.empty());
@ -561,24 +562,22 @@ namespace polysat {
if (rx == ry) if (rx == ry)
explain_class(x, y, out_deps); explain_class(x, y, out_deps);
else { else {
xs.push_back(sub_hi(rx)); xs.push_back(sub_hi(x));
xs.push_back(sub_lo(rx)); xs.push_back(sub_lo(x));
ys.push_back(sub_hi(ry)); ys.push_back(sub_hi(y));
ys.push_back(sub_lo(ry)); ys.push_back(sub_lo(y));
} }
} }
else if (width(x) > width(y)) { else if (width(x) > width(y)) {
enode* const rx = x->get_root(); xs.push_back(sub_hi(x));
xs.push_back(sub_hi(rx)); xs.push_back(sub_lo(x));
xs.push_back(sub_lo(rx));
ys.push_back(y); ys.push_back(y);
} }
else { else {
SASSERT(width(x) < width(y)); SASSERT(width(x) < width(y));
xs.push_back(x); xs.push_back(x);
enode* const ry = y->get_root(); ys.push_back(sub_hi(y));
ys.push_back(sub_hi(ry)); ys.push_back(sub_lo(y));
ys.push_back(sub_lo(ry));
} }
} }
SASSERT(ys.empty()); SASSERT(ys.empty());