mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity
20850 commits 65 branches 58 tags 180 MiB
Commit graph

20850 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
05e8e4a37c fix another regression by Nuno's changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:19 -08:00
Lev Nachmanson
24f3cddaac relax a too strong assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 21:02:19 -08:00
copilot-swe-agent[bot]
eef7d12667 Recompile a3-python.md workflow with gh-aw v0.43.2 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:19 -08:00
copilot-swe-agent[bot]
972f90ea88 Initial plan 2026-02-18 21:02:19 -08:00
Nikolaj Bjorner
08eb25e14c Add network permissions to Python workflow 2026-02-18 21:02:19 -08:00
Copilot
62030bfddd Simplify svector assignment operators using = default (#8566) 
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 21:02:19 -08:00
Nikolaj Bjorner
1e7be62bde Delete .github/workflows/README-a3-python.md 2026-02-18 21:02:19 -08:00
copilot-swe-agent[bot]
5400b39118 Add README documentation for a3-python workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:18 -08:00
copilot-swe-agent[bot]
9cd53f1f79 Add a3-python agentic workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:18 -08:00
copilot-swe-agent[bot]
426caf53e5 Initial plan 2026-02-18 21:02:18 -08:00
Nikolaj Bjorner
ba0a33231c Enhance nightly workflow to include Linux builds 
Added support for Linux binaries in the nightly workflow.
 2026-02-18 21:02:18 -08:00
Nikolaj Bjorner
dcd8ea4af2 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:18 -08:00
Nuno Lopes
23a0a529fb revert swap changes to fix CI 2026-02-18 21:02:18 -08:00
dependabot[bot]
25b48a74f8 Bump githubnext/gh-aw from 0.40.0 to 0.42.17 
Bumps [githubnext/gh-aw](https://github.com/githubnext/gh-aw) from 0.40.0 to 0.42.17.
- [Release notes](https://github.com/githubnext/gh-aw/releases)
- [Changelog](https://github.com/github/gh-aw/blob/main/CHANGELOG.md)
- [Commits](https://github.com/githubnext/gh-aw/compare/v0.40.0...v0.42.17)

---
updated-dependencies:
- dependency-name: githubnext/gh-aw
  dependency-version: 0.42.17
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:18 -08:00
dependabot[bot]
2e4a7c7138 Bump github/gh-aw from 0.42.6 to 0.42.17 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.42.6 to 0.42.17.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Changelog](https://github.com/github/gh-aw/blob/main/CHANGELOG.md)
- [Commits](https://github.com/github/gh-aw/compare/v0.42.6...v0.42.17)

---
updated-dependencies:
- dependency-name: github/gh-aw
  dependency-version: 0.42.17
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:18 -08:00
dependabot[bot]
06e6d55346 Bump actions/download-artifact from 6.0.0 to 7.0.0 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 6.0.0 to 7.0.0.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v6...v7)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: 7.0.0
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-18 21:02:18 -08:00
Nikolaj Bjorner
c8cd205207 fix build warnings and scoop up after Nuno's leaks 2026-02-18 21:02:18 -08:00
Nuno Lopes
bbb29911f3 fix crash 2026-02-18 21:02:17 -08:00
Nuno Lopes
9152013fbd remove a few copies 2026-02-18 21:02:17 -08:00
Nuno Lopes
a3e7bbb92f replace some copies with moves 2026-02-18 21:02:17 -08:00
Nikolaj Bjorner
6b28d65487 set random seed directly on m_smt_params before context initialization 
updates to random seed on ctx does not get propagated to arithmetic solver, preventing diversity within arithmetic solver.
 2026-02-18 21:02:17 -08:00
Nuno Lopes
bfc132a4fc move, dont copy 2026-02-18 21:02:17 -08:00
Nuno Lopes
b7bf23c3bb move, dont copy 2026-02-18 21:02:17 -08:00
Nikolaj Bjorner
fc6355cbe2 Update Windows.yml 2026-02-18 21:02:17 -08:00
Copilot
58431ec158 Replace user-defined swap with C++11 move semantics for covert move patterns (#8543) 2026-02-18 21:02:17 -08:00
Nikolaj Bjorner
c50d41a6e8 update readme with workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:16 -08:00
Nikolaj Bjorner
b8cfce92a8 update release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:16 -08:00
Nikolaj Bjorner
2aab7481d9 update release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:16 -08:00
Nikolaj Bjorner
a7dbe1698b update to next version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:16 -08:00
Lev Nachmanson
4c43bf585d fix the logic of adding all coefficients and blocking double insertions in m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 21:02:16 -08:00
Nikolaj Bjorner
0be8deefd3 Revert "mpz: use pointer tagging to save space (#8447)" 
This reverts commit 2f4abe2ce6.
 2026-02-18 21:02:16 -08:00
copilot-swe-agent[bot]
df024760b2 Remove OCaml Build badge from README status table 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:16 -08:00
copilot-swe-agent[bot]
b670727094 Initial plan 2026-02-18 21:02:15 -08:00
Nikolaj Bjorner
1387b2a759 Delete .github/workflows/README-macos-headerpad.md 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
51fd4b2806 Fix OCaml linker flag and align validation runners with build runners 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
3c401f186b Fix CMake variable name and clarify test path documentation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:15 -08:00
copilot-swe-agent[bot]
3ae8d7026a 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-18 21:02:10 -08:00
copilot-swe-agent[bot]
c291c7cf95 Fix install_name_tool command and runner consistency in validation jobs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:08 -08:00
copilot-swe-agent[bot]
2b3afe12a3 Add documentation for macOS headerpad validation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:08 -08:00
copilot-swe-agent[bot]
bde5553815 Add macOS dylib headerpad validation to nightly and release workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 20:58:08 -08:00
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