From 965db51b5c3f42e9813d0dc1a47f2afbe4314d63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2026 09:56:37 -0700 Subject: [PATCH] use patterns --- src/smt/smt_quantifier.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 68358e3b02..455ea83c74 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -219,9 +219,7 @@ namespace smt { STRACE(triggers, tout <<", Pat: "<< expr_ref(pat, m());); STRACE(causality, tout <<", Father:";); } - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); + for (auto [orig, substituted] : used_enodes) { (void) substituted; if (orig == nullptr) { STRACE(causality, tout << " #" << substituted->get_owner_id();); @@ -260,9 +258,7 @@ namespace smt { log_justification_to_root(out, bindings[i], already_visited, m_context, m()); } - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); + for (auto [orig, substituted] : used_enodes) { if (orig != nullptr) { log_justification_to_root(out, orig, already_visited, m_context, m()); log_justification_to_root(out, substituted, already_visited, m_context, m());