From 10c8e3d9e0a9ae3f3bb3c1da07964b3cb32cc15e Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 19 Jun 2026 10:08:51 -0600
Subject: [PATCH] Fix GMP bit-vector modulo semantics causing signed BV
 unsoundness and invalid SMT2 numerals (#9899)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When Z3 is built with GMP, negative bit-vector numerals were normalized
incorrectly, which could make valid BV proofs fail and emit invalid SMT2
constants like `(_ bv-1 64)`. This change restores canonical
modulo-`2^k` behavior for GMP-backed integers and adds a regression that
covers both solver soundness and SMT2 printing.

- **Root cause fix (GMP backend)**
- Updated `mpz_manager::mod2k` in the GMP path to use floor-division
remainder semantics:
    - `mpz_tdiv_r_2exp` → `mpz_fdiv_r_2exp`
- This ensures `mod2k` stays in `[0, 2^k)`, matching BV numeral
invariants expected by normalization and printing code.

- **Regression coverage (API test)**
  - Extended `test_bvneg` to cover the reported case:
    - `x : (_ BitVec 1)`, `sx = sign_extend 63 x`
    - Assert `¬(sx = 0 ∨ sx = -1)` is unsat
- Assert solver SMT2 serialization does not contain malformed negative
BV literals (`"(_ bv-"`)

```cpp
// GMP mod2k path
// before: mpz_tdiv_r_2exp(*result.m_ptr, a1(), k);
// after:
mpz_fdiv_r_2exp(*result.m_ptr, a1(), k);
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/test/api.cpp | 23 +++++++++++++++++++++++
 src/util/mpz.cpp |  2 +-
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/test/api.cpp b/src/test/api.cpp
index a7e7f329b..b1765fdd4 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -81,6 +81,29 @@ void test_bvneg() {
         std::cout << r << "\n";
     }
 
+    {
+        Z3_sort bv1 = Z3_mk_bv_sort(ctx, 1);
+        Z3_sort bv64 = Z3_mk_bv_sort(ctx, 64);
+        Z3_ast x = Z3_mk_fresh_const(ctx, "x", bv1);
+        Z3_ast sx = Z3_mk_sign_ext(ctx, 63, x);
+        Z3_ast zero = Z3_mk_int64(ctx, 0, bv64);
+        Z3_ast minus_one = Z3_mk_int64(ctx, -1, bv64);
+        Z3_ast args[2] = { Z3_mk_eq(ctx, sx, zero), Z3_mk_eq(ctx, sx, minus_one) };
+        Z3_ast claim = Z3_mk_or(ctx, 2, args);
+
+        Z3_solver_push(ctx, s);
+        Z3_solver_assert(ctx, s, Z3_mk_not(ctx, claim));
+        ENSURE(Z3_solver_check(ctx, s) == Z3_L_FALSE);
+        Z3_solver_pop(ctx, s, 1);
+
+        Z3_solver_push(ctx, s);
+        Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, sx, minus_one));
+        std::string smt2 = Z3_solver_to_string(ctx, s);
+        // Bit-vector numerals must print in canonical unsigned SMT2 form.
+        ENSURE(smt2.find("(_ bv-") == std::string::npos);
+        Z3_solver_pop(ctx, s, 1);
+    }
+
     Z3_solver_dec_ref(ctx, s);
     Z3_del_config(cfg);
     Z3_del_context(ctx);    
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 35de2deb0..7fd91404c 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -700,7 +700,7 @@ mpz mpz_manager<SYNCH>::mod2k(mpz const & a, unsigned k) {
     ensure_mpz_t a1(a);
     mk_big(result);
     MPZ_BEGIN_CRITICAL();
-    mpz_tdiv_r_2exp(*result.m_ptr, a1(), k);
+    mpz_fdiv_r_2exp(*result.m_ptr, a1(), k);
     MPZ_END_CRITICAL();
 #endif
     return result;