From 89e2ceffd079d8c2b5cd331b713fad5a360a2ecf Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 31 Jan 2026 17:14:47 -0800 Subject: [PATCH] Use structured bindings for stack entries in theory_datatype (#8442) * Initial plan * Refactor theory_datatype to use C++17 structured bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix structured binding syntax error in smt_justification.cpp Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/smt/theory_datatype.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 81f57862b..c7be4804c 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -975,8 +975,7 @@ namespace smt { // DFS traversal from `n`. Look at top element and explore it. while (!res && !m_stack.empty()) { - stack_op op = m_stack.back().first; - enode * app = m_stack.back().second; + auto [op, app] = m_stack.back(); m_stack.pop_back(); if (oc_cycle_free(app))