mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-10 07:10:30 +00:00
Code Activity
21903 commits 48 branches 58 tags 223 MiB
Commit graph

21903 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
4e5695eb53
Merge pull request #8896 from Z3Prover/copilot/fix-jni-bindings-architecture 
fix: JNI bindings respect target architecture during macOS cross-compilation
 2026-03-09 13:44:33 -07:00
Nikolaj Bjorner
4b377ae713
Merge pull request #8898 from Z3Prover/copilot/address-actionable-issues-discussion 
Fix actionable null pointer dereferences and uninitialized variables from static analysis
 2026-03-09 10:45:47 -07:00
Nikolaj Bjorner
525c9dbb12
Merge pull request #8900 from Z3Prover/copilot/fix-memory-leak-detected 
Fix memory leaks in test code detected by ASan/LSan
 2026-03-09 10:44:12 -07:00
copilot-swe-agent[bot]
a6c94a1bfc Refactor sls_euf_plugin.cpp validate_model and add SASSERT in udoc_relation.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:57:59 +00:00
copilot-swe-agent[bot]
391febed3b Fix null pointer dereferences and uninitialized variables from discussion #8891 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:51:12 +00:00
copilot-swe-agent[bot]
7d19851c2f fix: fix memory leaks detected by ASan in test code 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:48:17 +00:00
copilot-swe-agent[bot]
e4b85d234e Initial plan 2026-03-09 16:44:45 +00:00
Nikolaj Bjorner
2e1f79e0d4
Merge pull request #8897 from Z3Prover/copilot/address-open-issues-except-rust 
Go: add MkBVRotateLeft, MkBVRotateRight, MkRepeat to bitvec.go
 2026-03-09 09:37:01 -07:00
Nikolaj Bjorner
56d15655a7 update report 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-09 09:34:33 -07:00
copilot-swe-agent[bot]
6a1aa797e2 test: add unit tests and CI validation for JNI architecture fix 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:28:12 +00:00
copilot-swe-agent[bot]
47e9c37fbb Go: Add MkBVRotateLeft, MkBVRotateRight, MkRepeat to bitvec.go 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:20:13 +00:00
copilot-swe-agent[bot]
9dcd01c52b Initial plan 2026-03-09 16:18:25 +00:00
copilot-swe-agent[bot]
0af49cdf10 Initial plan 2026-03-09 16:17:19 +00:00
copilot-swe-agent[bot]
ba0f276584 fix: use SLINK_EXTRA_FLAGS for JNI bindings to support macOS cross-compilation 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-09 16:15:57 +00:00
copilot-swe-agent[bot]
b90f1e3e28 Initial plan 2026-03-09 16:09:14 +00:00
Lev Nachmanson
8a146a92ec fix: replace UNREACHABLE with VERIFY for non-COI constraint/monic violations in nra_solver 
The NRA solver's check() uses cone-of-influence (COI) to select a subset
of constraints for nlsat. When nlsat returns l_true, the model is validated
against all constraints, but non-COI constraints can legitimately be
violated since nlsat only solved over the COI subset.

- Non-COI violations gracefully return l_undef (fallback to other strategies)
- COI violations still trigger an assertion (indicating a real nlsat bug)

Fixes #8883

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-06 08:54:34 -10:00
Nikolaj Bjorner
84a7566c3a
Merge pull request #8878 from Z3Prover/copilot/rename-qf-s-benchmark 
Rename "Qf S Benchmark" to "ZIPT Benchmark"
 2026-03-05 16:26:26 -08:00
copilot-swe-agent[bot]
ea4ee11117 Rename Qf S Benchmark to ZIPT Benchmark in workflow files 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-06 00:05:35 +00:00
copilot-swe-agent[bot]
489b34a124 Initial plan 2026-03-06 00:02:10 +00:00
Nikolaj Bjorner
e8bfa10d29 test c3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-05 16:00:55 -08:00
Nikolaj Bjorner
e9ee188747
Merge pull request #8874 from Z3Prover/copilot/remove-unreachable-return-statement-another-one 
Remove unreachable `return false` in `match_ubv2s1`
 2026-03-05 10:05:53 -08:00
