Fix tagged pointer small integer bounds for 32/64-bit platforms by Copilot · Pull Request #8554 · Z3Prover/z3

Copilot · 2026-02-09T14:57:03Z

Fix mpz_tagged_ptr branch issues

Issues Fixed:

Implementation Complete:

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

nunoplopes · 2026-02-09T15:47:56Z

@copilot revert your fix to void set(int v). For performance reasons, setting a value should not deallocate memory. Once an mpz becomes large, it stays large forever.

nunoplopes · 2026-02-09T15:49:15Z

@copilot also, revert your massive changes to indentation. It makes the diff very hard to read.

Copilot · 2026-02-09T16:10:42Z

@copilot revert your fix to void set(int v). For performance reasons, setting a value should not deallocate memory. Once an mpz becomes large, it stays large forever.

Reverted. Set methods now only write to small integers when the mpz is already small. Once an mpz becomes large, it stays large. Fixed in d3572a9.

Copilot · 2026-02-09T16:10:46Z

@copilot also, revert your massive changes to indentation. It makes the diff very hard to read.

Reverted. Restored the original else { block structure in gcd function to maintain indentation. Fixed in d3572a9.

nunoplopes · 2026-02-09T17:58:51Z

    }

+    void set(int v) {
+        m_value = static_cast<uintptr_t>(static_cast<intptr_t>(v)) << 1;


@copilot you removed the memory leak fix that was here.
Once a value becomes large, it should stay large forever (and not leak memory like this).

@copilot Oh, I see it is only called if is_small() holds. Add an assertion then.

Added assertion to set() method to ensure it's only called when is_small() holds. Fixed in 46bc45d.

nunoplopes · 2026-02-09T18:02:20Z

-            if (a.value() == INT_MIN) {
+            int64_t val = a.value64();
+            cell = reserve;
+            if (val == mpz::SMALL_INT_MIN) {


@copilot this case doesn't seem to be needed

Removed the SMALL_INT_MIN special case. The generic negative case handles it correctly since we use uint64_t for abs_val. Fixed in 46bc45d.

nunoplopes · 2026-02-09T18:13:00Z

 template<bool SYNCH>
 void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
-    static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch");
+    static_assert(sizeof(int) == sizeof(int), "size mismatch");


@copilot this assert doesn't make sense anymore

Removed the nonsensical assertion sizeof(int) == sizeof(int). This was a bug from the mpz_tagged_ptr refactoring that compared int to itself instead of checking m_val. Fixed in f2ae873.

nunoplopes · 2026-02-09T18:14:41Z

    // Maximum and minimum values that can be stored as small integers
-    static constexpr int64_t SMALL_INT_MAX = (static_cast<int64_t>(1) << (SMALL_BITS - 1)) - 1;
-    static constexpr int64_t SMALL_INT_MIN = -(static_cast<int64_t>(1) << (SMALL_BITS - 1));
+    // Use unsigned arithmetic to avoid undefined behavior on left shift


@copilot revert this. I was wrong, you do 1 << 62, which doesn't overflow

Reverted to simpler shift. You're correct - 1 << 62 doesn't overflow, only 63+ would. Fixed in f2ae873.

nunoplopes · 2026-02-10T22:24:23Z

@copilot fix the CI error:

ASSERTION VIOLATION
File: ../src/util/mpz.cpp
Line: 1139
!is_small(a1)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB, Invoke (L)LDB
de-Morgan example

Copilot · 2026-02-10T22:47:25Z

@copilot fix the CI error:
ASSERTION VIOLATION

...

Fixed. The issue was in LEHMER_GCD algorithm which used value() (returns int) instead of value64() for small integers. On 64-bit platforms where small integers can exceed INT_MAX, this caused truncation and incorrect GCD computation. Also fixed similar issues in mlog2, bitwise_or, and bitwise_and functions. Fixed in 2f9e558.

NikolajBjorner · 2026-07-15T04:12:22Z

@copilot resolve the merge conflicts in this pull request

- Resolved conflict in src/test/memory.cpp: Accept const qualifier on catch - Resolved conflict in src/util/mpz.h: Keep HEAD's 64-bit digit handling - Resolved conflict in src/util/mpz.cpp: Combine ptr() method with fdiv fix - Resolved conflict in src/util/mpz.cpp: Adapt hash function for 64-bit values

Copilot · 2026-07-15T04:37:56Z

@copilot resolve the merge conflicts in this pull request

Resolved all merge conflicts with master branch in commit 468a1cb:

Conflicts resolved:

src/test/memory.cpp: Accepted const qualifier on exception handler
src/util/mpz.h: Kept tagged pointer's 64-bit digit handling logic
src/util/mpz.cpp: Combined ptr() method with master's mpz_fdiv_r_2exp fix from PR Fix GMP bit-vector modulo semantics causing signed BV unsoundness and invalid SMT2 numerals #9899
src/util/mpz.cpp: Adapted hash function to avoid undefined behavior with 64-bit values

Verification:

✅ Build passes successfully
✅ All 92 unit tests pass

The PR is now up to date with the latest master branch.

Copilot

Pull request overview

This PR refactors Z3’s mpz small-integer/tagged-pointer representation to correctly respect 32-bit vs 64-bit bounds, while also modernizing several low-level integer utilities (power-of-two, log2, GCD/trailing-zeros) to use C++20 <bit> and <numeric> helpers. The changes touch core arithmetic infrastructure (mpz, rational) and several downstream users that relied on previous helpers.

Changes:

Rework mpz storage to a tagged uintptr_t encoding (small values vs pointer), and standardize small-value extraction via value(): int64_t.
Replace custom bit/gcd helpers with std::has_single_bit, std::bit_width, std::countr_zero, and std::gcd, updating downstream call sites.
Extend rational with int64_t/uint64_t constructors and assignment support.

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/util/util.h	Switch power-of-two and `log2` helpers to C++20 `<bit>` primitives and add 64-bit overloads.
src/util/util.cpp	Remove legacy `log2`/`uint64_log2` implementations now provided inline in the header.
src/util/rational.h	Add 64-bit constructors and `operator=` overload routing through `int64_t`.
src/util/mpz.h	Introduce tagged-pointer `mpz` representation, new small-int bounds, and inline `trailing_zeros` via `<bit>`.
src/util/mpz.cpp	Update arithmetic ops to use `int64_t value()` and `std::gcd`; add overflow-checked small multiplication fast-path.
src/smt/theory_pb.cpp	Replace `u_gcd` with `std::gcd` and include `<numeric>`.
src/sat/smt/pb_solver.cpp	Replace `u_gcd` with `std::gcd`, include `<numeric>`, and drop now-unneeded `util/mpz.h` include.
src/math/polynomial/polynomial.cpp	Replace `u_gcd` with `std::gcd` and include `<numeric>`.

+#elif defined(_MSC_VER)
+    // MSVC _mul128 intrinsic
+    __int64 high;
+    result = _mul128(a, b, &high);
+    // Overflow if high bits are not the sign extension of result


        else {
-            big_set(target, source);
+            set(*source.ptr(), target, source.sign(), size(source));
        }


Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot AI assigned Copilot and nunoplopes Feb 9, 2026

Copilot started work on behalf of nunoplopes February 9, 2026 14:57 View session

Copilot AI changed the title ~~[WIP] Fix bug and optimize tagged pointer for size integers~~ Fix tagged pointer small integer bounds for 32/64-bit platforms Feb 9, 2026

Copilot AI requested a review from nunoplopes February 9, 2026 15:50

Copilot finished work on behalf of nunoplopes February 9, 2026 15:50

Copilot started work on behalf of nunoplopes February 9, 2026 15:50 View session

Copilot finished work on behalf of nunoplopes February 9, 2026 16:11

Copilot started work on behalf of nunoplopes February 9, 2026 17:55 View session

nunoplopes reviewed Feb 9, 2026

View reviewed changes

Comment thread src/util/mpz.h

nunoplopes reviewed Feb 9, 2026

View reviewed changes

Comment thread src/util/mpz.cpp

Copilot AI requested a review from nunoplopes February 9, 2026 18:12

Copilot finished work on behalf of nunoplopes February 9, 2026 18:12

Copilot started work on behalf of nunoplopes February 9, 2026 18:13 View session

nunoplopes reviewed Feb 9, 2026

View reviewed changes

Copilot AI requested a review from nunoplopes February 9, 2026 18:31

Copilot finished work on behalf of nunoplopes February 9, 2026 18:31

Copilot started work on behalf of nunoplopes February 9, 2026 18:31 View session

Copilot finished work on behalf of nunoplopes February 9, 2026 18:50

Copilot started work on behalf of nunoplopes February 10, 2026 22:24 View session

Copilot finished work on behalf of nunoplopes February 10, 2026 22:48

Copilot started work on behalf of NikolajBjorner July 15, 2026 04:12 View session

Copilot AI added 2 commits July 15, 2026 04:14

Start resolving merge conflicts with master branch

dcf81a2

Copilot finished work on behalf of NikolajBjorner July 15, 2026 04:38

Copilot AI requested a review from NikolajBjorner July 15, 2026 04:38

NikolajBjorner requested a review from Copilot July 15, 2026 04:50

Copilot started reviewing on behalf of NikolajBjorner July 15, 2026 04:51 View session

Copilot started work on behalf of NikolajBjorner July 15, 2026 04:51 View session

Copilot AI reviewed Jul 15, 2026

View reviewed changes

Fix Windows ARM64 overflow detection build

685ca67

Copilot started work on behalf of NikolajBjorner July 15, 2026 05:14 View session

Copilot AI and others added 2 commits July 15, 2026 05:14

Refine MSVC ARM64 multiplication overflow fallback

c1c01b4

Potential fix for pull request finding

20bba3e

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot started work on behalf of NikolajBjorner July 15, 2026 05:15 View session

Document MSVC ARM64 magnitude extraction

4c8c511

Copilot started work on behalf of NikolajBjorner July 15, 2026 05:22 View session

Copilot AI added 2 commits July 15, 2026 05:36

Fix MSVC mul_overflows sign extension check

e22487e

Clarify fallback and unsupported compiler error

b778291

Copilot finished work on behalf of NikolajBjorner July 15, 2026 05:37

Copilot AI added 3 commits July 15, 2026 05:37

Handle ARM64EC in MSVC mul_overflows path

a972537

Polish MSVC overflow fallback implementation

e3cfa56

Clarify MSVC target-specific overflow paths

3b28cc9

Copilot finished work on behalf of NikolajBjorner July 15, 2026 05:41

Fix x86 Windows build by guarding _mul128 to x64 only

efd31bd

Copilot finished work on behalf of NikolajBjorner July 15, 2026 05:46

Copilot AI added 2 commits July 15, 2026 05:53

Fix mpz self-assignment in set

96128e5

Handle mpz shared-self assignment in set

2fd3a28

Copilot finished work on behalf of NikolajBjorner July 15, 2026 06:13

Uh oh!

Conversation

Copilot AI commented Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Fix mpz_tagged_ptr branch issues

Issues Fixed:

Implementation Complete:

Uh oh!

nunoplopes commented Feb 9, 2026

Uh oh!

nunoplopes commented Feb 9, 2026

Uh oh!

Copilot AI commented Feb 9, 2026

Uh oh!

Copilot AI commented Feb 9, 2026

Uh oh!

Uh oh!

nunoplopes Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

nunoplopes Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

nunoplopes Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

nunoplopes Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

nunoplopes Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 9, 2026

Choose a reason for hiding this comment

Uh oh!

nunoplopes commented Feb 10, 2026

Uh oh!

Copilot AI commented Feb 10, 2026

Uh oh!

NikolajBjorner commented Jul 15, 2026

Uh oh!

Copilot AI commented Jul 15, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Copilot AI commented Feb 9, 2026 •

edited

Loading