mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity
20575 commits 46 branches 56 tags 170 MiB
Commit graph

20575 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
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
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
Nikolaj Bjorner
384a8e291b
Merge pull request #8499 from Z3Prover/copilot/add-regex-support-typescript-api 
Add regex support to TypeScript API
 2026-02-05 23:08:19 -08:00
Nikolaj Bjorner
30dc404163
Merge pull request #8515 from Z3Prover/copilot/change-discussion-to-issue 
[WIP] Change code-simplifier to create a GitHub issue
 2026-02-05 23:06:42 -08:00
copilot-swe-agent[bot]
e54bc3f428 Change code-simplifier to create GitHub issues instead of discussions and set schedule to run once daily at midnight UTC 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-06 07:03:53 +00:00
Nikolaj Bjorner
7d6c809f28
Merge pull request #8508 from Z3Prover/copilot/add-move-constructor-z3-context 
Add move semantics to z3::context
 2026-02-05 23:03:21 -08:00
Nikolaj Bjorner
7584a28252
Delete examples/c++/test_move_context.cpp 2026-02-05 23:01:47 -08:00
copilot-swe-agent[bot]
84f966427c Initial plan 2026-02-06 07:00:21 +00:00
Nikolaj Bjorner
7c66140cc8
Merge pull request #8513 from Z3Prover/copilot/update-code-simplifier-to-github-discussion 
Change code-simplifier to create discussions with git diffs instead of PRs
 2026-02-05 22:47:51 -08:00
copilot-swe-agent[bot]
f2fb33223a Update code-simplifier to create discussions with git diffs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-06 06:45:35 +00:00
copilot-swe-agent[bot]
69ba03106b Initial plan 2026-02-06 06:42:13 +00:00
Nikolaj Bjorner
b6de13d914
Merge pull request #8510 from Z3Prover/add-workflow-.github-workflows-code-simplifier.md-6102 
Add agentic workflow code-simplifier
 2026-02-05 12:33:08 -08:00
Nikolaj Bjorner
772bc28470 Add agentic workflow code-simplifier 2026-02-05 12:32:59 -08:00
Nikolaj Bjorner
1d84545b0c updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-05 12:28:49 -08:00
copilot-swe-agent[bot]
72b4c2258c Fix all build warnings with surgical changes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-05 19:02:39 +00:00
copilot-swe-agent[bot]
ee162695b6 Initial plan 2026-02-05 19:00:35 +00:00
copilot-swe-agent[bot]
ae88f4e159 Remove debug test file 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-05 17:16:20 +00:00
copilot-swe-agent[bot]
6e09a06307 Add move semantics to z3::context class 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-05 17:15:43 +00:00