tests.yml

name: Proof Replay

on: [ push ]

permissions:
    checks: write

jobs:
    compile_and_test:
        runs-on: ubuntu-latest
        steps:
            -   uses: actions/checkout@v3
            -   name: Set up JDK 21
                uses: actions/setup-java@v3
                with:
                    java-version: 21
                    distribution: 'corretto'
            -   name: Build with Gradle
                uses: gradle/gradle-build-action@v2.4.2
                with:
                    arguments: --continue assemble check

    replay-proofs:
        strategy:
            fail-fast: false
            matrix:
                target: [ check-overflow-methods, check-overflow-constructors, check-methods, check-constructors ]
        runs-on: ubuntu-latest
        steps:
            -   uses: actions/checkout@v3
            -   name: Set up JDK 21
                uses: actions/setup-java@v3
                with:
                    java-version: 21
                    distribution: 'corretto'
            -   name: Install SMT-Solvers
                run: .github/dlsmt.sh
                shell: bash                    
            -   name: "Verify with KeY ${{ matrix.target }}"
                run: make ${{ matrix.target }}