From 6a572543b43783a02bcb21199718d5f922246126 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 20 Nov 2023 15:54:00 -0800
Subject: [PATCH] n/a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_ac_plugin.cpp |  4 ++--
 src/test/euf_arith_plugin.cpp | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp
index 3bbf2de11..74a98ea59 100644
--- a/src/ast/euf/euf_ac_plugin.cpp
+++ b/src/ast/euf/euf_ac_plugin.cpp
@@ -254,7 +254,7 @@ namespace euf {
             sort(ml);
             sort(mr);
             for (unsigned i = ml.size(); i-- > 0;) {
-                if (ml[i] == mr[i])
+                if (ml[i]->root_id() == mr[i]->root_id())
                     continue;
                 if (ml[i]->root_id() < mr[i]->root_id())
                     std::swap(e.l, e.r);
@@ -480,7 +480,7 @@ namespace euf {
         bool has_two = false;
         for (auto n : m)
             if (n->root->eqs.size() > max_use)
-                max_n = n->root, max_use = n->root->eqs.size(), has_two |= max_n != nullptr;
+                has_two |= max_n && (max_n != n->root), max_n = n->root, max_use = n->root->eqs.size();
         m_eq_occurs.reset();
         for (auto n : m)
             if (n->root != max_n && has_two)
diff --git a/src/test/euf_arith_plugin.cpp b/src/test/euf_arith_plugin.cpp
index 821ea1302..218570854 100644
--- a/src/test/euf_arith_plugin.cpp
+++ b/src/test/euf_arith_plugin.cpp
@@ -45,9 +45,33 @@ static void test1() {
     std::cout << g << "\n";
 }
 
+static void test2() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph g(m);
+    g.add_plugins();
+    arith_util a(m);
+    sort_ref I(a.mk_int(), m);
 
+    expr_ref x(m.mk_const("x", I), m);
+    expr_ref y(m.mk_const("y", I), m);
+    auto* nx = get_node(g, a.mk_add(x, y));
+    auto* ny = get_node(g, a.mk_add(y, x));
+    TRACE("plugin", tout << "before merge\n" << g << "\n");
+    g.merge(nx, get_node(g, x), nullptr);
+    g.merge(ny, get_node(g, y), nullptr);
+
+    TRACE("plugin", tout << "before propagate\n" << g << "\n");
+    g.propagate();
+    TRACE("plugin", tout << "after propagate\n" << g << "\n");
+    SASSERT(get_node(g, x)->get_root() == get_node(g, y)->get_root());
+    g.merge(get_node(g, a.mk_add(x, a.mk_add(y, y))), get_node(g, a.mk_add(y, x)), nullptr);
+    g.propagate();
+    std::cout << g << "\n";
+}
 
 void tst_euf_arith_plugin() {
     enable_trace("plugin");
     test1();
+    test2();
 }