diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 5ad79cd84..7240d60e8 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -71,9 +71,9 @@ namespace euf {
     enode_bool_pair egraph::insert_table(enode* p) {
         TRACE(euf_verbose, tout << "insert_table " << bpp(p) << "\n");
         //SASSERT(!m_table.contains_ptr(p));
-        auto rc = m_table.insert(p);
-        p->m_cg = rc.first;
-        return rc;
+        auto [cg, comm] = m_table.insert(p);
+        p->m_cg = cg;
+        return {cg, comm};
     }
 
     void egraph::erase_from_table(enode* p) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 65a81d2e1..f2b0c0c9a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -653,8 +653,7 @@ namespace smt {
                 }
             }
             if (parent->is_cgc_enabled()) {
-                enode_bool_pair pair = m_cg_table.insert(parent);
-                enode * parent_prime = pair.first;
+                auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
                 if (parent_prime == parent) {
                     SASSERT(parent);
                     SASSERT(parent->is_cgr());
@@ -665,7 +664,6 @@ namespace smt {
                 parent->m_cg = parent_prime;
                 SASSERT(!m_cg_table.contains_ptr(parent));
                 if (parent_prime->m_root != parent->m_root) {
-                    bool used_commutativity = pair.second;
                     TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
                           << " used_commutativity: " << used_commutativity << "\n";);
                     push_new_congruence(parent, parent_prime, used_commutativity);
@@ -972,8 +970,8 @@ namespace smt {
                     (parent == cg ||           // parent was root of the congruence class before and after the merge
                      !congruent(parent, cg)    // parent was root of the congruence class before but not after the merge
                      )) {
-                    enode_bool_pair p = m_cg_table.insert(parent);
-                    parent->m_cg = p.first;
+                    auto [parent_cg, used_commutativity] = m_cg_table.insert(parent);
+                    parent->m_cg = parent_cg;
                 }
             }
         }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 578a1956e..90e7686eb 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1028,11 +1028,9 @@ namespace smt {
             }
             else {
                 if (cgc_enabled) {
-                    enode_bool_pair pair = m_cg_table.insert(e);
-                    enode * e_prime      = pair.first;
+                    auto [e_prime, used_commutativity] = m_cg_table.insert(e);
                     if (e != e_prime) {
                         e->m_cg = e_prime;
-                        bool used_commutativity = pair.second;
                         push_new_congruence(e, e_prime, used_commutativity);
                     }
                     else {