Add workflow to build and cache Z3 for reuse across CI (#8466)

* Initial plan

* Add Z3 build cache workflow and documentation

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

* Address code review feedback: improve cache strategy and documentation

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

* Fix cache restore-keys and update size documentation

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

* Delete .github/workflows/example-cached-z3.yml

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

.github/workflows/README-build-cache.md

@@ -0,0 +1,222 @@
+# Z3 Build Cache Workflow
+
+This workflow builds Z3 and caches the built binaries for use by other workflows, eliminating the need for repeated builds and saving significant CI time.
+
+## Purpose
+
+The `build-z3-cache.yml` workflow:
+1. Builds Z3 from source using the Python build system
+2. Caches the built binaries and libraries
+3. Can be triggered manually, on schedule, or on pushes to main
+4. Can be called as a reusable workflow from other workflows
+
+## Cache Contents
+
+The workflow caches:
+- `build/z3` - Main Z3 executable
+- `build/libz3.so` and `build/libz3.a` - Z3 libraries
+- `build/*.so` and `build/*.a` - Additional library files
+- `build/python` - Python bindings
+
+## Cache Key Format
+
+The cache key is: `z3-build-{OS}-{git-sha}`
+
+**How it works:**
+- Each commit gets its own cache entry based on its git SHA
+- When restoring, the `restore-keys` pattern allows falling back to caches from previous commits
+- The most recent cache matching the `restore-keys` pattern will be used if an exact key match isn't found
+- This means workflows typically restore from a recent build and save a new cache for the current commit
+
+**Example:**
+- A workflow on commit `abc123` will look for `z3-build-Linux-abc123`
+- If not found, it falls back to the most recent `z3-build-Linux-*` cache
+- After building, it saves a new cache with key `z3-build-Linux-abc123`
+
+This ensures:
+- Caches are OS-specific
+- Each new commit can reuse builds from recent commits
+- The cache stays relatively up-to-date with the repository
+
+## Using the Cached Build
+
+### Option 1: Direct Cache Restore (Recommended)
+
+Add these steps to your workflow before you need to use Z3:
+
+```yaml
+- name: Checkout code
+  uses: actions/checkout@v6
+
+- name: Setup Python
+  uses: actions/setup-python@v6
+  with:
+    python-version: '3.x'
+
+- name: Restore Z3 cache
+  id: cache-z3
+  uses: actions/cache/restore@v4
+  with:
+    path: |
+      build/z3
+      build/libz3.so
+      build/libz3.a
+      build/*.so
+      build/*.a
+      build/python
+    key: z3-build-${{ runner.os }}-${{ github.sha }}
+    restore-keys: |
+      z3-build-${{ runner.os }}-
+
+- name: Build Z3 (if not cached)
+  if: steps.cache-z3.outputs.cache-hit != 'true'
+  run: |
+    python scripts/mk_make.py
+    cd build
+    make -j$(nproc)
+
+- name: Verify Z3 is available
+  run: |
+    build/z3 --version
+```
+
+### Option 2: Call as Reusable Workflow
+
+You can also call this workflow before your job:
+
+```yaml
+jobs:
+  build-cache:
+    uses: ./.github/workflows/build-z3-cache.yml
+
+  your-job:
+    needs: build-cache
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Restore Z3 cache
+        uses: actions/cache/restore@v4
+        with:
+          path: |
+            build/z3
+            build/libz3.so
+            build/libz3.a
+            build/*.so
+            build/*.a
+            build/python
+          key: ${{ needs.build-cache.outputs.cache-key }}
+      
+      - name: Use Z3
+        run: build/z3 --version
+```
+
+## Benefits
+
+- **Time Savings**: Eliminates 15-17 minute build time when cache hit
+- **Resource Efficiency**: Reduces CI compute usage
+- **Reliability**: Ensures consistent Z3 binary across workflow runs
+- **Flexibility**: Works with manual triggers, schedules, and pushes
+
+## Example: Soundness Bug Detector
+
+The soundness bug detector workflow can now use cached Z3:
+
+```yaml
+name: Soundness Bug Detector
+
+on:
+  schedule:
+    - cron: '0 4 * * *'
+
+jobs:
+  detect-bugs:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+
+      - name: Setup Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3.x'
+
+      - name: Restore Z3 cache
+        uses: actions/cache/restore@v4
+        with:
+          path: |
+            build/z3
+            build/libz3.so
+            build/libz3.a
+            build/*.so
+            build/*.a
+            build/python
+          key: z3-build-${{ runner.os }}-${{ github.sha }}
+          restore-keys: |
+            z3-build-${{ runner.os }}-
+
+      - name: Build Z3 (if not cached)
+        run: |
+          if [ ! -f build/z3 ]; then
+            python scripts/mk_make.py
+            cd build
+            make -j$(nproc)
+          fi
+
+      - name: Test soundness issues
+        run: |
+          # Now Z3 is available at build/z3
+          build/z3 --version
+          # ... rest of soundness testing logic
+```
+
+## Cache Maintenance
+
+**GitHub Actions Cache Policies:**
+- **Retention**: Caches are removed after 7 days without being accessed
+- **Repository Limit**: Total cache size per repository is limited to 10GB
+- **Eviction**: Least Recently Used (LRU) caches are evicted when the limit is reached
+- **Size per Entry**: Each Z3 build cache is approximately 70MB (z3 executable, libz3 libraries, and Python bindings)
+
+**This Workflow's Strategy:**
+- **Daily Schedule**: Runs daily at 2 AM UTC to refresh the cache
+- **Push Trigger**: Updates cache on pushes to master/main branches  
+- **Manual Trigger**: Can be triggered manually via workflow_dispatch
+
+**Best Practices:**
+- The daily schedule ensures at least one cache is always available (within 7-day retention)
+- Multiple commits may share the same cache via the `restore-keys` fallback pattern
+- If you need guaranteed cache availability for a specific commit, manually trigger the workflow
+
+## Troubleshooting
+
+### Cache miss on every run
+
+If you're getting cache misses, check:
+1. The cache key format matches between save and restore
+2. The git SHA is consistent (use the same checkout before restore)
+3. The runner OS matches
+
+### Build not working after restore
+
+After restoring from cache:
+1. Verify all library files are present: `ls -la build/`
+2. Check library dependencies: `ldd build/z3`
+3. Ensure Python bindings are in the correct location
+
+### Need different build configuration
+
+If you need a different Z3 build (e.g., with debug symbols), you can:
+1. Create a separate cache workflow with a different cache key
+2. Or build Z3 directly in your workflow with custom flags
+
+## Related Workflows
+
+- `ci.yml` - Main CI workflow (could benefit from caching)
+- `soundness-bug-detector.lock.yml` - Automated soundness testing
+- `nightly.yml` - Nightly builds (uses its own build process)
+
+## Implementation Note
+
+This addresses the recommendation from [GitHub Discussion #8458](https://github.com/Z3Prover/z3/discussions/8458), which identified that the soundness bug detector and other workflows were unable to test properly due to missing Z3 binaries and build tool limitations.

.github/workflows/build-z3-cache.yml

@@ -0,0 +1,79 @@
+name: Build and Cache Z3
+
+on:
+  # Allow manual trigger
+  workflow_dispatch:
+  # Run on schedule to keep cache fresh (daily at 2 AM UTC)
+  schedule:
+    - cron: '0 2 * * *'
+  # Run on pushes to main to update cache with latest changes
+  push:
+    branches: [ "master", "main" ]
+  # Make this callable as a reusable workflow
+  workflow_call:
+    outputs:
+      cache-key:
+        description: "The cache key for the built Z3 binary"
+        value: ${{ jobs.build-z3.outputs.cache-key }}
+
+permissions:
+  contents: read
+
+jobs:
+  build-z3:
+    name: "Build Z3 for caching"
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    outputs:
+      cache-key: ${{ steps.cache-key.outputs.key }}
+    
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+
+      - name: Setup Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3.x'
+
+      - name: Generate cache key
+        id: cache-key
+        run: |
+          # Create a cache key based on git SHA and relevant source files
+          echo "key=z3-build-${{ runner.os }}-${{ github.sha }}" >> $GITHUB_OUTPUT
+          echo "fallback-key=z3-build-${{ runner.os }}-" >> $GITHUB_OUTPUT
+
+      - name: Restore or create cache
+        id: cache-z3
+        uses: actions/cache@v4
+        with:
+          path: |
+            build/z3
+            build/libz3.so
+            build/libz3.a
+            build/*.so
+            build/*.a
+            build/python
+          key: ${{ steps.cache-key.outputs.key }}
+          restore-keys: |
+            z3-build-${{ runner.os }}-
+
+      - name: Configure Z3
+        if: steps.cache-z3.outputs.cache-hit != 'true'
+        run: python scripts/mk_make.py
+
+      - name: Build Z3
+        if: steps.cache-z3.outputs.cache-hit != 'true'
+        run: |
+          cd build
+          make -j$(nproc)
+
+      - name: Display build info
+        run: |
+          echo "Cache key: ${{ steps.cache-key.outputs.key }}"
+          echo "Build directory contents:"
+          ls -lh build/ || echo "Build directory not found"
+          if [ -f build/z3 ]; then
+            echo "Z3 version:"
+            build/z3 --version
+          fi