mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-21 15:57:35 +00:00
Code Activity
20660 commits 59 branches 58 tags 180 MiB
Commit graph

20660 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
5528eac82e Initial plan 2026-02-18 20:58:08 -08:00
Nikolaj Bjorner
d24561005d update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:08 -08:00
Nikolaj Bjorner
3e54f2328b Update RELEASE_NOTES.md for version 4.15.6 
Added release notes for version 4.15.6, including optimizations and fixes.
 2026-02-18 20:58:08 -08:00
Copilot
0761e91e8f Remove unused swap() methods (#8538) 2026-02-18 20:58:08 -08:00
Lev Nachmanson
f0c3a5bbb6 fix nlsat_explain.cpp that the regression tests would pass with lws=false 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:07 -08:00
copilot-swe-agent[bot]
d3c388a489 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-18 20:58:07 -08:00
copilot-swe-agent[bot]
62bfb13ada Initial plan 2026-02-18 20:58:07 -08:00
Copilot
3a8b688008 Store rational by value in parameter variant (#8518) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Nuno Lopes
e73c897bd4 constructor 2026-02-18 20:58:07 -08:00
Copilot
70626ac914 mpz: use pointer tagging to save space (#8447) 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:07 -08:00
Nuno Lopes
1fa430479f remove redundant assert 2026-02-18 20:58:07 -08:00
Nikolaj Bjorner
29ad07c2e2 version updated on workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:07 -08:00
Nikolaj Bjorner
8672d26bd0 remove obsoleted ADO workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:07 -08:00
Nikolaj Bjorner
ccaa346a46 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:07 -08:00
copilot-swe-agent[bot]
38661f25e4 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-18 20:58:07 -08:00
copilot-swe-agent[bot]
3df140052b Initial plan 2026-02-18 20:58:06 -08:00
Lev Nachmanson
784c510bd5 Revert "optionally throttle patch_basic_columns() especially useful in unsat cases" 
This reverts commit bee2b45743.
 2026-02-18 20:58:06 -08:00
Lev Nachmanson
6351b612fc Revert "try fixed int patch period" 
This reverts commit 3e2027ec11.
 2026-02-18 20:58:06 -08:00
Nikolaj Bjorner
76a60f697c 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-18 20:58:06 -08:00
Nikolaj Bjorner
8725bd757d 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-18 20:58:06 -08:00
copilot-swe-agent[bot]
af5135274d Fix TypeScript compilation error: add updateField to Context interface 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
8af4983863 Add datatype_update_field to C++, Python, TypeScript, and OCaml bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
58c2bfa1bd Initial plan 2026-02-18 20:58:06 -08:00
copilot-swe-agent[bot]
119008b46f Fix all build warnings with surgical changes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
b5407d7302 Initial plan 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
999a92e3e6 Revert prexpr to non-static for debugging availability 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
21fd199062 Add static linkage to internal functions 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-02-18 20:58:05 -08:00
copilot-swe-agent[bot]
ba6cfffcdf Initial plan 2026-02-18 20:58:05 -08:00
Lev Nachmanson
edc2715aa8 try fixed int patch period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:05 -08:00
Copilot
b0b33367ef Add static linkage to inline functions in header files (#8519) 2026-02-18 20:58:05 -08:00
Lev Nachmanson
99bb57cb25 optionally throttle patch_basic_columns() especially useful in unsat cases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:58:05 -08:00
Nikolaj Bjorner
840688a290 Update a3-rust verifier documentation: correct artifact references and descriptions 2026-02-18 20:58:05 -08:00
Nikolaj Bjorner
fad7daecd0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:05 -08:00
Copilot
adf72f2a66 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-18 20:58:05 -08:00
copilot-swe-agent[bot]
ff7898ef7c Fix JSDoc formatting and improve type safety in tests 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
185a639027 Document Loop function semantics and fix review comments 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
6d3fe721b7 Add comprehensive tests for regex functionality 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
38ad7d2265 Add regex support to TypeScript API - types and implementations 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
b56e50f081 Initial plan 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
edca1ed5c3 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-18 20:58:04 -08:00
copilot-swe-agent[bot]
5c72c5c1e0 Initial plan 2026-02-18 20:58:04 -08:00
Nikolaj Bjorner
a4eb59aaba Delete examples/c++/test_move_context.cpp 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
1bd67d99c9 Remove debug test file 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
bc9ebb3a15 Add move semantics to z3::context class 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
993db98d17 Initial plan 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
4cb12f94a3 Update code-simplifier to create discussions with git diffs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:04 -08:00
copilot-swe-agent[bot]
bc31aafaa5 Initial plan 2026-02-18 20:58:03 -08:00
Nikolaj Bjorner
b5154a0924 Add agentic workflow code-simplifier 2026-02-18 20:58:03 -08:00
Nikolaj Bjorner
d1efd3416b updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:58:03 -08:00
Copilot
73f6dae095 Refactor mk_concat call sites to use std::initializer_list (#8494) 
* Initial plan

* Refactor mk_concat call sites to use std::initializer_list

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

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-18 20:58:03 -08:00