mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-14 21:01:49 +00:00
Code Activity
20611 commits 53 branches 57 tags 174 MiB
Commit graph

20611 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
5305b438be Add out-of-line definitions for static constexpr members to fix ODR violations 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 19:34:13 +00:00
copilot-swe-agent[bot]
7654ab4b72 Fix SMALL_BITS constant reference to use direct calculation instead 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 18:24:50 +00:00
copilot-swe-agent[bot]
23fe87612a Fix undefined behavior when negating SMALL_INT_MIN in power_of_two_multiple 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 16:48:50 +00:00
copilot-swe-agent[bot]
f9ec57947c Fix remaining int truncation issues in is_power_of_two, power_of_two_multiple, and log2 for 64-bit platforms 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 15:47:46 +00:00
copilot-swe-agent[bot]
a4e58b1547 Refactor decompose function and consolidate value()/value64() into single value() returning int64_t 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 14:10:48 +00:00
copilot-swe-agent[bot]
ded37fa012 Fix machine_div2k to not truncate when result doesn't fit in small (add assertion instead) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 13:48:38 +00:00
copilot-swe-agent[bot]
5c61d08dc1 Fix more uses of value() that should use value64() for 64-bit correctness 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-13 12:35:47 +00:00
copilot-swe-agent[bot]
2f9e5581e2 Fix uses of value() that should be value64() for 64-bit small integers 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-10 22:47:15 +00:00
copilot-swe-agent[bot]
f2ae873fde Remove nonsensical assertion and revert to simpler shift for SMALL_INT constants 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 18:49:20 +00:00
copilot-swe-agent[bot]
46bc45d904 Add assertion to set() method and simplify get_sign_cell by removing redundant SMALL_INT_MIN case 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 18:30:29 +00:00
copilot-swe-agent[bot]
940910efb6 Fix undefined behavior in SMALL_INT_MAX/MIN constants by using unsigned arithmetic 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 18:11:53 +00:00
copilot-swe-agent[bot]
d3572a95b9 Revert deallocation in set methods and restore indentation in gcd function 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 16:08:58 +00:00
copilot-swe-agent[bot]
cd492c3e9c Implement proper bounds checking for small integers based on platform pointer size 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 15:38:31 +00:00
copilot-swe-agent[bot]
6e545ac56a Fix syntax errors in mpz.h 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-09 15:16:45 +00:00
copilot-swe-agent[bot]
7ed69045bc Merge branch 'mpz_tagged_ptr' into copilot/fix-tagged-pointer-bug 2026-02-09 14:59:43 +00:00
copilot-swe-agent[bot]
552eef2027 Initial plan 2026-02-09 14:57:02 +00:00
Nuno Lopes
50a63500c1 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
 2026-02-09 14:54:27 +00:00
Nikolaj Bjorner
feabb3ae2e update readme with workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-08 20:25:36 -08:00
Nikolaj Bjorner
3251ccdfd5 update release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-08 20:11:41 -08:00
Nikolaj Bjorner
2330e1419d update release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-08 20:10:43 -08:00
Nikolaj Bjorner
212e8735fb update to next version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-08 19:52:43 -08:00
Lev Nachmanson
dd09603f4d fix the logic of adding all coefficients and blocking double insertions in m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-08 15:01:51 -10:00
Nikolaj Bjorner
c269421942 Revert "mpz: use pointer tagging to save space (#8447)" 
This reverts commit 2f4abe2ce6.
 2026-02-08 14:48:21 -08:00
Nikolaj Bjorner
a1cab09c1c
Merge pull request #8547 from Z3Prover/copilot/update-readme-status-badges 
Remove non-existent ocaml-all.yaml badge from README Build status table
 2026-02-08 13:37:12 -08:00
