From ffa8ef4cee0a4da543015511a15a9690b3356c6a Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 27 Jan 2026 11:46:28 -0800
Subject: [PATCH] Refactor pb_rewriter to use structured bindings for
 expression/coefficient pairs (#8380)

* Initial plan

* Refactor pb_rewriter to use C++17 structured bindings

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>
---
 src/ast/rewriter/pb_rewriter.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
index 4ecf3c774..4f7de21b0 100644
--- a/src/ast/rewriter/pb_rewriter.cpp
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -251,11 +251,11 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
         rational slack(0);
         m_args.reset();
         m_coeffs.reset();
-        for (auto const& kv : vec) {
-            m_args.push_back(kv.first);
-            m_coeffs.push_back(kv.second);
-            SASSERT(kv.second.is_pos());
-            slack += kv.second;
+        for (auto const& [e, coeff] : vec) {
+            m_args.push_back(e);
+            m_coeffs.push_back(coeff);
+            SASSERT(coeff.is_pos());
+            slack += coeff;
             all_unit &= m_coeffs.back().is_one();
         }
         if (is_eq) {