This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Z3 Trace Log Generator | |
| on: | |
| push: | |
| branches: [ "main" ] | |
| # only triggers job when smt2 files are changed (added/removed/modified) in a push | |
| paths: | |
| - '**/*.smt2' | |
| # job can also be triggered manually on GitHub | |
| workflow_dispatch: | |
| jobs: | |
| generate_log: | |
| strategy: | |
| matrix: | |
| versions: | |
| - {z3: '4.12.2', installz3: 'v1.3'} | |
| - {z3: '4.10.0', installz3: 'v1.3'} | |
| - {z3: '4.8.7', installz3: '1.2.2'} | |
| # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2 | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 # this copies the whole repository | |
| with: | |
| fetch-depth: 0 # needed, see GitHub Action "Changed Files" | |
| - name: Install Z3 | |
| if: ${{ matrix.versions.installz3 }} == 'v1.3' | |
| uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3" | |
| with: | |
| version: ${{ matrix.versions.z3 }} | |
| - name: Install Z3 | |
| if: ${{ matrix.versions.installz3 }} == '1.2.2' | |
| uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3" | |
| with: | |
| version: ${{ matrix.versions.z3 }} | |
| # this fetches all changed (added/modified) smt2 files in the repository | |
| - name: Fetch changed smt2 files | |
| id: changed-smt2-files | |
| uses: tj-actions/[email protected] # see GitHub Action "Changed Files" | |
| with: | |
| files_yaml: | | |
| smt: | |
| - '**/*.smt2' | |
| - name: Run Z3 solver on changed smt2 files and compress | |
| id: run_z3_and_upload | |
| run: | | |
| # Create the 'logs' directory | |
| mkdir logs | |
| # Loop through the files | |
| for file in ${{ steps.changed-smt2-files.outputs.smt_all_changed_files }}; do | |
| echo "Processing $file" | |
| # Get the filename without extension | |
| base_name=$(basename "${file%.*}") | |
| # Run Z3 solver for the file and save the log in the 'logs' directory | |
| z3 trace=true proof=true trace-file-name=logs/${base_name}.log ./$file | |
| done | |
| # Compress the 'logs' directory using bzip2 | |
| # z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g') | |
| z3_v_clean=$(echo "${{ matrix.versions.z3 }}" | sed 's/\./_/g') | |
| tar -cjf logs_z3_v${z3_v_clean}.tar.bz2 logs/ | |
| echo "logs_path=$(realpath logs_z3_v${z3_v_clean}.tar.bz2)" >> $GITHUB_OUTPUT | |
| - name: Upload build artifacts | |
| uses: actions/[email protected] | |
| with: | |
| name: "logs_z3_v${{ matrix.versions.z3 }}" | |
| path: ${{ steps.run_z3_and_upload.outputs.logs_path }} |