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

20823 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
7c01e5de14 Initial plan 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
3930647e37 Fix template interpolation failure in agentic workflows 
Remove shell command substitution syntax $(date +%Y-%m-%d) from workflow
markdown files that was causing template interpolation to fail. The shell
syntax is not valid in the context/frontmatter section that gets processed
by the template engine.

Fixed files:
- .github/workflows/a3-python-v2.md
- .github/workflows/a3-python.md
- .github/workflows/code-simplifier.md

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
54b12320a7 Initial plan 2026-02-18 21:02:26 -08:00
Daniel Tang
c17e8f990e Document example for Solver.sexpr() 2026-02-18 21:02:26 -08:00
copilot-swe-agent[bot]
5202b40309 Fix a3-python-v2 workflow compilation error 
- Remove invalid source reference to non-existent commit
- Fix network domains: 'default' → 'defaults'
- Remove serena tools configuration
- Recompile workflow with gh-aw v0.45.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:25 -08:00
copilot-swe-agent[bot]
06a49cdfaf Initial plan 2026-02-18 21:02:25 -08:00
Nikolaj Bjorner
8ab445c0d3 remove junk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:25 -08:00
copilot-swe-agent[bot]
068e8c70c4 Fix git sparse-checkout error in a3-python workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:25 -08:00
copilot-swe-agent[bot]
a29b41c744 Initial plan 2026-02-18 21:02:25 -08:00
Daniel Tang
c281e9dace Add Solver.solutions(t) 
For parity with
[z3.rs](https://docs.rs/z3/latest/z3/struct.Solver.html#method.solutions)
.

Having a way to find all solutions is frequently requested:
* https://stackoverflow.com/q/63231398/10477326
* https://stackoverflow.com/q/11867611/10477326

In accordance with the Rust, I did not
[guess `t`](https://stackoverflow.com/a/11869410/10477326).
 2026-02-18 21:02:25 -08:00
Daniel Tang
5b349f8f9a Suggest eval in ModelRef.__getitem__ error 
This improves the previously cryptic error message. I searched multiple
websites before Google AI suggested using model.eval(arr[0]) for getting
solutions out of arrays.
 2026-02-18 21:02:25 -08:00
Daniel Tang
380a8ee20f Alias ArithRef.__abs__ to Abs 
This integrates with the `abs(Int('x'))` Python builtin.
 2026-02-18 21:02:25 -08:00
Nikolaj Bjorner
a03500a194 git bindings v1.0 2026-02-18 21:02:25 -08:00
Nikolaj Bjorner
adacc27644 upgrade workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:24 -08:00
Copilot
d9c6da215f Eliminate unnecessary copies with std::move for ref-counted types (#8591) 2026-02-18 21:02:24 -08:00
Nikolaj Bjorner
61d8547a25 add tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
d75fbe766e Remove RuntimeIdentifier to fix assembly loading on macOS 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
4903917bc5 Fix test-nuget on macOS by rewriting csproj with proper configuration 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
85061952ca Initial plan 2026-02-18 21:02:24 -08:00
Nikolaj Bjorner
36342f9821 increment minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:24 -08:00
Nikolaj Bjorner
fdb4a4d3a5 update release to dedup and include manylinux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
ba75aae688 Replace Python deduplication script with shell commands 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
5fc29434dd Fix EOF handling in bash read and improve empty content detection 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
d7f87d7b19 Add proper error handling for empty file list and preserve filepath integrity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
86c2fa7a9d Improve file handling to properly handle special characters 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
9fe340cced Fix nightly build workflow by removing --clobber and adding deduplication 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:24 -08:00
copilot-swe-agent[bot]
014ba143a0 Initial plan 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
487db1a658 Modify behavior for division by zero 
Allow division by zero in z3 expressions without raising an error.
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
bcc87975e5 Delete src/api/python/test_critical_fixes.py 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
25c2b7e4c1 Fix error message capitalization for Python conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
0ee04d25c8 Add comprehensive tests for Python API bug fixes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
28db5e2440 Fix 9 critical assert statements and RatVal division by zero (Priority 1) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
fa17a90f15 Initial plan 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
5b54e4197e bump version to prepare for release with wheels and npm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
8fc8b51002 Remove --clobber option from nightly release 
Remove the --clobber option from the nightly release command.
 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
8c78067d6e Add release trigger to documentation workflow 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
49d41272d9 Remove assertion for number of watches in normalize 2026-02-18 21:02:23 -08:00
Nikolaj Bjorner
4c8b540020 Fix copy command for Linux Python packages 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
c946207e23 Fix BOUNDS and ASSERT_FAIL issues in Python API 
- Add negative index support to AstVector.__setitem__, ModelRef.__getitem__, ApplyResult.__getitem__
- Replace bare assertions with proper Z3Exception in z3num.Numeral methods
- All changes tested and validated with comprehensive test suite

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:23 -08:00
copilot-swe-agent[bot]
803b71f2a5 Initial plan 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
d9466be698 revert back to working build for manylinux arm 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
e8a8260081 manual attempt to fix up how wheels are copied based on old release.yml file 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
07c639a422 #8552 
make it recompile constraints with duplicates
 2026-02-18 21:02:22 -08:00
Nikolaj Bjorner
c031058978 small update to testing on p.m_sls_worker instead of should_run_sls 2026-02-18 21:02:22 -08:00
Copilot
730a54a767 Eliminate unnecessary copy operations in function parameters and range-based loops (#8589) 2026-02-18 21:02:22 -08:00
copilot-swe-agent[bot]
8fbf3f0169 Fix manylinux-python-arm64 to use native ARM64 container via QEMU 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:22 -08:00
copilot-swe-agent[bot]
bda8712458 Initial plan 2026-02-18 21:02:22 -08:00
Nuno Lopes
f6f8beaf78 Remove copies (#8583) 2026-02-18 21:02:22 -08:00
copilot-swe-agent[bot]
f2ad141ddf Refactor manylinux wheel production in nightly.yml workflow 
- Fix ARM64 auditwheel repair to use manylinux_2_28_aarch64 platform
- Update python-package job to copy pre-built manylinux wheels directly
- Remove Linux wheel rebuilding from python-package job
- Fix artifact naming: change PythonPackage to PythonPackages in publish-test-pypi

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:21 -08:00
copilot-swe-agent[bot]
9e489da0d0 Initial plan 2026-02-18 21:02:21 -08:00