z3/.github/workflows/nightly-validation.yml

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
      
      - name: Setup .NET
        uses: actions/setup-dotnet@v5
        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
      
      - name: Setup .NET
        uses: actions/setup-dotnet@v5
        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
      
      - name: Setup .NET
        uses: actions/setup-dotnet@v5
        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
      
      - name: Setup .NET
        uses: actions/setup-dotnet@v5
        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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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
      
      - 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

      - 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

      - 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