copilot-swe-agent[bot]
822f19819c Remove unreachable return false in match_ubv2s1 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-05 17:59:50 +00:00
copilot-swe-agent[bot]
d89532a33d Initial plan 2026-03-05 17:58:32 +00:00
Nikolaj Bjorner
e7e116f2b2
Merge pull request #8869 from Z3Prover/copilot/any-branch-fix 
Fix contradictory UBSan recovery flags in memory-safety workflow
 2026-03-05 08:58:29 -08:00
copilot-swe-agent[bot]
71a4786371 Fix contradictory UBSan recovery flags in memory-safety.yml 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-03-05 16:14:27 +00:00
copilot-swe-agent[bot]
90af464af3 Initial plan 2026-03-05 16:10:48 +00:00
Nikolaj Bjorner
51ae6eeccc
Merge pull request #8856 from angelica-moreira/memory-safety-pipeline 
Add ASan/UBSan memory safety CI workflow
 2026-03-04 13:05:57 -08:00
Angelica Moreira
123bb620d4 Add ASan/UBSan memory safety CI workflow 
Adds a workflow that builds and tests Z3 with AddressSanitizer and
UndefinedBehaviorSanitizer on every push to catch runtime memory errors
and undefined behavior. Runs unit tests, SMT-LIB2 benchmarks, and
regression tests under both sanitizers. Includes a Copilot agentic
workflow to generate summary reports as GitHub Discussions.

Triggered on push (path-filtered to src/) and manual dispatch.
 2026-03-04 16:31:29 +00:00
Nikolaj Bjorner
d40c4721d8
Merge pull request #8838 from Z3Prover/copilot/fix-no-such-field-error 
Fix NoSuchFieldError in Java JNI wrapper for BOOL OUT/INOUT parameters
 2026-03-02 19:10:21 -08:00
Nikolaj Bjorner
9031089999 add zipt reviewer to master branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-02 16:51:52 -08:00
copilot-swe-agent[bot]
c384710b08 Fix NoSuchFieldError in JNI for BoolPtr: use Z field descriptor and SetBooleanField 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 23:56:42 +00:00
copilot-swe-agent[bot]
027b46b2ed Initial plan 2026-03-02 23:52:53 +00:00
Nikolaj Bjorner
30483d6cf2
Merge pull request #8835 from Z3Prover/dependabot/github_actions/actions/download-artifact-8.0.0 
Bump actions/download-artifact from 6.0.0 to 8.0.0
 2026-03-02 15:48:03 -08:00
Nikolaj Bjorner
ef648ff632
Merge pull request #8833 from Z3Prover/dependabot/github_actions/actions/upload-artifact-7.0.0 
Bump actions/upload-artifact from 6.0.0 to 7.0.0
 2026-03-02 15:47:48 -08:00
Nikolaj Bjorner
07742ed49f
Merge pull request #8834 from Z3Prover/dependabot/github_actions/actions/cache-5.0.3 
Bump actions/cache from 4.3.0 to 5.0.3
 2026-03-02 15:47:34 -08:00
Nikolaj Bjorner
ba88256a2a
Merge pull request #8836 from Z3Prover/dependabot/github_actions/actions/checkout-6.0.2 
Bump actions/checkout from 5.0.1 to 6.0.2
 2026-03-02 15:47:22 -08:00
Nikolaj Bjorner
377c85f491
Merge pull request #8837 from Z3Prover/dependabot/github_actions/github/gh-aw-0.51.6 
Bump github/gh-aw from 0.45.6 to 0.51.6
 2026-03-02 15:47:11 -08:00
dependabot[bot]
11d3a11cea
Bump github/gh-aw from 0.45.6 to 0.51.6 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.45.6 to 0.51.6.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.45.6...v0.51.6)

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

