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

20773 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
cff06b528f fix #8563 - align indices for flat quantifiers with sks vector layout, and also guard creating instantiation equalities with sort checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 20:57:38 -08:00
Nikolaj Bjorner
c0e8698bae
Merge pull request #8668 from Z3Prover/copilot/fix-build-warnings 
Fix C4267 warnings in ast.h initializer_list overloads
 2026-02-16 20:50:47 -08:00
copilot-swe-agent[bot]
037a4aa155 Fix C4267 build warnings in ast.h by adding static_cast for size_t to unsigned conversions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:44:23 +00:00
Nikolaj Bjorner
6884ffdd07
Merge pull request #8667 from Z3Prover/copilot/fix-a3-python-workflow-error 
Fix shell substitution breaking agentic workflow template interpolation
 2026-02-16 20:28:05 -08:00
copilot-swe-agent[bot]
9d8f736270 Initial plan 2026-02-17 04:27:04 +00:00
copilot-swe-agent[bot]
23d6262f7d Fix shell substitution in a3-python-v2 workflow as well 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:16:11 +00:00
copilot-swe-agent[bot]
f28b7ce440 Remove problematic shell substitution from a3-python workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:41 +00:00
copilot-swe-agent[bot]
a467a49453 Initial plan: Fix a3-python.md workflow shell substitution issue 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 04:15:08 +00:00
copilot-swe-agent[bot]
5da2b4ec19 Initial plan 2026-02-17 04:10:45 +00:00
Nikolaj Bjorner
27f11c8e76
Merge pull request #8664 from Z3Prover/copilot/simplify-go-bindings-code 
Simplify Go bindings: use astVectorToExprs helper in GetLowerAsVector/GetUpperAsVector
 2026-02-16 20:08:47 -08:00
copilot-swe-agent[bot]
5a9f416837 Simplify Go bindings: refactor GetLowerAsVector and GetUpperAsVector to use astVectorToExprs helper 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-17 03:46:58 +00:00
copilot-swe-agent[bot]
966e651b8b Initial plan 2026-02-17 03:44:53 +00:00
Nikolaj Bjorner
f9daab94d4
Merge pull request #8658 from Z3Prover/dependabot/github_actions/githubnext/gh-aw-0.45.1 
Bump githubnext/gh-aw from 0.42.17 to 0.45.1
 2026-02-16 19:40:30 -08:00
Nikolaj Bjorner
5c41b93498
Merge pull request #8659 from Z3Prover/dependabot/github_actions/actions/download-artifact-7.0.0 
Bump actions/download-artifact from 6.0.0 to 7.0.0
 2026-02-16 19:40:15 -08:00
Nikolaj Bjorner
88b004b5b6
Merge pull request #8660 from Z3Prover/dependabot/github_actions/actions/checkout-6.0.2 
Bump actions/checkout from 5.0.1 to 6.0.2
 2026-02-16 19:34:55 -08:00
Nikolaj Bjorner
86a12f4836
Merge pull request #8661 from Z3Prover/dependabot/github_actions/github/gh-aw-0.45.1 
Bump github/gh-aw from 0.43.15 to 0.45.1
 2026-02-16 19:34:43 -08:00
Nikolaj Bjorner
8eed390a6c
Merge pull request #8662 from Z3Prover/dependabot/github_actions/actions/cache-5.0.3 
Bump actions/cache from 4.3.0 to 5.0.3
 2026-02-16 19:34:29 -08:00
Nikolaj Bjorner
e612bfa226
Merge pull request #8657 from Z3Prover/copilot/fix-formatting-z3-go 
Fix formatting of z3.go
 2026-02-16 19:34:11 -08:00
