From 482e4da4d77f04a44e4c592904715a9815da768c Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 23 Oct 2023 15:24:02 +0200
Subject: [PATCH] skip on_merge for equality nodes

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

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());