From 72b4c2258c345f5448fe6f8ba6d21df1dda775af Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 5 Feb 2026 19:02:39 +0000
Subject: [PATCH] Fix all build warnings with surgical changes

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/muz/rel/udoc_relation.cpp | 1 -
 src/smt/dyn_ack.cpp           | 4 ++--
 src/smt/smt_context.cpp       | 2 +-
 src/smt/theory_lra.cpp        | 2 +-
 src/util/vector.h             | 7 +++++++
 5 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index dbda7611f..068af24b6 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -282,7 +282,6 @@ namespace datalog {
         return false;
     }
     unsigned udoc_plugin::num_sort_bits(sort* s) const {
-        unsigned num_bits = 0;
         if (bv.is_bv_sort(s))
             return bv.get_bv_size(s);
         if (m.is_bool(s)) 
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 1c66427e2..932b70019 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -357,7 +357,7 @@ namespace smt {
         m_context.m_stats.m_num_del_dyn_ack++;
         app_pair p((app*)nullptr,(app*)nullptr);
         if (m_clause2app_pair.find(cls, p)) {
-            auto [a1, a2] = p;
+            [[maybe_unused]] auto [a1, a2] = p;
             SASSERT(a1 && a2);
             m_instantiated.erase(p);
             m_clause2app_pair.erase(cls);
@@ -366,7 +366,7 @@ namespace smt {
         }
         app_triple tr(0,0,0);
         if (m_triple.m_clause2apps.find(cls, tr)) {
-            auto [a1, a2, a3] = tr;
+            [[maybe_unused]] auto [a1, a2, a3] = tr;
             SASSERT(a1 && a2 && a3);
             m_triple.m_instantiated.erase(tr);
             m_triple.m_clause2apps.erase(cls);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 185a830d8..ff4f5b964 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2408,7 +2408,7 @@ namespace smt {
        \warning This method will not invoke reset_cache_generation.
     */
     unsigned context::pop_scope_core(unsigned num_scopes) {
-        unsigned units_to_reassert_lim;
+        unsigned units_to_reassert_lim = 0;
 
         try {
             if (m.has_trace_stream() && !m_is_auxiliary)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 545191a66..b3b2afce4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3446,7 +3446,7 @@ public:
             break;
         }
         case equality_source: {
-            auto [n1, n2] = m_equalities[idx];
+            [[maybe_unused]] auto [n1, n2] = m_equalities[idx];
             SASSERT(n1 != nullptr);
             SASSERT(n2 != nullptr);
             m_eqs.push_back(m_equalities[idx]);          
diff --git a/src/util/vector.h b/src/util/vector.h
index ad2802e92..8932a789c 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -405,7 +405,14 @@ public:
         if (CallDestructors) {
             back().~T(); 
         }
+#if defined(__GNUC__) && !defined(__clang__)
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Warray-bounds"
+#endif
         reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--; 
+#if defined(__GNUC__) && !defined(__clang__)
+#pragma GCC diagnostic pop
+#endif
     }
 
     vector& push_back(T const & elem) {