3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
Commit graph

20469 commits

Author SHA1 Message Date
Copilot
338df5a38f Migrate release.yml from Azure DevOps to GitHub Actions (#8239)
* Initial plan

* Create GitHub Actions release.yml workflow

- Migrated Azure DevOps release pipeline to GitHub Actions
- Aligned structure and conventions with nightly.yml
- Added manual workflow dispatch with version input
- Included conditional publishing to GitHub, NuGet, and PyPI
- Updated to use manylinux_2_28 container (consistent with nightly)
- Added --zip flag to all Windows builds
- Set 7-day retention for release artifacts

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:34 -08:00
Nikolaj Bjorner
aeee4f41af update nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:57:34 -08:00
Copilot
90101c830e Add .github/workflows/nightly.yml to update_version.py (#8236)
* Initial plan

* Add update_github_nightly_yml function to update .github/workflows/nightly.yml

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:34 -08:00
Nikolaj Bjorner
cc136efe94 Update python-package job dependencies in nightly.yml
Removed manylinux-python-arm64 dependency from python-package job.
2026-02-18 20:57:34 -08:00
Nikolaj Bjorner
b769ca3639 check context match
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:57:34 -08:00
Copilot
018461e60d Migrate iterator-based for loops to range-based for loops (#8231)
* Initial plan

* Migrate iterator-based for loops to range-based for loops in 11 files

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix compilation error in aig_exporter.cpp - use correct iterator API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Revert changes to z3++.h as requested

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:34 -08:00
Copilot
afe432b165 Fix nightly release deployment: explicitly delete Git tag to prevent asset conflicts (#8233)
* Initial plan

* Fix nightly release deployment by explicitly deleting tag

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:34 -08:00
Copilot
c58ef30944 Add sequence higher-order functions to Java API (#8226)
* Initial plan

* Add four sequence operations to Java API (SeqMap, SeqMapi, SeqFoldl, SeqFoldli)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix checkContextMatch call and add test for sequence operations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add 4-parameter checkContextMatch overload for consistency

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:33 -08:00
Copilot
509cd8d36e Add benchmark export to C# and TypeScript APIs (#8228)
* Initial plan

* Add benchmark export functionality to C# and TypeScript APIs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix TypeScript build error: remove redundant array length parameter

The Z3 TypeScript wrapper auto-generates array length parameters from the array itself, so passing assumptions.length explicitly causes a parameter count mismatch. Removed the redundant parameter.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:33 -08:00
Copilot
2304da0fa2 Add advanced sequence operations to C# API (#8227)
* Initial plan

* Add advanced sequence operations to C# API

- Add MkSeqMap: Map function over sequence
- Add MkSeqMapi: Map function over sequence with index
- Add MkSeqFoldLeft: Fold left operation on sequence
- Add MkSeqFoldLeftI: Fold left with index on sequence

These functions match Python's SeqMap, SeqMapI, SeqFoldLeft, and SeqFoldLeftI and provide feature parity with other language bindings.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:33 -08:00
Nikolaj Bjorner
6dd29d2b54 Update nightly.yml 2026-02-18 20:57:33 -08:00
Nikolaj Bjorner
c27378b8cc List files in tmp directory for nightly release
Add a command to list files before creating the nightly release.
2026-02-18 20:57:33 -08:00
Copilot
381d604e78 Change code-conventions-analyzer workflow from weekly to daily schedule (#8229)
* Initial plan

* Update code-conventions-analyzer to run daily instead of weekly

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:33 -08:00
Nikolaj Bjorner
eaec507c94 Add architecture option to build command 2026-02-18 20:57:33 -08:00
Copilot
22e404a93f Fix mk_unix_dist.py cross-compilation from ARM to x64 on macOS (#8222)
* Initial plan

* Add support for ARM to X64 cross-compilation on macOS

- Initialize LINUX_X64 from mk_util.LINUX_X64
- Add support for --arch=x64 flag to force x64 builds
- Handle cross-compilation from ARM64 to x64 on macOS using -arch x86_64 flags
- Update help text to reflect both arm64 and x64 architecture options

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix cross-compilation detection using HOST_IS_ARM64

Use separate HOST_IS_ARM64 variable to track the host architecture,
allowing proper detection of ARM to x64 cross-compilation scenarios.
This ensures the correct compiler flags are set when building x64
on ARM hosts.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review: improve arch flag handling

- Extract target_arch_flag to variable to reduce duplication
- Add .strip() calls to handle trailing spaces in environment variables
- Ensure proper spacing in concatenated flags

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:32 -08:00
copilot-swe-agent[bot]
2e04baa062 Clean up temporary test files
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:32 -08:00
copilot-swe-agent[bot]
0115b7cadc Fix segfault in dioph_eq.cpp by adding bounds check
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:32 -08:00
copilot-swe-agent[bot]
4e502ba928 Initial analysis of segfault issue
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:32 -08:00
copilot-swe-agent[bot]
ddb0a2f7e8 Initial plan 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
bd7caa2802 Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
021d24d0cb Update C++ compiler version in cross-build workflow 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
a0dca6b570 Change container image from ubuntu:jammy to ubuntu:noble 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
f63a4236c3 Update GCC version in cross-build workflow 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
b0c655d2cf Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
3f48780224 Update nightly.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
fd1ef7f7b0 Add workflow_dispatch trigger to android-build.yml 2026-02-18 20:57:32 -08:00
Nikolaj Bjorner
2d814446a5 Update cross-build.yml 2026-02-18 20:57:31 -08:00
Copilot
de825be4c7 Replace fall-through comments with Z3_fallthrough macro (#8219)
* Initial plan

* Fix switch fall-through warnings with Z3_fallthrough attribute

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:31 -08:00
Copilot
c8d6b3161f Update cross-build workflow to GCC 12 for C++20 support (#8220)
* Initial plan

* Update cross-build workflow to use g++-12 for C++20 support

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:31 -08:00
Copilot
11970f9203 Fix 13 compiler warnings: sign-comparison and unused parameters (#8215)
* Initial plan

* Fix 13 compiler warnings: sign-comparison and unused parameters

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:31 -08:00
Copilot
ac097f1d74 Fix artifact extraction patterns in nightly Python packaging job (#8217)
* Initial plan

* Fix unzip patterns in Python packaging job

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:31 -08:00
Ilana Shapiro
6f41e9fc29 Fix UNKNOWN bug in search tree about inconsistent end state (#8214)
* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree

* clean up code, fix deadlock

* delete test files

* clean up

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
2026-02-18 20:57:31 -08:00
Copilot
1d304d0300 Fix nightly build failures in ARM64 and Python packaging jobs (#8213)
* Initial plan

* Fix nightly build workflow failures for ARM64 and Python packaging

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:31 -08:00
Nuno Lopes
b1b582d3e8 bot: restore std::format 2026-02-18 20:57:31 -08:00
Copilot
2bcc366d32 [WIP] Update nightly.yml to fix build error with macOS runner (#8209)
* Initial plan

* Fix macos-13 runner retirement: update to macos-14

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Copilot
5986ca33ef Fix checkout action GLIBC incompatibility in manylinux and macOS builds (#8207)
* Initial plan

* Fix checkout action compatibility with manylinux containers and macOS

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Copilot
71d26fd233 Reapply PR #8190: Replace std::ostringstream with C++20 std::format (#8204)
* Initial plan

* Reapply PR #8190: Replace std::ostringstream with C++20 std::format

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Copilot
a71cabf8c7 Migrate nightly builds from Azure DevOps to GitHub Actions (#8206)
* Initial plan

* Add GitHub Actions workflow for nightly builds

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix Windows builds to use --zip flag instead of manual archiving

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Nikolaj Bjorner
f39497c8e7 fix #8195
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:57:30 -08:00
Copilot
d43b6d2684 Change code-conventions-analyzer workflow discussion category to "Agentic Workflows" (#8203)
* Initial plan

* Update code-conventions-analyzer discussion category to "Agentic Workflows"

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Copilot
5d78c82f01 Update api-coherence-checker workflow to use "Agentic Workflows" discussion category (#8202)
* Initial plan

* Update api-coherence-checker to use "Agentic Workflows" discussion category

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Nikolaj Bjorner
aa6fddf944 simplify contains check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:57:30 -08:00
Ilana Shapiro
f5fc7eb173 Add core strengthening and non-chronological backtracking to parallel search tree (#8193)
* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
2026-02-18 20:57:30 -08:00
Copilot
8a4f5f56fc Fix api-coherence workflow to verify and filter resolved issues (#8201)
* Initial plan

* Update api-coherence workflow to verify and filter resolved issues

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:30 -08:00
Copilot
317dd92105 Standardize for-loop increments to prefix form (++i) (#8199)
* Initial plan

* Convert postfix to prefix increment in for loops

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix member variable increment conversion bug

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update API generator to produce prefix increments

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:29 -08:00
Copilot
851b8ea31c Replace manual pair unpacking with structured bindings (#8197)
* Initial plan

* Apply structured bindings to enode_bool_pair usage

Replace manual unpacking of pairs with C++17 structured bindings in:
- src/ast/euf/euf_egraph.cpp
- src/smt/smt_internalizer.cpp
- src/smt/smt_context.cpp (2 locations)

This improves code readability and reduces boilerplate code.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:27 -08:00
Copilot
a5a2a37495 Replace remaining NULL with nullptr (#8198)
* Initial plan

* Replace NULL with nullptr in spacer_context.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:27 -08:00
Copilot
1ee3e17c31 Update ARM GCC toolchain to 13.3 for C++20 std::format support (#8196)
* Initial plan

* Update ARM GCC toolchain from 11.2 to 13.3 for C++20 std::format support

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-18 20:57:23 -08:00
Nikolaj Bjorner
3dd466d4f1 remove RCF example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2026-02-18 20:57:14 -08:00
Nuno Lopes
3dd21d481b fix build 2026-02-18 20:57:14 -08:00