Fix GMP bit-vector modulo semantics causing signed BV unsoundness and invalid SMT2 numerals (#9899)

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/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;