mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity
20591 commits 50 branches 56 tags 170 MiB
Commit graph

20591 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
b13784b3e0 Revert "Fix memory leak in mpz pointer tagging implementation" 
This reverts commit 64d5544a32.

As explained by @NikolajBjorner, the original implementation intentionally
did NOT free memory on set() calls. This was a performance optimization to
avoid reallocating memory when the mpz cell needs large numbers again later.

The deallocate() calls introduced in the previous commit would cause
performance regressions, particularly in code paths like Simplex that
frequently reset values.

The actual memory leak must be in the original pointer tagging commit
(2f4abe2ce6) and needs to be fixed there
rather than by adding deallocate() calls in set() methods.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 23:08:31 +00:00
copilot-swe-agent[bot]
64d5544a32 Fix memory leak in mpz pointer tagging implementation 
The memory leak was caused by mpz_manager::set() methods that would
directly overwrite the m_value field when setting small values, without
first deallocating any existing large value. This resulted in leaked
memory when transitioning from large to small integers.

Fixed by adding deallocate() calls before setting small values in:
- set(mpz& target, mpz const& source)
- set(mpz& a, int val)
- set(mpz& a, uint64_t val)
- set_i64(mpz& c, int64_t v)

The deallocate() method safely handles the case when the value is already
small (it's a no-op in that case), so this fix is safe for all scenarios.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-08 22:44:28 +00:00
copilot-swe-agent[bot]
58df141825 Initial plan 2026-02-08 21:58:22 +00: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
Nikolaj Bjorner
3f5810a365
Merge pull request #8531 from Z3Prover/copilot/fix-build-warnings-again 
Fix MSVC C4267 warnings in initializer_list overloads
 2026-02-07 18:45:52 -08:00
Lev Nachmanson
f5b8dfc2f1 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases" 
This reverts commit bee2b45743.
 2026-02-07 10:45:15 -10:00
Lev Nachmanson
73696725e4 Revert "try fixed int patch period" 
This reverts commit 3e2027ec11.
 2026-02-07 10:45:15 -10:00
copilot-swe-agent[bot]
8b42b190a0 Fix build warnings: cast size_t to unsigned in arith_decl_plugin.h and bv_decl_plugin.h 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-07 19:49:28 +00:00
copilot-swe-agent[bot]
c2603cc449 Initial plan 2026-02-07 19:32:17 +00:00
Nikolaj Bjorner
013172d25c
Update RELEASE_NOTES.md for version 4.15.5 
Removed several outdated features and added new functionalities across various APIs, including improvements for TypeScript, Java, and C++ bindings. Updated release notes for version 4.15.5 to reflect these changes.
 2026-02-07 10:42:23 -08:00
Nikolaj Bjorner
f322e3b795
Update RELEASE_NOTES with new features and fixes 
Added numerous enhancements and fixes including migration to GitHub Actions, new API features, optimizations, and bug fixes.
 2026-02-07 10:39:01 -08:00
Nikolaj Bjorner
3bd5b5a5d4
Merge pull request #8500 from Z3Prover/copilot/update-functional-datatype 
Add datatype_update_field to C++, Python, TypeScript, and OCaml bindings
 2026-02-07 10:11:54 -08:00
Nikolaj Bjorner
8978f1549b
Merge pull request #8509 from Z3Prover/copilot/fix-build-warnings 
Fix compiler warnings: unused variables, uninitialized variable, and false positive array bounds
 2026-02-07 05:10:02 -08:00
Nikolaj Bjorner
f26f570ec7
Merge pull request #8521 from Z3Prover/copilot/add-static-linkage-functions 
Add static linkage to file-local function
 2026-02-07 05:08:00 -08:00
copilot-swe-agent[bot]
eced186d1f Revert prexpr to non-static for debugging availability 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-07 09:35:28 +00:00
Lev Nachmanson
3e2027ec11 try fixed int patch period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-06 14:40:04 -10:00
copilot-swe-agent[bot]
52885a4d62 Add static linkage to internal functions 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-06 23:19:16 +00:00
copilot-swe-agent[bot]
5bf3ed2a17 Initial plan 2026-02-06 22:58:50 +00:00
Copilot
3095ab511f
Add static linkage to inline functions in header files (#8519) 2026-02-06 22:57:51 +00:00
Lev Nachmanson
bee2b45743 optionally throttle patch_basic_columns() especially useful in unsat cases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-06 10:14:39 -10:00
Nikolaj Bjorner
f6a1d87e32 Update a3-rust verifier documentation: correct artifact references and descriptions 2026-02-06 19:45:05 +00:00
Nikolaj Bjorner
0f30ae2f90 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-06 11:24:39 -08:00
copilot-swe-agent[bot]
decb0fffc1 Fix TypeScript compilation error: add updateField to Context interface 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-06 17:27:19 +00:00
Copilot
bb35267e46
Modern C++: Add std::span overload for mk_or, adopt std::clamp, optimize stream output (#8507) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-06 11:54:06 +00:00