dependabot[bot]
d241c7e745
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-02-16 22:15:45 +00:00
dependabot[bot]
f2f2d37a3f
Bump github/gh-aw from 0.43.15 to 0.45.1 
Bumps [github/gh-aw](https://github.com/github/gh-aw) from 0.43.15 to 0.45.1.
- [Release notes](https://github.com/github/gh-aw/releases)
- [Commits](https://github.com/github/gh-aw/compare/v0.43.15...v0.45.1)

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

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-16 22:15:27 +00:00
dependabot[bot]
93afd93766
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-02-16 22:13:44 +00:00
dependabot[bot]
7319b08b7f
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-16 22:13:09 +00:00
dependabot[bot]
a0d47dc65e
Bump githubnext/gh-aw from 0.42.17 to 0.45.1 
Bumps [githubnext/gh-aw](https://github.com/githubnext/gh-aw) from 0.42.17 to 0.45.1.
- [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.42.17...v0.45.1)

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

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-16 22:12:48 +00:00
copilot-swe-agent[bot]
96d9c66aff Fix formatting of z3.go using gofmt 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 22:00:07 +00:00
copilot-swe-agent[bot]
395c974941 Initial plan 2026-02-16 21:58:24 +00:00
Nikolaj Bjorner
1fb405cf44
Merge pull request #8655 from Z3Prover/copilot/fix-go-bindings-reference-count 
[WIP] Fix reference counting for Z3_ast_vector in go bindings
 2026-02-16 13:58:03 -08:00
Nikolaj Bjorner
dbfdf7f93f
Merge pull request #8654 from Z3Prover/copilot/update-go-bindings 
Add missing HIGH priority Solver APIs to Go bindings
 2026-02-16 13:56:09 -08:00
copilot-swe-agent[bot]
5dad1247de Fix variable naming: tmpFile -> tempFile for Go conventions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:48:51 +00:00
copilot-swe-agent[bot]
ea1f5a333a Fix Go bindings reference counting for Z3_ast_vector objects 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:48:49 +00:00
copilot-swe-agent[bot]
c99baf45d0 Address code review feedback: use os.CreateTemp and remove unused vars 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:47:33 +00:00
copilot-swe-agent[bot]
6d3c41143c Fix duplicate example in advanced_example.go and add silent markers for unused vars 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:46:23 +00:00
copilot-swe-agent[bot]
1e77b150a8 Initial plan 2026-02-16 21:44:51 +00:00
copilot-swe-agent[bot]
188880a20c Add missing high-priority Go bindings to Solver 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 21:28:24 +00:00
copilot-swe-agent[bot]
3212f7bdd7 Initial plan 2026-02-16 21:25:47 +00:00
Nikolaj Bjorner
144c352f7d
Merge pull request #8650 from Z3Prover/copilot/fix-sparse-checkout-error 
Fix sparse-checkout initialization in a3-python workflows
 2026-02-16 10:11:57 -08:00
Nikolaj Bjorner
184daa01a4
Merge pull request #8651 from Z3Prover/copilot/update-api-coherence-checker 
Add Go bindings to API coherence checker workflow
 2026-02-16 10:09:27 -08:00
copilot-swe-agent[bot]
479a6d3d3b Add Go bindings to API coherence checker workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 17:50:48 +00:00
copilot-swe-agent[bot]
47469a3876 Initial plan 2026-02-16 17:48:18 +00:00
Nikolaj Bjorner
1924066ff0 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:47:37 -08:00
Nikolaj Bjorner
dd10826c99
Merge pull request #8646 from Z3Prover/copilot/build-go-bindings-ci 
Enable Go bindings in ubuntu-cmake CI builds
 2026-02-16 09:45:42 -08:00
copilot-swe-agent[bot]
e3981e5213 Fix git sparse-checkout initialization in a3-python workflows 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 17:45:25 +00:00
copilot-swe-agent[bot]
9e459a7f6a Initial plan 2026-02-16 17:43:30 +00:00
Nikolaj Bjorner
e553ee2110 revert to last working flows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:29:10 -08:00
Nikolaj Bjorner
e87cf5ad2b remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-16 09:20:57 -08:00
copilot-swe-agent[bot]
d33c0e5601 Fix trailing whitespace in Go source files 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 06:06:48 +00:00
copilot-swe-agent[bot]
3f4bd11f00 Fix Go bindings and enable in CI 
- Fix all compilation errors in Go bindings
- Add missing type definitions (Pattern, ASTVector, ParamDescrs)
- Fix boolean comparisons to use bool() casts
- Fix Z3_app type casts using unsafe.Pointer
- Fix null symbol handling to use nil
- Fix unused variable in basic_example.go
- Fix CMake test target to run from examples/go directory
- Restore CI steps to build and test Go bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 06:05:58 +00:00
copilot-swe-agent[bot]
bbc1e501ab Fix Go bindings compilation issues and add to CI 
- Fix malformed z3.go with duplicate function body fragments
- Fix datatype.go to use Z3_del_constructor and Z3_del_constructor_list instead of non-existent inc_ref/dec_ref functions
- Remove non-existent Push/Pop methods from fixedpoint.go
- Fix CMake Go bindings targets quoting for proper LDFLAGS handling
- Add Go bindings support to ubuntu-cmake CI jobs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 05:58:20 +00:00
copilot-swe-agent[bot]
c454b14c24 Add Go bindings support to ubuntu-cmake CI builds 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-16 05:34:36 +00:00
Nikolaj Bjorner
249b59f42c
Merge pull request #8637 from Z3Prover/copilot/refactor-proof-functions-initializer-list 
Modernize mk_unit_resolution and mk_transitivity with std::initializer_list overloads
 2026-02-15 21:33:08 -08:00
Nikolaj Bjorner
a6620765dc
Merge pull request #8638 from Z3Prover/copilot/refactor-update-quantifier-initializer-list 
Modernize update_quantifier with std::initializer_list overloads
 2026-02-15 21:32:38 -08:00