fix overflow in mpz::bitwise_not

Z3Prover · Dec 9, 2022 · a96f5a9 · a96f5a9
1 parent c6f9c09
commit a96f5a9
Showing 1 changed file with 5 additions and 3 deletions.
diff --git 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;