Signed-off-by: dependabot[bot] <support@github.com>
 2026-03-02 23:44:00 +00:00
dependabot[bot]
e482052b37
Bump actions/checkout from 5.0.1 to 6.0.2 
Bumps [actions/checkout](https://github.com/actions/checkout) from 5.0.1 to 6.0.2.
- [Release notes](https://github.com/actions/checkout/releases)
- [Commits](https://github.com/actions/checkout/compare/v5.0.1...v6.0.2)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: 6.0.2
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-03-02 23:42:08 +00:00
dependabot[bot]
867e768aa8
Bump actions/download-artifact from 6.0.0 to 8.0.0 
Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 6.0.0 to 8.0.0.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](https://github.com/actions/download-artifact/compare/v6...v8)

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

Signed-off-by: dependabot[bot] <support@github.com>
 2026-03-02 23:41:23 +00:00
dependabot[bot]
b7a4ddbcd5
Bump actions/cache from 4.3.0 to 5.0.3 
Bumps [actions/cache](https://github.com/actions/cache) from 4.3.0 to 5.0.3.
- [Release notes](https://github.com/actions/cache/releases)
- [Commits](https://github.com/actions/cache/compare/v4.3.0...v5.0.3)

---
updated-dependencies:
- dependency-name: actions/cache
  dependency-version: 5.0.3
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-03-02 23:40:54 +00:00
dependabot[bot]
a7e3635931
Bump actions/upload-artifact from 6.0.0 to 7.0.0 
Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 6.0.0 to 7.0.0.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](https://github.com/actions/upload-artifact/compare/v6...v7)

---
updated-dependencies:
- dependency-name: actions/upload-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-03-02 23:40:26 +00:00
Nikolaj Bjorner
96285b0f91
Merge pull request #8824 from Z3Prover/copilot/fix-issues-except-rust 
Fix issues reported in discussion 8823 for all languages except Rust
 2026-03-02 10:35:31 -08:00
Nikolaj Bjorner
94809d413a
Merge pull request #8825 from Z3Prover/copilot/fix-reported-issues-8822 
Fix CSA-reported undefined behavior and uninitialized variables
 2026-03-02 10:03:16 -08:00
copilot-swe-agent[bot]
1461a53347 Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 16:22:08 +00:00
copilot-swe-agent[bot]
28fbe33114 Add missing API bindings: Python BvNand/BvNor/BvXnor, Go MkAsArray/MkRecFuncDecl/AddRecDef/Model.Translate, TS Array.fromFunc/Model.translate, OCaml Model.translate 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:21:57 +00:00
copilot-swe-agent[bot]
8e94cad8ab Fix static analysis findings: uninitialized vars, bitwise shift UB, garbage values 
- nla_core.cpp: Initialize j = null_lpvar in is_octagon_term
- bit2int.cpp: Initialize sign_p, sign_n, sz_p, sz_n
- act_cache.cpp: Initialize debug vars to nullptr
- enum2bv_rewriter.cpp: Use unsigned literal in 1u << idx
- bit_matrix.cpp: Use unsigned literal in 1u << (n-1)
- bit_util.cpp: Guard against bit_shift == 0 in shl/shr
- mpff.cpp: Cast exp to unsigned before shifting
- sorting_network.h: Guard against bits == 0
- dl_sparse_table.h: Use >= 64 instead of == 64

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-02 00:13:55 +00:00
copilot-swe-agent[bot]
122ee94935 Initial plan 2026-03-02 00:06:13 +00:00
copilot-swe-agent[bot]
8fad12fe18 Initial plan 2026-03-02 00:05:23 +00:00
Nikolaj Bjorner
dcb888d4c8
Merge pull request #8821 from Z3Prover/copilot/update-clang-analyzer-timeout 
Increase Clang Static Analyzer workflow timeout to 180 minutes
 2026-03-01 12:40:41 -08:00