Skip to content
Open
Show file tree
Hide file tree
Changes from 43 commits
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
d8abd04
Initial plan
Copilot Feb 9, 2026
ac1bef0
mpz: use pointer tagging to save space (#8447)
nunoplopes Feb 9, 2026
cb3b860
Fix syntax errors in mpz.h
Copilot Feb 9, 2026
6faaf86
Implement proper bounds checking for small integers based on platform…
Copilot Feb 9, 2026
b8ed45b
Revert deallocation in set methods and restore indentation in gcd fun…
Copilot Feb 9, 2026
4dc74e2
Fix undefined behavior in SMALL_INT_MAX/MIN constants by using unsign…
Copilot Feb 9, 2026
dcfeb55
Add assertion to set() method and simplify get_sign_cell by removing …
Copilot Feb 9, 2026
5edef9e
Remove nonsensical assertion and revert to simpler shift for SMALL_IN…
Copilot Feb 9, 2026
76dde47
Fix uses of value() that should be value64() for 64-bit small integers
Copilot Feb 10, 2026
a5e1fa9
Fix more uses of value() that should use value64() for 64-bit correct…
Copilot Feb 13, 2026
10c82a3
Fix machine_div2k to not truncate when result doesn't fit in small (a…
Copilot Feb 13, 2026
9bf691f
Refactor decompose function and consolidate value()/value64() into si…
Copilot Feb 13, 2026
cd699ca
Fix remaining int truncation issues in is_power_of_two, power_of_two_…
Copilot Feb 13, 2026
4941ef1
Fix undefined behavior when negating SMALL_INT_MIN in power_of_two_mu…
Copilot Feb 13, 2026
227e48c
Fix SMALL_BITS constant reference to use direct calculation instead
Copilot Feb 13, 2026
45f5209
Add out-of-line definitions for static constexpr members to fix ODR v…
Copilot Feb 13, 2026
8562788
fixes
nunoplopes Feb 15, 2026
10f986e
fix
nunoplopes Feb 15, 2026
67ce05c
fix
nunoplopes Feb 15, 2026
1c5cbcb
fix
nunoplopes Feb 15, 2026
9448f67
fix
nunoplopes Feb 15, 2026
88242fb
fix
nunoplopes Feb 15, 2026
5f429d1
fix
nunoplopes Feb 15, 2026
8ce362a
fix
nunoplopes Feb 15, 2026
e9556c4
fix
nunoplopes Feb 15, 2026
92158ac
fix
nunoplopes Feb 15, 2026
4cdbe22
fix
nunoplopes Feb 15, 2026
dad012a
fix
nunoplopes Feb 15, 2026
0a22332
fix
nunoplopes Feb 15, 2026
bd993ca
fix
nunoplopes Feb 15, 2026
ac748d9
fix
nunoplopes Feb 15, 2026
1a189eb
fix
nunoplopes Feb 15, 2026
fa73827
fixes
nunoplopes Feb 15, 2026
04f07fe
Fix invalid zero representation in set_big_i64 and set_big_ui64
Copilot Feb 15, 2026
957ba91
Revert "Fix invalid zero representation in set_big_i64 and set_big_ui64"
Copilot Feb 16, 2026
cc7902a
Fix set_big_i64/set_big_ui64 zero handling: zero is always represente…
Copilot Feb 16, 2026
c01062e
Revert "Fix set_big_i64/set_big_ui64 zero handling: zero is always re…
Copilot Feb 16, 2026
4a8aeb0
fixes
nunoplopes Feb 17, 2026
6db067c
fixes
nunoplopes Feb 17, 2026
fdc5793
fixes
nunoplopes Feb 17, 2026
e6607df
fixes
nunoplopes Feb 17, 2026
dcf81a2
Start resolving merge conflicts with master branch
Copilot Jul 15, 2026
468a1cb
Merge master branch and resolve conflicts
Copilot Jul 15, 2026
685ca67
Fix Windows ARM64 overflow detection build
Copilot Jul 15, 2026
c1c01b4
Refine MSVC ARM64 multiplication overflow fallback
Copilot Jul 15, 2026
20bba3e
Potential fix for pull request finding
NikolajBjorner Jul 15, 2026
4c8c511
Document MSVC ARM64 magnitude extraction
Copilot Jul 15, 2026
e22487e
Fix MSVC mul_overflows sign extension check
Copilot Jul 15, 2026
b778291
Clarify fallback and unsupported compiler error
Copilot Jul 15, 2026
a972537
Handle ARM64EC in MSVC mul_overflows path
Copilot Jul 15, 2026
e3cfa56
Polish MSVC overflow fallback implementation
Copilot Jul 15, 2026
3b28cc9
Clarify MSVC target-specific overflow paths
Copilot Jul 15, 2026
efd31bd
Fix x86 Windows build by guarding _mul128 to x64 only
Copilot Jul 15, 2026
96128e5
Fix mpz self-assignment in set
Copilot Jul 15, 2026
2fd3a28
Handle mpz shared-self assignment in set
Copilot Jul 15, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/math/polynomial/polynomial.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ Module Name:
#include "util/ref_buffer.h"
#include "util/common_msgs.h"
#include <memory>
#include <numeric>

namespace polynomial {

Expand Down Expand Up @@ -2687,7 +2688,7 @@ namespace polynomial {
}
if (j == 1 || j == -1)
return;
g = u_gcd(abs(j), g);
g = std::gcd(abs(j), g);
if (g == 1)
return;
}
Expand Down
4 changes: 2 additions & 2 deletions src/sat/smt/pb_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Module Name:
--*/

#include <cmath>
#include "util/mpz.h"
#include <numeric>
#include "sat/sat_types.h"
#include "sat/smt/pb_solver.h"
#include "sat/smt/euf_solver.h"
Expand Down Expand Up @@ -1250,7 +1250,7 @@ namespace pb {
g = coeff;
}
else {
g = u_gcd(g, coeff);
g = std::gcd(g, coeff);
}
}

Expand Down
4 changes: 2 additions & 2 deletions src/smt/theory_pb.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ Module Name:
#include "ast/rewriter/pb_rewriter_def.h"
#include "math/simplex/sparse_matrix_def.h"
#include "math/simplex/simplex_def.h"

#include <numeric>

namespace smt {

Expand Down Expand Up @@ -1788,7 +1788,7 @@ namespace smt {
g = static_cast<unsigned>(coeff);
}
else {
g = u_gcd(g, static_cast<unsigned>(coeff));
g = std::gcd(g, static_cast<unsigned>(coeff));
}
}
if (g >= 2) {
Expand Down
Loading
Loading