copilot-swe-agent[bot]
5aa18e0af6 Remove OCaml Build badge from README status table 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 21:36:09 +00:00
copilot-swe-agent[bot]
5db87bc4bf Initial plan 2026-02-08 21:34:24 +00:00
Nikolaj Bjorner
45fd779621
Merge pull request #8541 from Z3Prover/copilot/update-nightly-build-test-process 
Add macOS dylib headerpad fix and CI validation
 2026-02-08 12:43:45 -08:00
Nikolaj Bjorner
85534f154d update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-08 12:42:35 -08:00
Nikolaj Bjorner
1799e6b8a3
Update RELEASE_NOTES.md for version 4.15.6 
Added release notes for version 4.15.6, including optimizations and fixes.
 2026-02-08 11:32:01 -08:00
Nikolaj Bjorner
8eff8dc9c8
Merge branch 'master' into copilot/update-nightly-build-test-process 2026-02-08 11:28:21 -08:00
Nikolaj Bjorner
8c3aefca93
Delete .github/workflows/README-macos-headerpad.md 2026-02-08 11:25:40 -08:00
Copilot
c0be7ac621
Remove unused swap() methods (#8538) 2026-02-08 18:53:43 +00:00
Lev Nachmanson
56db8d5e98 fix nlsat_explain.cpp that the regression tests would pass with lws=false 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-08 08:40:49 -10:00
copilot-swe-agent[bot]
e685ea45ed Fix OCaml linker flag and align validation runners with build runners 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:26:30 +00:00
copilot-swe-agent[bot]
34d2d08364 Fix CMake variable name and clarify test path documentation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:24:18 +00:00
copilot-swe-agent[bot]
af76ac69d6 Apply headerpad fix to build systems (Python and CMake) and fix validation test paths 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:23:04 +00:00
copilot-swe-agent[bot]
406e99b0d2 Fix install_name_tool command and runner consistency in validation jobs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:19:57 +00:00
copilot-swe-agent[bot]
40c0b0cdb2 Add documentation for macOS headerpad validation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:17:17 +00:00
copilot-swe-agent[bot]
8d404f6b87 Add macOS dylib headerpad validation to nightly and release workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 17:16:32 +00:00
Nikolaj Bjorner
72564da251
Merge pull request #8535 from Z3Prover/copilot/fix-install-name-tool-issue 
Add -headerpad_max_install_names to all macOS dylib builds
 2026-02-08 09:13:57 -08:00
copilot-swe-agent[bot]
f48716f3b5 Initial plan 2026-02-08 17:13:32 +00:00
Copilot
47897d6fb6
Store rational by value in parameter variant (#8518) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-08 12:17:13 +00:00
Nuno Lopes
6ed5b6d667 constructor 2026-02-08 11:56:00 +00:00
Copilot
2f4abe2ce6
mpz: use pointer tagging to save space (#8447) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-08 11:55:14 +00:00
Nuno Lopes
3a4f1fd65a remove redundant assert 2026-02-08 11:27:17 +00:00
Nikolaj Bjorner
bc388672c1 version updated on workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-07 19:32:42 -08:00
copilot-swe-agent[bot]
a08e8a99f9 Add -headerpad_max_install_names flag for macOS dylib builds 
This fixes the install_name_tool issue on macOS where the tool fails
with "larger updated load commands do not fit". The linker flag
-Wl,-headerpad_max_install_names ensures sufficient header padding
in the Mach-O binary for install_name_tool to modify install names.

Changes made:
- CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin
- Python build: Changed flag from ML-only to all macOS builds
- OCaml CMake: Added flag to OCaml stublib build on APPLE

Fixes #7623 (regression in 4.15.5)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 03:26:13 +00:00
copilot-swe-agent[bot]
f988e76da6 Initial plan 2026-02-08 03:21:20 +00:00
Nikolaj Bjorner
c89c01dedf remove obsoleted ADO workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-07 18:48:38 -08:00
Nikolaj Bjorner
0ed85db8a2 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-07 18:47:15 -08:00