mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity
20708 commits 69 branches 57 tags 175 MiB
Commit graph

20708 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a0d232fc2a
Merge pull request #8642 from Z3Prover/copilot/debug-agentic-workflow-a3-python-v2 
Fix a3-python-v2 workflow compilation failure
 2026-02-15 20:46:41 -08:00
Nikolaj Bjorner
a96a4f5447 remove junk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-15 18:00:42 -08:00
copilot-swe-agent[bot]
d6300b995c 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-16 01:33:43 +00:00
copilot-swe-agent[bot]
573e53adfa Initial plan 2026-02-16 01:29:46 +00:00
Nikolaj Bjorner
1463b1ef08
Merge pull request #8611 from Z3Prover/copilot/fix-action-run-error 
Fix sparse-checkout initialization in a3-python workflows
 2026-02-15 17:23:06 -08:00
Nikolaj Bjorner
166a9afab0
Merge pull request #8633 from danielzgtg/feat/solverSolutions 
Add Solver.solutions(t)
 2026-02-15 17:22:03 -08:00
Nikolaj Bjorner
24f3258c49
Merge pull request #8626 from danielzgtg/feat/modelRefGetitemErrorMessageModelRefEval 
Suggest eval in ModelRef.__getitem__ error
 2026-02-15 17:20:11 -08:00
Nikolaj Bjorner
e58c689d42
Merge pull request #8623 from danielzgtg/feat/__abs__ 
Alias ArithRef.__abs__ to Abs
 2026-02-15 17:17:21 -08:00
Daniel Tang
32c4c87e22
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-15 01:18:02 -05:00
Daniel Tang
1ada488cb6
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-14 18:16:39 -05:00
Daniel Tang
c172b58268
Alias ArithRef.__abs__ to Abs 
This integrates with the `abs(Int('x'))` Python builtin.
 2026-02-14 01:37:58 -05:00
Nikolaj Bjorner
e2486eff77 upgrade workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-13 08:57:00 -08:00
Copilot
cc7e6cd92d
Eliminate unnecessary copies with std::move for ref-counted types (#8591) 2026-02-13 12:16:47 +00:00
copilot-swe-agent[bot]
8a49ca490f Fix git sparse-checkout error in a3-python workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-13 03:54:06 +00:00
copilot-swe-agent[bot]
34038e2b6d Initial plan 2026-02-13 03:51:36 +00:00
Nikolaj Bjorner
83b60990b1 add tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 19:40:19 -08:00
Nikolaj Bjorner
3f15666441
Merge pull request #8603 from Z3Prover/copilot/fix-github-actions-job 
Fix macOS NuGet validation: remove RuntimeIdentifier to match package structure
 2026-02-12 19:25:17 -08:00
Nikolaj Bjorner
a81f691899 increment minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 17:31:50 -08:00
copilot-swe-agent[bot]
fc6140e489 Remove RuntimeIdentifier to fix assembly loading on macOS 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 21:24:22 +00:00
copilot-swe-agent[bot]
1ea2b0865a Fix test-nuget on macOS by rewriting csproj with proper configuration 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 21:22:30 +00:00
copilot-swe-agent[bot]
c392c460ad Initial plan 2026-02-12 21:19:19 +00:00
Nikolaj Bjorner
f80414f4bb update release to dedup and include manylinux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 11:38:41 -08:00
Nikolaj Bjorner
b381de4f3f
Merge pull request #8602 from Z3Prover/copilot/fix-nightly-build-job 
Fix nightly workflow: remove unsupported --clobber flag and add artifact deduplication
 2026-02-12 10:23:19 -08:00
copilot-swe-agent[bot]
97bdef79b5 Replace Python deduplication script with shell commands 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 18:21:25 +00:00
copilot-swe-agent[bot]
24d9a62356 Fix EOF handling in bash read and improve empty content detection 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 17:43:37 +00:00
copilot-swe-agent[bot]
a1f5016f02 Add proper error handling for empty file list and preserve filepath integrity 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 17:42:24 +00:00
copilot-swe-agent[bot]
c1603fc65a Improve file handling to properly handle special characters 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 17:41:02 +00:00
Nikolaj Bjorner
5497de0af7
Merge pull request #8597 from Z3Prover/copilot/fix-high-severity-bugs-python-api 
Fix 13 critical bugs in Python API: assertion removal, division by zero, bounds checking
 2026-02-12 09:40:50 -08:00
copilot-swe-agent[bot]
6bc44183bc Fix nightly build workflow by removing --clobber and adding deduplication 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 17:39:24 +00:00
copilot-swe-agent[bot]
aa95c98664 Initial plan 2026-02-12 17:36:49 +00:00
Nikolaj Bjorner
e6d32f3d40 bump version to prepare for release with wheels and npm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-12 08:59:40 -08:00
Nikolaj Bjorner
0be5434f29
Remove --clobber option from nightly release 
Remove the --clobber option from the nightly release command.
 2026-02-12 08:21:54 -08:00
Nikolaj Bjorner
7c42ec3b25
Add release trigger to documentation workflow 2026-02-12 07:53:21 -08:00
Nikolaj Bjorner
8077e3d031
Modify behavior for division by zero 
Allow division by zero in z3 expressions without raising an error.
 2026-02-12 07:10:00 -08:00
Nikolaj Bjorner
dcbafa9442
Delete src/api/python/test_critical_fixes.py 2026-02-12 07:07:15 -08:00
Nikolaj Bjorner
39f5ef5e4e
Remove assertion for number of watches in normalize 2026-02-12 07:03:52 -08:00
Nikolaj Bjorner
3974bd1f45
Fix copy command for Linux Python packages 2026-02-12 06:59:06 -08:00
copilot-swe-agent[bot]
a8f32ed291 Fix error message capitalization for Python conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 05:03:07 +00:00
copilot-swe-agent[bot]
69bf729a22 Add comprehensive tests for Python API bug fixes 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 05:01:41 +00:00
copilot-swe-agent[bot]
629d999fa2 Fix 9 critical assert statements and RatVal division by zero (Priority 1) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-12 04:45:35 +00:00
copilot-swe-agent[bot]
860bcd4483 Initial plan 2026-02-12 04:42:49 +00:00
Nikolaj Bjorner
7b38512efa
Merge pull request #8595 from Z3Prover/copilot/fix-dse-confirmed-bugs 
Fix Python API: negative index handling and exception types
 2026-02-11 19:31:11 -08:00
copilot-swe-agent[bot]
6743d42ea4 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-12 03:05:06 +00:00
copilot-swe-agent[bot]
9a46074b37 Initial plan 2026-02-12 02:43:35 +00:00
Nikolaj Bjorner
3c1a82f80c revert back to working build for manylinux arm 2026-02-11 17:45:29 -08:00
Nikolaj Bjorner
eec44bd5d5 manual attempt to fix up how wheels are copied based on old release.yml file 2026-02-11 17:40:34 -08:00
Nikolaj Bjorner
ae51cb04ba #8552 
make it recompile constraints with duplicates
 2026-02-11 17:38:45 -08:00
Nikolaj Bjorner
fb172b67ac small update to testing on p.m_sls_worker instead of should_run_sls 2026-02-11 17:38:45 -08:00
Copilot
20fef3f449
Eliminate unnecessary copy operations in function parameters and range-based loops (#8589) 2026-02-11 21:14:32 +00:00
Nikolaj Bjorner
f76c30b3bd
Merge pull request #8590 from Z3Prover/copilot/fix-nightly-build-workflow 
[WIP] Fix failing GitHub Actions job in Nightly Build workflow
 2026-02-11 12:59:03 -08:00