name: Uclid5-based Verifier Tests

on:
  # Trigger this workflow also on workflow_call events.
  workflow_call:
    inputs:
      compiler-ref:
        required: false
        type: string
      runtime-ref:
        required: false
        type: string

jobs:
  run:
    strategy:
      matrix:
        platform: [ubuntu-24.04]
    runs-on: ${{ matrix.platform }}
    steps:
      - name: Check out lingua-franca repository
        uses: actions/checkout@v3
        with:
          repository: lf-lang/lingua-franca
          submodules: true
          ref: ${{ inputs.compiler-ref }}
          fetch-depth: 0
      - name: Prepare build environment
        uses: ./.github/actions/prepare-build-env
      - name: Check out specific ref of reactor-c
        uses: actions/checkout@v3
        with:
          repository: lf-lang/reactor-c
          path: core/src/main/resources/lib/c/reactor-c
          ref: ${{ inputs.runtime-ref }}
        if: ${{ inputs.runtime-ref }}
      - name: Setup Scala
        uses: olafurpg/setup-scala@v11
        with:
          java-version: openjdk@1.17.0
      - name: Check out Uclid5 repository
        uses: actions/checkout@v3
        with:
          repository: uclid-org/uclid
          ref: 4fd5e566c5f87b052f92e9b23723a85e1c4d8c1c
          path: uclid
      - name: Download Z3
        working-directory: uclid/
        if: steps.cache-z3.outputs.cache-hit != 'true'
        run: ./get-z3-linux.sh
      - name: Add Z3 to Path
        working-directory: uclid/
        run: |
          echo "$(pwd)/z3/bin/" >> $GITHUB_PATH
          echo "LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(pwd)/z3/bin/" >> $GITHUB_ENV
      - name: Print Z3 Version
        run: z3 --version
      - name: Install Uclid5
        working-directory: uclid/
        run: |

          sbt update clean compile
          sbt universal:packageBin
          cd target/universal/
          unzip uclid-0.9.5.zip
          ./uclid-0.9.5/bin/uclid --help
          echo "$(pwd)/uclid-0.9.5/bin" >> $GITHUB_PATH
          cd ../..
      - name: Run verifier tests
        run: |
          echo "$pwd"
          ls -la
          ./gradlew core:integrationTest --tests org.lflang.tests.runtime.CVerifierTest.* core:integrationTestCodeCoverageReport
      - name: Report to CodeCov
        uses: ./.github/actions/report-code-coverage
        with:
          files: core/build/reports/jacoco/integrationTestCodeCoverageReport/integrationTestCodeCoverageReport.xml
        if: ${{ github.repository == 'lf-lang/lingua-franca' }}
