diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 314d15da9..35e93a7d2 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -838,9 +838,13 @@ namespace polysat { } void slicing::egraph_on_merge(enode* root, enode* other) { - LOG("on_merge: root " << slice_pp(*this, root) << "other " << slice_pp(*this, other)); + LOG("on_merge: root " << slice_pp(*this, root) << " other " << slice_pp(*this, other)); if (root->interpreted()) return; + if (root->is_equality()) { + SASSERT(other->is_equality()); + return; + } SASSERT(!other->interpreted()); // by convention, interpreted nodes are always chosen as root SASSERT(root != other); SASSERT_EQ(root, root->get_root());