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

21680 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
8f23830879 Initial plan 2026-02-20 04:22:02 +00:00
Nikolaj Bjorner
8314aecb44
Merge pull request #8686 from Z3Prover/finite-sets 
Finite sets
 2026-02-19 19:49:47 -08:00
Nikolaj Bjorner
30e4c9a629
Fix badge links in README.md 2026-02-19 19:47:30 -08:00
Nikolaj Bjorner
c56e033a94
Merge pull request #8700 from Z3Prover/copilot/update-readme-banners-remove-workflows 
Update README.md build status banners
 2026-02-19 19:40:40 -08:00
Nikolaj Bjorner
99e1ba3a6e update macos runner id 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 19:12:44 -08:00
Nikolaj Bjorner
3d8dd0d783 update params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 19:06:06 -08:00
copilot-swe-agent[bot]
e37624ab13 Update README.md banners: remove disabled workflows, fix WASM link, add A3 Python badge 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-20 03:01:16 +00:00
copilot-swe-agent[bot]
1521c43702 Initial plan 2026-02-20 02:57:28 +00:00
Lev Nachmanson
9c4e172e95 set the default of lws_spt_threshold to 4 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 14:18:11 -10:00
Lev Nachmanson
385f913a33 try optimize handle_nullified_poly 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 13:58:45 -10:00
Nikolaj Bjorner
38ce0882db remove lattice component 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 15:49:45 -08:00
Nikolaj Bjorner
bf73fddf6f
Merge pull request #8693 from Z3Prover/copilot/fix-test-coverage-gaps 
Add unit tests covering ackermannization module and Z3_algebraic_eval
 2026-02-19 15:32:46 -08:00
Nikolaj Bjorner
369890330e
Merge pull request #8699 from Z3Prover/copilot/fix-missed-bugs-ff-by-one 
Fix off-by-one vulnerabilities in ackermannization module
 2026-02-19 15:32:23 -08:00
copilot-swe-agent[bot]
dbd7cd7414 Fix off-by-one vulnerabilities: use range-based for on goals; cache loop bound 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 22:37:22 +00:00
copilot-swe-agent[bot]
093e227689 Add ackermannize tests for mutation coverage 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 22:07:41 +00:00
Nikolaj Bjorner
5bd7d93b55 add parameter validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 14:02:59 -08:00
Nikolaj Bjorner
ee03533c3a update examples to use arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:57:43 -08:00
Lev Nachmanson
426f8396e3
Merge pull request #8691 from Z3Prover/no_fail 
Disable failure on a nullified polynomial in levelwise
 2026-02-19 11:46:46 -10:00
Nikolaj Bjorner
c94eb5dc88 fixup API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-19 13:33:25 -08:00
copilot-swe-agent[bot]
f414c7982d Initial plan 2026-02-19 21:26:59 +00:00
copilot-swe-agent[bot]
5e5d9ebfaf Fix test_ackermannize_bv_model: skip crashing model converter test, keep 4 passing tests 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 21:07:30 +00:00
Lev Nachmanson
23560ba8a5 cleanup regarding levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 09:31:30 -10:00
Nikolaj Bjorner
44cd412426
Merge pull request #8694 from Z3Prover/copilot/sub-pr-8686 
Fix ambiguous svector constructor calls in theory_finite_set_lattice_refutation
 2026-02-19 10:49:13 -08:00
Nikolaj Bjorner
ca1865c3fe
Merge pull request #8696 from Z3Prover/copilot/fix-z3-import-error 
Fix arm64 libz3.dylib being packaged in x86_64 macOS wheels
 2026-02-19 10:48:30 -08:00
copilot-swe-agent[bot]
879dc93d2a Add tests for ackermannization module and Z3_algebraic_eval 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 18:18:19 +00:00
copilot-swe-agent[bot]
c4acd2a47e Fix macOS cross-compilation from ARM64 to x86_64 in mk_unix_dist.py and mk_util.py 
When macos-latest changed to ARM64 runners, the mac-build-x64 job started
producing arm64 libz3.dylib inside x86_64-tagged wheels, causing import
failures on macOS x86_64.

