mirror of
https://github.com/Z3Prover/z3
synced 2026-07-21 22:45:51 +00:00
b39692a643
Bumps [actions/setup-dotnet](https://github.com/actions/setup-dotnet) from 5 to 6. <details> <summary>Release notes</summary> <p><em>Sourced from <a href="https://github.com/actions/setup-dotnet/releases">actions/setup-dotnet's releases</a>.</em></p> <blockquote> <h2>v6.0.0</h2> <h2>What's Changed</h2> <ul> <li>Migrate to ESM and upgrade dependencies by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/752">actions/setup-dotnet#752</a></li> <li>Bump actions/checkout from 6.0.3 to 7.0.0 by <a href="https://github.com/dependabot"><code>@dependabot</code></a>[bot] in <a href="https://redirect.github.com/actions/setup-dotnet/pull/751">actions/setup-dotnet#751</a></li> <li>chore(deps): bump <code>@actions/cache</code> to 6.2.0 by <a href="https://github.com/philip-gai"><code>@philip-gai</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/756">actions/setup-dotnet#756</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/philip-gai"><code>@philip-gai</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/756">actions/setup-dotnet#756</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-dotnet/compare/v5...v6.0.0">https://github.com/actions/setup-dotnet/compare/v5...v6.0.0</a></p> <h2>v5.4.0</h2> <h2>What's Changed</h2> <h3>Enhancements</h3> <ul> <li>Improve global.json SDK version validation for rollForward by <a href="https://github.com/priyagupta108"><code>@priyagupta108</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/742">actions/setup-dotnet#742</a></li> <li>Pin actions to commit SHAs in workflows by <a href="https://github.com/priya-kinthali"><code>@priya-kinthali</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/744">actions/setup-dotnet#744</a></li> <li>Expand the CSC problem matcher to light up more errors on GitHub. by <a href="https://github.com/StephenCleary"><code>@StephenCleary</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/717">actions/setup-dotnet#717</a></li> </ul> <h3>Documentation</h3> <ul> <li>Docs(action): Explicitly mark all optional inputs with required: false by <a href="https://github.com/kranthipoturaju"><code>@kranthipoturaju</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/737">actions/setup-dotnet#737</a></li> </ul> <h3>Bug Fixes</h3> <ul> <li>Fix global.json creation command by <a href="https://github.com/michal2612"><code>@michal2612</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/694">actions/setup-dotnet#694</a></li> </ul> <h3>Dependency Updates</h3> <ul> <li>Upgrade <code>@actions/cache</code> to 5.1.0, log cache write denied by <a href="https://github.com/jasongin"><code>@jasongin</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/746">actions/setup-dotnet#746</a></li> </ul> <h2>New Contributors</h2> <ul> <li><a href="https://github.com/jasongin"><code>@jasongin</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/746">actions/setup-dotnet#746</a></li> <li><a href="https://github.com/michal2612"><code>@michal2612</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/694">actions/setup-dotnet#694</a></li> <li><a href="https://github.com/kranthipoturaju"><code>@kranthipoturaju</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/737">actions/setup-dotnet#737</a></li> <li><a href="https://github.com/StephenCleary"><code>@StephenCleary</code></a> made their first contribution in <a href="https://redirect.github.com/actions/setup-dotnet/pull/717">actions/setup-dotnet#717</a></li> </ul> <p><strong>Full Changelog</strong>: <a href="https://github.com/actions/setup-dotnet/compare/v5...v5.4.0">https://github.com/actions/setup-dotnet/compare/v5...v5.4.0</a></p> <h2>v5.3.0</h2> <h2>What's Changed</h2> <h3>Enhancements</h3> <ul> <li>Add dotnet-version: latest support with dotnet-channel input by <a href="https://github.com/mahabaleshwars"><code>@mahabaleshwars</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/730">actions/setup-dotnet#730</a></li> <li>Support global.json's rollForward latest* variants by <a href="https://github.com/js6pak"><code>@js6pak</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/538">actions/setup-dotnet#538</a></li> <li>Improve version resolution by <a href="https://github.com/akoeplinger"><code>@akoeplinger</code></a> in <a href="https://redirect.github.com/actions/setup-dotnet/pull/560">actions/setup-dotnet#560</a></li> </ul> <h3>Dependency Updates</h3> <!-- raw HTML omitted --> </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href="a98b56852c"><code>a98b568</code></a> chore(deps): bump <code>@actions/cache</code> to 6.2.0 (<a href="https://redirect.github.com/actions/setup-dotnet/issues/756">#756</a>)</li> <li><a href="afb2931642"><code>afb2931</code></a> Bump actions/checkout from 6.0.3 to 7.0.0 (<a href="https://redirect.github.com/actions/setup-dotnet/issues/751">#751</a>)</li> <li><a href="6df8cefd14"><code>6df8cef</code></a> Migrate to ESM and upgrade dependencies (<a href="https://redirect.github.com/actions/setup-dotnet/issues/752">#752</a>)</li> <li>See full diff in <a href="https://github.com/actions/setup-dotnet/compare/v5...v6">compare view</a></li> </ul> </details> <br /> [](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) --- <details> <summary>Dependabot commands and options</summary> <br /> You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot show <dependency name> ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself) </details> Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
940 lines
32 KiB
YAML
940 lines
32 KiB
YAML
name: Nightly Build Validation
|
|
|
|
on:
|
|
workflow_run:
|
|
workflows: ["Nightly Build"]
|
|
types:
|
|
- completed
|
|
workflow_dispatch:
|
|
inputs:
|
|
release_tag:
|
|
description: 'Release tag to validate (default: Nightly)'
|
|
required: false
|
|
default: 'Nightly'
|
|
|
|
permissions:
|
|
contents: read
|
|
|
|
jobs:
|
|
# ============================================================================
|
|
# VALIDATION JOBS FOR NUGET PACKAGES
|
|
# ============================================================================
|
|
|
|
validate-nuget-windows-x64:
|
|
name: "Validate NuGet on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v6
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Create test project
|
|
shell: pwsh
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
$nupkgFile = Get-ChildItem ../nuget-packages/*.nupkg -Exclude *.symbols.nupkg | Select-Object -First 1
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
shell: pwsh
|
|
run: |
|
|
@"
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
"@ | Out-File -FilePath test-nuget/Program.cs -Encoding utf8
|
|
|
|
- name: Run test
|
|
shell: pwsh
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-ubuntu-x64:
|
|
name: "Validate NuGet on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v6
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-macos-x64:
|
|
name: "Validate NuGet on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v6
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-macos-arm64:
|
|
name: "Validate NuGet on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v6
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
# ============================================================================
|
|
# VALIDATION JOBS FOR EXECUTABLES
|
|
# ============================================================================
|
|
|
|
validate-exe-windows-x64:
|
|
name: "Validate executable on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download Windows x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x64-win*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath z3-test
|
|
$z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
|
|
& "$z3Dir/bin/z3.exe" --version
|
|
|
|
# Test basic SMT solving
|
|
@"
|
|
(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)
|
|
"@ | & "$z3Dir/bin/z3.exe" -in
|
|
|
|
validate-exe-windows-x86:
|
|
name: "Validate executable on Windows x86"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download Windows x86 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x86-win*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x86-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath z3-test
|
|
$z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
|
|
& "$z3Dir/bin/z3.exe" --version
|
|
|
|
# Test basic SMT solving
|
|
@"
|
|
(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)
|
|
"@ | & "$z3Dir/bin/z3.exe" -in
|
|
|
|
validate-exe-ubuntu-x64:
|
|
name: "Validate executable on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download Ubuntu x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*x64-glibc*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-glibc*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
validate-exe-macos-x64:
|
|
name: "Validate executable on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download macOS x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*x64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
validate-exe-macos-arm64:
|
|
name: "Validate executable on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download macOS ARM64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
# ============================================================================
|
|
# REGRESSION TEST VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-regressions-ubuntu:
|
|
name: "Validate regression tests on Ubuntu"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Ubuntu x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*x64-glibc*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-glibc*.zip
|
|
cd ..
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
run: |
|
|
Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
|
|
chmod +x $Z3_PATH
|
|
python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2
|
|
|
|
validate-regressions-windows:
|
|
name: "Validate regression tests on Windows"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Windows x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x64-win*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath downloads
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
shell: pwsh
|
|
run: |
|
|
$z3Path = Get-ChildItem downloads -Filter z3.exe -Recurse | Select-Object -First 1
|
|
python z3test/scripts/test_benchmarks.py $z3Path.FullName z3test/regressions/smt2
|
|
|
|
validate-regressions-macos:
|
|
name: "Validate regression tests on macOS"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download macOS ARM64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
cd ..
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
run: |
|
|
Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
|
|
chmod +x $Z3_PATH
|
|
python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2
|
|
|
|
# ============================================================================
|
|
# PYTHON WHEEL VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-python-wheel-ubuntu-x64:
|
|
name: "Validate Python wheel on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*manylinux*x86_64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-macos-arm64:
|
|
name: "Validate Python wheel on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*macosx*arm64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-macos-x64:
|
|
name: "Validate Python wheel on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*macosx*x86_64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-windows-x64:
|
|
name: "Validate Python wheel on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*win_amd64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
shell: pwsh
|
|
run: |
|
|
$wheel = Get-ChildItem wheels/*.whl | Select-Object -First 1
|
|
pip install $wheel.FullName
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-riscv64:
|
|
name: "Validate Python wheel for RISC-V 64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download RISC-V 64 Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*riscv64.whl" --dir wheels
|
|
|
|
- name: Verify wheel platform tag and contents
|
|
run: |
|
|
pip install wheel
|
|
WHEEL_FILE=$(ls wheels/*.whl | head -n 1)
|
|
echo "Wheel file: $WHEEL_FILE"
|
|
|
|
# Check that the wheel has a riscv64 platform tag
|
|
WHEEL_NAME=$(basename $WHEEL_FILE)
|
|
echo "Wheel name: $WHEEL_NAME"
|
|
if echo "$WHEEL_NAME" | grep -q "riscv64"; then
|
|
echo "riscv64 platform tag found"
|
|
else
|
|
echo "ERROR: riscv64 platform tag not found in wheel name"
|
|
exit 1
|
|
fi
|
|
|
|
# Inspect wheel contents
|
|
python -m zipfile -l $WHEEL_FILE
|
|
|
|
# Verify wheel contains z3 library
|
|
if python -m zipfile -l $WHEEL_FILE | grep -q "libz3"; then
|
|
echo "libz3 found in wheel"
|
|
else
|
|
echo "ERROR: libz3 not found in wheel"
|
|
exit 1
|
|
fi
|
|
|
|
# ============================================================================
|
|
# MACOS DYLIB HEADERPAD VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-macos-headerpad-x64:
|
|
name: "Validate macOS x64 dylib headerpad"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download macOS x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*x64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
|
|
|
|
- name: Test install_name_tool with headerpad
|
|
run: |
|
|
cd downloads/$Z3_DIR/bin
|
|
|
|
# Get the original install name
|
|
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "Original install name: $ORIGINAL_NAME"
|
|
|
|
# Create a test path with same length as typical setup-z3 usage
|
|
# This simulates what setup-z3 does: changing to absolute path
|
|
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib"
|
|
|
|
# Try to change the install name - this will fail if headerpad is insufficient
|
|
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
|
|
|
|
# Verify the change was successful
|
|
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "New install name: $NEW_NAME"
|
|
|
|
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
|
|
echo "✓ install_name_tool succeeded - headerpad is sufficient"
|
|
else
|
|
echo "✗ install_name_tool failed to update install name"
|
|
exit 1
|
|
fi
|
|
|
|
validate-macos-headerpad-arm64:
|
|
name: "Validate macOS ARM64 dylib headerpad"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download macOS ARM64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
|
|
|
|
- name: Test install_name_tool with headerpad
|
|
run: |
|
|
cd downloads/$Z3_DIR/bin
|
|
|
|
# Get the original install name
|
|
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "Original install name: $ORIGINAL_NAME"
|
|
|
|
# Create a test path with same length as typical setup-z3 usage
|
|
# This simulates what setup-z3 does: changing to absolute path
|
|
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib"
|
|
|
|
# Try to change the install name - this will fail if headerpad is insufficient
|
|
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
|
|
|
|
# Verify the change was successful
|
|
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "New install name: $NEW_NAME"
|
|
|
|
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
|
|
echo "✓ install_name_tool succeeded - headerpad is sufficient"
|
|
else
|
|
echo "✗ install_name_tool failed to update install name"
|
|
exit 1
|
|
fi
|
|
|
|
# ============================================================================
|
|
# BUILD SCRIPT UNIT TESTS
|
|
# ============================================================================
|
|
|
|
validate-build-script-tests:
|
|
name: "Validate build script unit tests"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 10
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Run build script unit tests
|
|
run: python -m unittest discover -s scripts/tests -p "test_*.py" -v
|
|
|
|
# ============================================================================
|
|
# DOTNET MANAGED WRAPPER ARCHITECTURE VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-dotnet-anycpu:
|
|
name: "Validate Microsoft.Z3.dll is AnyCPU (issue #9863)"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 15
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v7.0.0
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
run: |
|
|
TAG="${{ github.event.inputs.release_tag }}"
|
|
if [ -z "$TAG" ]; then
|
|
TAG="Nightly"
|
|
fi
|
|
gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Extract managed DLL from NuGet package
|
|
run: |
|
|
# NuGet packages are ZIP archives; exclude the symbols package
|
|
NUPKG=$(ls nuget-packages/*.nupkg | grep -v '\.symbols\.' | grep -v '\.snupkg' | head -n 1)
|
|
echo "Checking package: $NUPKG"
|
|
unzip -q "$NUPKG" "lib/netstandard2.0/Microsoft.Z3.dll" -d nupkg-extracted
|
|
|
|
- name: Check PE Machine field is AnyCPU (not architecture-specific)
|
|
run: |
|
|
python3 - <<'EOF'
|
|
import struct
|
|
import sys
|
|
|
|
dll_path = "nupkg-extracted/lib/netstandard2.0/Microsoft.Z3.dll"
|
|
|
|
with open(dll_path, 'rb') as f:
|
|
# Verify MZ magic
|
|
if f.read(2) != b'MZ':
|
|
print("ERROR: Not a valid PE file (missing MZ header)")
|
|
sys.exit(1)
|
|
|
|
# Read PE header offset stored at 0x3C in the DOS stub
|
|
f.seek(0x3C)
|
|
pe_offset = struct.unpack('<I', f.read(4))[0]
|
|
|
|
# Verify PE signature
|
|
f.seek(pe_offset)
|
|
if f.read(4) != b'PE\x00\x00':
|
|
print("ERROR: Missing PE\\0\\0 signature")
|
|
sys.exit(1)
|
|
|
|
# COFF Machine field is the 2 bytes immediately after the PE signature
|
|
machine = struct.unpack('<H', f.read(2))[0]
|
|
|
|
machine_names = {
|
|
0x0000: "Unknown/AnyCPU",
|
|
0x014C: "i386 (AnyCPU for managed assemblies)",
|
|
0x8664: "AMD64/x64",
|
|
0xAA64: "ARM64",
|
|
0x01C0: "ARM",
|
|
0x01C4: "ARM Thumb-2",
|
|
}
|
|
machine_name = machine_names.get(machine, f"0x{machine:04X}")
|
|
print(f"Machine field: 0x{machine:04X} = {machine_name}")
|
|
|
|
if machine == 0x8664:
|
|
print()
|
|
print("FAIL: Machine is AMD64 (0x8664).")
|
|
print("This prevents loading on arm64 .NET hosts even though the assembly")
|
|
print("contains only pure IL (CorFlags.ILONLY=True).")
|
|
print("The DLL must be built as AnyCPU (Machine=0x014C) so the CLR loader")
|
|
print("accepts it on every host architecture.")
|
|
print("See issue #9863 for details.")
|
|
sys.exit(1)
|
|
elif machine == 0xAA64:
|
|
print()
|
|
print("FAIL: Machine is ARM64 (0xAA64).")
|
|
print("This prevents loading on x64 .NET hosts.")
|
|
print("The DLL must be built as AnyCPU (Machine=0x014C).")
|
|
sys.exit(1)
|
|
elif machine in (0x014C, 0x0000):
|
|
print()
|
|
print("PASS: Machine field indicates AnyCPU.")
|
|
print("Microsoft.Z3.dll will load on any .NET host architecture.")
|
|
else:
|
|
print()
|
|
print(f"FAIL: Unexpected Machine field 0x{machine:04X}.")
|
|
print("Expected 0x014C (i386/AnyCPU) for a managed-only assembly.")
|
|
sys.exit(1)
|
|
EOF
|