From a5e1078172dbd8ad3a54ded620d7d250b38955b9 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 13 May 2026 17:24:13 -0400
Subject: [PATCH] Silence GCC false positives in bound propagation and mpz
 sign-cell paths (#9530)

Recent GCC builds report two warning classes in core codepaths: a
possible uninitialized read in `bound_propagator::relevant_bound`, and
repeated `-Warray-bounds` diagnostics in `mpz_manager::get_sign_cell`
when materializing small integers into a reserved `mpz_cell`.

- **Warning cleanup in bound propagation**
- Initialize `interval_size` at declaration in
`src/ast/simplifiers/bound_propagator.cpp` so the compiler can prove
safety across templated `LOWER/UPPER` instantiations using `std::clamp`.
- Preserves existing control flow and refinement heuristics (`bounded`
remains the gate for interval-based logic).

- **Warning cleanup in mpz small-value cell materialization**
- In `src/util/mpz.h`, replace direct writes through `cell->m_digits[0]`
with writes via a derived digits pointer
(`reinterpret_cast<digit_t*>(cell + 1)`), avoiding zero-length
trailing-array indexing diagnostics.
- Keeps memory layout and semantics unchanged for the stack-reserved
`sign_cell` buffer.

- **Representative change**
  ```cpp
  cell = reserve;
  cell->m_size = 1;
  digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
  cell_digits[0] = a.value() < 0 ? -a.value() : a.value();
  ```

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/simplifiers/bound_propagator.cpp | 3 +--
 src/util/mpz.h                           | 5 +++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ast/simplifiers/bound_propagator.cpp b/src/ast/simplifiers/bound_propagator.cpp
index 240ba7a98..a73d81fb8 100644
--- a/src/ast/simplifiers/bound_propagator.cpp
+++ b/src/ast/simplifiers/bound_propagator.cpp
@@ -381,7 +381,7 @@ bool bound_propagator::relevant_bound(var x, double new_k) const {
     if (b == nullptr)
         return true; // variable did not have a bound
     
-    double interval_size;
+    double interval_size = 0.0;
     bool bounded = get_interval_size(x, interval_size);
 
     if (!is_int(x)) {
@@ -939,4 +939,3 @@ void bound_propagator::display(std::ostream & out) const {
 }
 
 
-
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 505bb177e..7b714b9be 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -314,13 +314,14 @@ class mpz_manager {
             else {
                 cell = reserve;
                 cell->m_size = 1;
+                digit_t* cell_digits = reinterpret_cast<digit_t*>(cell + 1);
                 if (a.value() < 0) {
                     sign = -1;
-                    cell->m_digits[0] = -a.value();
+                    cell_digits[0] = -a.value();
                 }
                 else {
                     sign = 1;
-                    cell->m_digits[0] = a.value();
+                    cell_digits[0] = a.value();
                 }
             }
         }