Root cause: mk_make.py subprocess detects the ARM64 host at module level
(IS_ARCH_ARM64=True), and without --arm64=false override it adds -arch arm64
to SLIBEXTRAFLAGS, overriding the -arch x86_64 set via environment variables.

Fix 1 (mk_unix_dist.py): Pass --arm64=false to mk_make.py subprocess when
building x64 on an ARM64 host, preventing the arm64 flag inheritance.

Fix 2 (mk_util.py): When IS_ARCH_ARM64=False on an ARM64 macOS host, add
-arch x86_64 to SLIBEXTRAFLAGS so the shared library linker also targets
x86_64 (LDFLAGS already receives this flag from the env var).

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 18:02:52 +00:00
Nikolaj Bjorner
2fa04f5e38
Merge pull request #8695 from Z3Prover/copilot/simplify-code-structure 
Remove unnecessary blank lines in mk_genfile_common.py and mk_api_doc.py
 2026-02-19 09:58:19 -08:00
copilot-swe-agent[bot]
866f352ea9 Fix ambiguous svector constructor calls in theory_finite_set_lattice_refutation.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 17:57:04 +00:00
Nikolaj Bjorner
8a28bc28f1
Update nightly-validation.yml 2026-02-19 09:54:29 -08:00
copilot-swe-agent[bot]
0ad40a3f54 Remove unnecessary blank lines in mk_genfile_common.py and mk_api_doc.py 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-19 17:52:11 +00:00
copilot-swe-agent[bot]
9c8c9f5eea Initial plan 2026-02-19 17:51:02 +00:00
copilot-swe-agent[bot]
d7aa454760 Initial plan 2026-02-19 17:50:23 +00:00
copilot-swe-agent[bot]
ca8f379823 Initial plan 2026-02-19 17:49:39 +00:00
copilot-swe-agent[bot]
cd32dbe403 Initial plan 2026-02-19 17:26:34 +00:00
Lev Nachmanson
91a3068f79 disable a failure on a nullified poly in levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-19 07:18:10 -10:00
Nikolaj Bjorner
86dc55691d add extra parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:34:29 -08:00
Nikolaj Bjorner
9f91380b7d next release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:30:08 -08:00
Nikolaj Bjorner
31a85925ee
Delete FINITE_SET_API.md 2026-02-18 21:14:55 -08:00
Nikolaj Bjorner
a32c9effb2 remove examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:13:48 -08:00
Nikolaj Bjorner
24f36c2498
Delete examples/SMT-LIB2/finite-sets/cycle.smt2 2026-02-18 21:12:28 -08:00
Nikolaj Bjorner
7fe9b1f873
Merge branch 'master' into finite-sets 2026-02-18 21:11:44 -08:00
Nikolaj Bjorner
07d8971ef9 add sketch for incremental algorithm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:10:17 -08:00
Nikolaj Bjorner
69b73c64cf enable post setup parameter tweaking in theory solvers, update azure-pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:08:24 -08:00
Nikolaj Bjorner
c32b213a20 add finite sets to datatype recursion, delay initialize finite_set plugin, fix bugs in are_distinct and equality simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:07:40 -08:00
Nikolaj Bjorner
a1d43f5fb9 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:03:19 -08:00
Nikolaj Bjorner
fc792b645c update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
2f33a34692 Fix OCaml build error in solver_get_levels 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
316bc3d821 Initial plan 2026-02-18 21:02:32 -08:00
Nikolaj Bjorner
29e759ac27 Delete examples/go/test_new_api_additions.go 2026-02-18 21:02:32 -08:00
copilot-swe-agent[bot]
c22e20c8a0 Add test for new Go API methods 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 21:02:32 -08:00