From ef337f3a3f0a9eb5d5a5bc94c3f8c8f62e71caea Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 20 Jul 2023 17:28:37 +0200
Subject: [PATCH] shortcut in merge

---
 src/math/polysat/slicing.cpp | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index dddfc07ab..4f06f2844 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -581,6 +581,22 @@ namespace polysat {
             enode* y = ys.back();
             xs.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)) {
                 get_base(x, xs);
                 x = xs.back();