pull-request-checks.yaml

name: Build and Test CBMC
on:
  push:
    branches: [ develop ]
  pull_request:
    branches: [ develop ]
env:
  cvc5-version: "1.3.4"
  z3-version: "4.8.10"
  linux-vcpus: 4
  windows-vcpus: 4

jobs:
  # This job takes approximately 15 to 40 minutes
  check-ubuntu-24_04-make-gcc:
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-make-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-make-${{ github.ref }}
            ${{ runner.os }}-24.04-make
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with make
        run: |
          git clone https://github.com/conp-solutions/riss riss.git
          cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release -DCMAKE_POLICY_VERSION_MINIMUM=3.5
          make -C riss.git/release riss-coprocessor-lib-static -j${{env.linux-vcpus}}
          make -C src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
          make -C jbmc/src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss

          make -C unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss

          make -C jbmc/unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
      - name: Print ccache stats
        run: ccache -s
      - name: Checking completeness of help output
        run: scripts/check_help.sh g++
      - name: Run unit tests
        run: |
          make -C unit test IPASIR=$PWD/riss.git/riss
          make -C jbmc/unit test IPASIR=$PWD/riss.git/riss
          echo "Running expected failure tests"
          make TAGS="[!shouldfail]" -C unit test IPASIR=$PWD/riss.git/riss
          make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
      - name: Run regression tests
        run: |
          export PATH=$PATH:`pwd`/src/solvers
          make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
          make -C regression/cbmc test-paths-lifo
          make -C regression/cbmc test-cprover-smt2
          make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
      - name: Check cleanup
        run: |
          make -C src clean IPASIR=$PWD/riss.git/riss
          make -C jbmc/src clean IPASIR=$PWD/riss.git/riss
          rm -r riss.git
          rm src/goto-cc/goto-ld
          make -C unit clean
          make -C regression clean
          make -C jbmc/unit clean
          make -C jbmc/regression clean
          if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
            git status --ignored
            exit 1
          fi

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 25 to 34 minutes
  check-ubuntu-24_04-make-clang:
    runs-on: ubuntu-24.04
    env:
      CC: "ccache /usr/bin/clang"
      CXX: "ccache /usr/bin/clang++"
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
          make -C src minisat2-download cadical-download
          cpanm Thread::Pool::Simple
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-make-clang-${{ github.ref }}
            ${{ runner.os }}-24.04-make-clang
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with make
        run: |
          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
          make -C unit      -j${{env.linux-vcpus}}
          make -C jbmc/src  -j${{env.linux-vcpus}}
          make -C jbmc/unit -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run unit tests
        run: |
          make -C unit      test
          make -C jbmc/unit test
          make TAGS="[z3]" -C unit test
      - name: Run expected failure unit tests
        run: |
          make TAGS="[!shouldfail]" -C unit test
          make TAGS="[!shouldfail]" -C jbmc/unit test
      - name: Run regression tests
        run: |
          export PATH=$PATH:`pwd`/src/solvers
          make -C regression test-parallel JOBS=${{env.linux-vcpus}}
          make -C regression/cbmc test-paths-lifo
          make -C regression/cbmc test-cprover-smt2
          make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job has been copied from the one above it, and modified to only build CBMC
  # and run the `regression/cbmc/` regression tests against Z3. The rest of the tests
  # (unit/regression) have been stripped based on the rationale that they are going
  # to be run by the job above, which is basically the same, but more comprehensive.
  # The reason we opted for a new job is that adding a `test-z3` step to the current
  # jobs increases the job runtime to unacceptable levels (over 2hrs).
  # This job takes approximately 3 to 18 minutes
  check-ubuntu-24_04-make-clang-smt-z3:
    runs-on: ubuntu-24.04
    env:
      CC: "ccache /usr/bin/clang"
      CXX: "ccache /usr/bin/clang++"
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
          make -C src minisat2-download
          cpanm Thread::Pool::Simple
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-make-clang-${{ github.ref }}
            ${{ runner.os }}-24.04-make-clang
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with make
        run: make -C src -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run regression/cbmc tests with z3 as the backend
        run: make -C regression/cbmc test-z3

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 17 to 42 minutes
  check-ubuntu-24_04-cmake-gcc:
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-Release-${{ github.ref }}
            ${{ runner.os }}-24.04-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: Check that doc task works
        run: ninja -C build doc
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Checking completeness of help output
        run: scripts/check_help.sh /usr/bin/g++ build/bin
      - name: Check if package building works
        run: |
          cd build
          ninja package
          ls *.deb
      - name: Run tests
        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
      - name: Check cleanup
        run: |
          cmake --build build --target clean
          rm -r build
          find regression jbmc/regression \( -name '*.out' -o -name '*.gb' -o -name '*.dimacs' -o -name '*.obj' -o -name '*.o' -o -name '*.goto-cc-saved' \) -delete
          find regression -not -path 'regression/goto-bmc/invalid-files/*' -name '*.goto' -delete
          find regression/cbmc regression/cbmc-incr-smt2 regression/cbmc-sequentialization regression/cbmc-shadow-memory regression/book-examples regression/statement-list -name '*.smt2' -delete
          find regression/snapshot-harness regression/solver-hardness -name '*.json' -delete
          find regression/goto-harness -name '*-harness.c' -delete
          find regression/goto-instrument-wmm-core -mindepth 2 \( -name '*.txt' -o -name '*.dot' \) -delete
          rm -rf jbmc/regression/jbmc/classpath-class-incorrect-package/incorrect-classes
          rm -rf jbmc/regression/jbmc/classpath-class-with-one-dir/default-classes
          rm -rf jbmc/regression/jbmc/overlay-class/annotations jbmc/regression/jbmc/overlay-class/correct-overlay jbmc/regression/jbmc/overlay-class/ignored-method jbmc/regression/jbmc/overlay-class/unmarked-overlay
          rm -f jbmc/regression/jbmc/overlay-class/Test.class
          if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
            git status --ignored
            exit 1
          fi

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 20 to 38 minutes
  check-ubuntu-22_04-make-clang:
    runs-on: ubuntu-22.04
    env:
      CC: "ccache /usr/bin/clang"
      CXX: "ccache /usr/bin/clang++"
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
          make -C src minisat2-download cadical-download
          cpanm Thread::Pool::Simple
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-22.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-22.04-make-clang-${{ github.ref }}
            ${{ runner.os }}-22.04-make-clang
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Perform C/C++ library syntax check
        run: |
          make -C src/ansi-c library_check
          make -C src/cpp library_check
      - name: Build with make
        run: |
          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
          make -C unit      -j${{env.linux-vcpus}}
          make -C jbmc/src  -j${{env.linux-vcpus}}
          make -C jbmc/unit -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run unit tests
        run: |
          make -C unit      test
          make -C jbmc/unit test
          make TAGS="[z3]" -C unit test
      - name: Run expected failure unit tests
        run: |
          make TAGS="[!shouldfail]" -C unit test
          make TAGS="[!shouldfail]" -C jbmc/unit test
      - name: Run regression tests
        run: |
          export PATH=$PATH:`pwd`/src/solvers
          make -C regression test-parallel JOBS=${{env.linux-vcpus}}
          make -C regression/cbmc test-paths-lifo
          make -C regression/cbmc test-cprover-smt2
          make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 17 to 41 minutes
  check-ubuntu-22_04-cmake-gcc:
    runs-on: ubuntu-22.04
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-22.04-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-22.04-Release-${{ github.ref }}
            ${{ runner.os }}-22.04-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: Check that doc task works
        run: ninja -C build doc
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Check if package building works
        run: |
          cd build
          ninja package
          ls *.deb
      - name: Run tests
        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 14 to 46 minutes
  check-ubuntu-24_04-cmake-gcc-14:
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
          # Update symlinks so that any use of gcc (including our regression
          # tests) will use GCC 14.
          sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \
            --slave /usr/bin/g++ g++ /usr/bin/g++-14 \
            --slave /usr/bin/gcov gcov /usr/bin/gcov-14
          sudo ln -sf cpp-14 /usr/bin/cpp
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}
            ${{ runner.os }}-24.04-Release-gcc-14
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_FLAGS=-Wp,-D_GLIBCXX_ASSERTIONS
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run tests
        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 17 to 41 minutes
  check-ubuntu-24_04-arm-cmake-gcc:
    runs-on: ubuntu-24.04-arm
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}
            ${{ runner.os }}-24.04-Arm-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: Check that doc task works
        run: ninja -C build doc
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Check if package building works
        run: |
          cd build
          ninja package
          ls *.deb
      - name: Run tests
        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 14 to 60 minutes
  check-ubuntu-22_04-cmake-gcc-32bit:
    runs-on: ubuntu-22.04
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-22.04-Release-32-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-22.04-Release-32-${{ github.ref }}
            ${{ runner.os }}-22.04-Release-32
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_C_FLAGS=-m32 -DCMAKE_CXX_FLAGS=-m32
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run tests
        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 2 to 24 minutes
  check-ubuntu-24_04-cmake-gcc-KNOWNBUG:
    runs-on: ubuntu-24.04
    # Sequenced after check-ubuntu-24_04-cmake-gcc so that this job benefits
    # from the matching ccache produced in the same workflow run. The cmake
    # configure flags below must stay in sync with that job's so the compile
    # commands hash identically and ccache hits in full.
    needs: check-ubuntu-24_04-cmake-gcc
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
      - name: Restore ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-Release-${{ github.ref }}
            ${{ runner.os }}-24.04-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run tests
        run: |
          cd build
          ctest . -V -L KNOWNBUG -j${{env.linux-vcpus}}
          export PATH=$PWD/bin:$PATH
          cd ../regression/cbmc
          sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
          # the following tests fail on Windows only
          git checkout -- memory_allocation1 printf1 printf3 union12 va_list3
          ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K

      # No "Save ccache" step here: the cache is produced by
      # check-ubuntu-24_04-cmake-gcc, which this job depends on.
  # This job takes approximately 7 to 30 minutes
  check-ubuntu-24_04-cmake-gcc-THOROUGH:
    runs-on: ubuntu-24.04
    # Sequenced after check-ubuntu-24_04-cmake-gcc so that this job benefits
    # from the matching ccache produced in the same workflow run. The cmake
    # configure flags below must stay in sync with that job's so the compile
    # commands hash identically and ccache hits in full.
    needs: check-ubuntu-24_04-cmake-gcc
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
      - name: Restore ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-24.04-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-24.04-Release-${{ github.ref }}
            ${{ runner.os }}-24.04-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Configure using CMake
        run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build with Ninja
        run: ninja -C build -j${{env.linux-vcpus}}
      - name: Print ccache stats
        run: ccache -s
      - name: Run tests
        run: cd build; ctest . -V -L THOROUGH -j${{env.linux-vcpus}}

      # No "Save ccache" step here: the cache is produced by
      # check-ubuntu-24_04-cmake-gcc, which this job depends on.
  # This job takes approximately 39 to 69 minutes
  check-macos-15-intel-make-clang:
    runs-on: macos-15-intel
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        run: |
          # maven is already installed and upgrading to a newer version yields
          # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
          brew install flex bison parallel ccache z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-make-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-make-${{ github.ref }}
            ${{ runner.os }}-make
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Build using Make
        run: |
          make -C src minisat2-download cadical-download
          make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
          make -C jbmc/src -j4 CXX="ccache clang++"
          make -C unit "CXX=ccache clang++"
          make -C jbmc/unit "CXX=ccache clang++"
      - name: Print ccache stats
        run: ccache -s
      - name: Run unit tests
        run: |
          cd unit; ./unit_tests
          ./unit_tests "[z3]"
      - name: Run JBMC unit tests
        run: cd jbmc/unit; ./unit_tests
      - name: Run regression tests
        run: |
          export PATH=$PATH:`pwd`/src/solvers
          make -C regression test-parallel JOBS=4
      - name: Run JBMC regression tests
        run: make -C jbmc/regression test-parallel JOBS=4

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 36 to 85 minutes
  check-macos-26-cmake-clang:
    runs-on: macos-26
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        run: brew install ninja maven flex bison ccache z3
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-26-Release-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-26-Release-${{ github.ref }}
            ${{ runner.os }}-26-Release
      - name: ccache environment
        run: |
          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
      - name: Zero ccache stats and limit in size
        run: ccache -z --max-size=500M
      - name: Configure using CMake
        run: |
          mkdir build
          cd build
          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -Dsat_impl=cadical
      - name: Build with Ninja
        run: cd build; ninja -j3
      - name: Print ccache stats
        run: ccache -s
      - name: Run CTest
        run: cd build; ctest -V -L CORE . -j3

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 49 to 70 minutes
  # Note: as of June 2026 the "windows-2025" runner label is being migrated to
  # the Windows Server 2025 image that ships Visual Studio 2026 (MSVC 14.5x)
  # instead of VS 2022/2025 (MSVC 14.4x); see actions/runner-images#14017.
  # During the rollout both images are served under this label, so this job may
  # run on either toolset.
  check-vs-2026-cmake-build-and-test:
    runs-on: windows-2025
    env:
      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Setup Visual Studio environment
        uses: microsoft/setup-msbuild@v3
      - name: Get current month for cache key
        id: cache-key
        run: echo "month=$(Get-Date -Format 'yyyy-MM')" >> $env:GITHUB_OUTPUT
      - name: Cache Chocolatey packages
        uses: actions/cache@v6
        with:
          path: |
            C:\ProgramData\chocolatey\lib\winflexbison3
            C:\ProgramData\chocolatey\bin
          key: ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}-winflexbison3
          restore-keys: |
            ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}
      - name: Fetch dependencies
        run: |
          function Require-Tool($Name) {
            if (-not (Get-Command $Name -ErrorAction SilentlyContinue)) {
              Write-Output "::error ::Required tool '$Name' not found in PATH after Chocolatey installation."
              exit 1
            }
          }
          if (-not (Get-Command win_flex -ErrorAction SilentlyContinue))
          {
            # Only contact the Chocolatey servers when the package is not
            # already present (restored from the cache above or pre-installed on
            # the runner).  This lets the step succeed from cache when the
            # Chocolatey infrastructure is unavailable.
            choco install -y winflexbison3
            if($LastExitCode -ne 0)
            {
              Write-Output "::error ::Dependency installation via Chocolatey failed."
              exit $LastExitCode
            }
          }
          else
          {
            Write-Output "winflexbison3 restored from cache; skipping Chocolatey install."
          }
          Require-Tool win_flex
          Require-Tool win_bison
          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
      - name: Install Z3
        uses: ./.github/actions/install-z3
        with:
          version: ${{ env.z3-version }}
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Confirm cvc5 solver is available and log the version installed
        run: cvc5 --version
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-msbuild-${{ github.ref }}
            ${{ runner.os }}-msbuild
      - name: ccache environment
        run: |
          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
      - name: Configure with cmake
        run: cmake -S . -B build
      - name: Zero ccache stats and limit in size (2 GB)
        run: |
          clcache -z
          clcache -M 2147483648
      - name: Build Release
        run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
      - name: Print ccache stats
        run: clcache -s
      - uses: ilammy/msvc-dev-cmd@v1
      - name: Test cbmc
        run: |
          Set-Location build
          ctest -V -L CORE -C Release . -j${{env.windows-vcpus}}

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 65 to 84 minutes
  check-vs-2022-make-build-and-test:
    runs-on: windows-2022
    env:
      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Setup MSBuild
        uses: microsoft/setup-msbuild@v3
      - name: Get current month for cache key
        id: cache-key
        run: echo "month=$(Get-Date -Format 'yyyy-MM')" >> $env:GITHUB_OUTPUT
      - name: Cache Chocolatey packages
        uses: actions/cache@v6
        with:
          path: |
            C:\ProgramData\chocolatey\lib\winflexbison3
            C:\ProgramData\chocolatey\lib\wget
            C:\ProgramData\chocolatey\bin
          key: ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}-winflexbison3-strawberryperl-wget
          restore-keys: |
            ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}
      - name: Fetch dependencies
        run: |
          function Require-Tool($Name) {
            if (-not (Get-Command $Name -ErrorAction SilentlyContinue)) {
              Write-Output "::error ::Required tool '$Name' not found in PATH after Chocolatey installation."
              exit 1
            }
          }
          # Only contact the Chocolatey servers for packages that are not
          # already present (restored from the cache above or pre-installed on
          # the runner -- which ships Strawberry Perl).  This lets the step
          # succeed from cache when the Chocolatey infrastructure is unavailable.
          #
          # `perl` is only used to run regression's test.pl, so any Perl
          # interpreter already on PATH is sufficient; we therefore install
          # strawberryperl only when no perl at all is found (strawberryperl,
          # unlike winflexbison3/wget, is intentionally not cached).
          $toInstall = @()
          if (-not (Get-Command win_flex -ErrorAction SilentlyContinue)) { $toInstall += 'winflexbison3' }
          if (-not (Get-Command perl     -ErrorAction SilentlyContinue)) { $toInstall += 'strawberryperl' }
          if (-not (Get-Command wget.exe -ErrorAction SilentlyContinue)) { $toInstall += 'wget' }
          if ($toInstall.Count -gt 0)
          {
            choco install -y $toInstall
            if($LastExitCode -ne 0)
            {
              Write-Output "::error ::Dependency installation via Chocolatey failed."
              exit $LastExitCode
            }
          }
          else
          {
            Write-Output "All Chocolatey dependencies already present; skipping install."
          }
          Require-Tool win_flex
          Require-Tool win_bison
          Require-Tool perl
          Require-Tool wget.exe
          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
          echo "c:\Strawberry\" >> $env:GITHUB_PATH
      - name: Install Z3
        uses: ./.github/actions/install-z3
        with:
          version: ${{ env.z3-version }}
      - name: Install cvc5
        uses: ./.github/actions/install-cvc5
        with:
          version: ${{ env.cvc5-version }}
      - name: Confirm z3 solver is available and log the version installed
        run: z3 --version
      - name: Confirm cvc5 solver is available and log the version installed
        run: cvc5 --version
      - name: Initialise Developer Command Line
        uses: ilammy/msvc-dev-cmd@v1
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR
          restore-keys: |
            ${{ runner.os }}-msbuild-make-${{ github.ref }}
            ${{ runner.os }}-msbuild-make
      - name: ccache environment
        run: |
          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
      - name: Zero ccache stats and limit in size (2 GB)
        run: |
          clcache -z
          clcache -M 2147483648
      - name: Download minisat with make
        run: make -C src minisat2-download
      - name: Build CBMC with make
        run: |
          make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
          echo "$pwd\src\solvers;" >> $env:GITHUB_PATH
      - name: Build unit tests with make
        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
      - name: Build jbmc with make
        run: |
          make CXX=clcache -j${{env.windows-vcpus}} -C jbmc/src setup-submodules
          make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/src
      - name: Build JBMC unit tests
        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/unit all
      - name: Print ccache stats
        run: clcache -s
      - name: Run CBMC and JBMC unit tests
        run: |
          make CXX=clcache BUILD_ENV=MSVC -C unit      test
          make CXX=clcache BUILD_ENV=MSVC -C unit test TAGS="[z3]"
          make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
      - name: Run CBMC regression tests
        run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C regression test-parallel-jobs

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 7 to 32 minutes
  windows-msi-package:
    runs-on: windows-2025
    env:
      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Setup Visual Studio environment
        uses: microsoft/setup-msbuild@v3
      - name: Get current month for cache key
        id: cache-key
        run: echo "month=$(Get-Date -Format 'yyyy-MM')" >> $env:GITHUB_OUTPUT
      - name: Cache Chocolatey packages
        uses: actions/cache@v6
        with:
          path: |
            C:\ProgramData\chocolatey\lib\winflexbison3
            C:\ProgramData\chocolatey\bin
          key: ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}-winflexbison3
          restore-keys: |
            ${{ runner.os }}-choco-${{ steps.cache-key.outputs.month }}
      - name: Fetch dependencies
        run: |
          function Require-Tool($Name) {
            if (-not (Get-Command $Name -ErrorAction SilentlyContinue)) {
              Write-Output "::error ::Required tool '$Name' not found in PATH after Chocolatey installation."
              exit 1
            }
          }
          if (-not (Get-Command win_flex -ErrorAction SilentlyContinue))
          {
            # Only contact the Chocolatey servers when the package is not
            # already present (restored from the cache above or pre-installed on
            # the runner).  This lets the step succeed from cache when the
            # Chocolatey infrastructure is unavailable.
            choco install -y winflexbison3
            if($LastExitCode -ne 0)
            {
              Write-Output "::error ::Dependency installation via Chocolatey failed."
              exit $LastExitCode
            }
          }
          else
          {
            Write-Output "winflexbison3 restored from cache; skipping Chocolatey install."
          }
          Require-Tool win_flex
          Require-Tool win_bison
          nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
          echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
      - name: Restore ccache
        id: restore-ccache
        uses: actions/cache/restore@v6
        with:
          path: .ccache
          key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PKG
          restore-keys: |
            ${{ runner.os }}-msbuild-${{ github.ref }}
            ${{ runner.os }}-msbuild
      - name: ccache environment
        run: |
          echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
          echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
      - name: Configure with cmake
        run: cmake -S . -B build
      - name: Build Release
        run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
      - name: Print ccache stats
        run: clcache -s
      - name: Create packages
        id: create_packages
        # We need to get the path to cpack because fascinatingly,
        # chocolatey also includes a command called "cpack" which takes precedence
        run: |
          Set-Location build
          $cpack = "$(Split-Path -Parent (Get-Command cmake).Source)\cpack.exe"
          & $cpack . -C Release
          $msi_name = (Get-ChildItem -name *.msi).Name
          echo "msi_installer=build/$msi_name" >> $env:GITHUB_OUTPUT
          echo "msi_name=$msi_name" >> $env:GITHUB_OUTPUT

      - name: Save ccache
        if: always()
        uses: actions/cache/save@v6
        with:
          path: .ccache
          key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
  # This job takes approximately 2 to 3 minutes
  check-string-table:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - name: Check for unused irep ids
        run: ./scripts/string_table_check.sh

  # This job takes approximately 23 to 29 minutes
  check-docker-image:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Download test dependencies
        run: |
          sudo apt update
          sudo apt install openjdk-11-jdk-headless
      - name: Set up Docker Buildx
        id: setup-buildx
        uses: docker/setup-buildx-action@v4
      - name: Cache Docker build mounts (apt downloads + ccache)
        uses: actions/cache@v6
        id: docker-cache-mount
        with:
          path: docker-cache-mount
          key: docker-cache-mount-${{ github.sha }}
          restore-keys: |
            docker-cache-mount-
      - name: Inject build mounts into BuildKit
        # Docker layer caching cannot speed up the build on a source-changing
        # PR, because `COPY . /tmp/cbmc` invalidates the build layer.  Instead
        # we persist the Dockerfile's apt and ccache `--mount=type=cache`
        # contents across runs: this step restores them into the buildx builder
        # before the build and extracts them again afterwards (saved by the
        # actions/cache step above).  ccache then reuses objects across source
        # changes.  Note: on pull requests from forks the actions/cache write is
        # restricted, so the cache is read-only there and this gracefully
        # degrades to an uncached build.
        uses: reproducible-containers/buildkit-cache-dance@v3
        with:
          builder: ${{ steps.setup-buildx.outputs.name }}
          cache-dir: docker-cache-mount
          dockerfile: Dockerfile
          skip-extraction: ${{ steps.docker-cache-mount.outputs.cache-hit }}
      - name: Build docker image
        run: docker buildx build --load -t cbmc .
      - name: Smoke test goto-cc
        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-cc -o /mnt/smoke/test.goto /mnt/smoke/test.c
      - name: Smoke test cbmc
        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc cbmc /mnt/smoke/test.goto
      - name: Smoke test jbmc
        run: |
          javac .github/workflows/smoke_test_assets/Test.java
          docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc jbmc --classpath /mnt/smoke Test
      - name: Smoke test goto-analyzer
        run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions

  # This job takes approximately 22 to 41 minutes
  include-what-you-use:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
        with:
          submodules: recursive
      - name: Fetch dependencies
        env:
          # This is needed in addition to -yq to prevent apt-get from asking for
          # user input
          DEBIAN_FRONTEND: noninteractive
        run: |
          sudo apt-get update
          sudo apt-get install --no-install-recommends -yq cmake ninja-build clang-19 clang++-19 gdb maven flex bison iwyu
      - name: Configure using CMake
        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++
      - name: Run include-what-you-use
        run: |
          iwyu_tool -p build/compile_commands.json -j${{env.linux-vcpus}} | tee includes.txt
          if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
            echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
            exit 1
          fi