From 586a6b893de64113d0e6952d70311685339a9eab Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 18 Jun 2026 19:23:29 +0000
Subject: [PATCH] Fix GMP mod2k sign bug and add BV regression test

---
 src/test/api.cpp | 22 ++++++++++++++++++++++
 src/util/mpz.cpp |  2 +-
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/test/api.cpp b/src/test/api.cpp
index a7e7f329b..8de8d8c06 100644
--- a/src/test/api.cpp
+++ b/src/test/api.cpp
@@ -81,6 +81,28 @@ 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);
+        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;