diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 51d23fc8b..e368e137b 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -101,8 +101,8 @@ void theory_seq::add_consequence(bool uses_eq, expr_ref_vector const& clause) {
     linearize(dep, eqs, lits);
     for (auto& lit : lits)
         lit.neg();
-    for (auto eq : eqs)
-        lits.push_back(~mk_eq(eq.first->get_expr(), eq.second->get_expr(), false));
+    for (auto const& [n1, n2] : eqs)
+        lits.push_back(~mk_eq(n1->get_expr(), n2->get_expr(), false));
     for (auto f : clause)
         lits.push_back(mk_literal(f));    
     add_axiom(lits);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 94dcc2e34..a578b553d 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -201,9 +201,9 @@ namespace smt {
                 js->get_antecedents(*this);
             }
             while (!m_todo_eqs.empty()) {
-                enode_pair p = m_todo_eqs.back();
+                auto [n1, n2] = m_todo_eqs.back();
                 m_todo_eqs.pop_back();
-                eq2literals(p.first, p.second);
+                eq2literals(n1, n2);
             }
             if (m_todo_js_qhead == m_todo_js.size()) {
                 m_antecedents = nullptr;
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index a1a2b249e..51e7c7192 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -487,8 +487,8 @@ namespace smt {
             fmls.push_back(n);
         }
         for (unsigned i = 0; i < num_eq_antecedents; ++i) {
-            enode_pair const & p = eq_antecedents[i];
-            n = m.mk_eq(p.first->get_expr(), p.second->get_expr());
+            auto const& [n1, n2] = eq_antecedents[i];
+            n = m.mk_eq(n1->get_expr(), n2->get_expr());
             fmls.push_back(n);
         }
         if (x && y) {
@@ -697,7 +697,8 @@ namespace smt {
     }
 
     std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {
-        return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n";
+        auto const& [n1, n2] = p.p;
+        return out << enode_pp(n1, p.ctx) << " = " << enode_pp(n2, p.ctx) << "\n";
     }
 
     void context::log_stats() {
diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp
index 43e3349fd..2431eeaa8 100644
--- a/src/smt/smt_justification.cpp
+++ b/src/smt/smt_justification.cpp
@@ -321,26 +321,27 @@ namespace smt {
         region& r = ctx.get_region();
         m_eqs = new (r) enode_pair[num_eqs];
         std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs);
-        DEBUG_CODE({
+        DEBUG_CODE(
             for (unsigned i = 0; i < num_eqs; ++i) {
-                SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root());
+                enode_pair const & [n1, n2] = eqs[i];
+                SASSERT(n1->get_root() == n2->get_root());
             }
-        });
+        );
     }
 
     void ext_simple_justification::get_antecedents(conflict_resolution & cr) {
         simple_justification::get_antecedents(cr);
         for (unsigned i = 0; i < m_num_eqs; ++i) {
-            enode_pair const & p = m_eqs[i];
-            cr.mark_eq(p.first, p.second);
+            auto const& [n1, n2] = m_eqs[i];
+            cr.mark_eq(n1, n2);
         }
     }
 
     bool ext_simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) {
         bool visited = simple_justification::antecedent2proof(cr, result);
         for (unsigned i = 0; i < m_num_eqs; ++i) {
-            enode_pair const & p = m_eqs[i];
-            proof * pr = cr.get_proof(p.first, p.second);
+            auto const& [n1, n2] = m_eqs[i];
+            proof * pr = cr.get_proof(n1, n2);
             if (pr == nullptr)
                 visited = false;
             else