From a96f5a9b425b6f5ba7e8ce1c1a75db6683c4bdc9 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 9 Dec 2022 11:59:39 +0000
Subject: [PATCH] fix overflow in mpz::bitwise_not

---
 src/util/mpz.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 9b0da70fcfb..c56ab166794 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1460,9 +1460,11 @@ void mpz_manager<SYNCH>::bitwise_xor(mpz const & a, mpz const & b, mpz & c) {
 template<bool SYNCH>
 void mpz_manager<SYNCH>::bitwise_not(unsigned sz, mpz const & a, mpz & c) {
     SASSERT(is_nonneg(a));
-    if (is_small(a) && sz <= 63) {
-        int64_t mask = (static_cast<int64_t>(1) << sz) - static_cast<int64_t>(1);
-        set_i64(c, (~ i64(a)) & mask);
+    if (is_small(a) && sz <= 64) {
+        uint64_t v = ~get_uint64(a);
+        unsigned zero_out = 64 - sz;
+        v = (v >> zero_out) << zero_out;
+        set(c, v);
     }
     else {
         mpz a1, a2, m, tmp;