From 15fb88b79f2b67ef37ea41a42959995e721e3e9a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 30 Nov 2024 11:38:52 +0000
Subject: [PATCH] ebmc release flow: add Cadical

This adds Cadical to the release builds for Debian/Ubuntu and Redhat.
---
 .github/workflows/ebmc-release.yaml        | 12 +++++------
 .github/workflows/pull-request-checks.yaml | 24 ++++++++++------------
 2 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/ebmc-release.yaml b/.github/workflows/ebmc-release.yaml
index 6514d45f..fb269c03 100644
--- a/.github/workflows/ebmc-release.yaml
+++ b/.github/workflows/ebmc-release.yaml
@@ -67,12 +67,12 @@ jobs:
           restore-keys: ${{ runner.os }}-22.04-make-gcc
       - name: ccache path
         run: ccache -p | grep cache_dir
-      - name: Get minisat
-        run: make -C lib/cbmc/src minisat2-download
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
         run: |
           # -static-libstdc++ is insufficient, owing to varying GLIBC versions
-          make -C src -j4 CXX="ccache g++" LINKFLAGS="-static"
+          make -C src -j4 CXX="ccache g++" LINKFLAGS="-static" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run the ebmc tests with SAT
         run: make -C regression/ebmc test
       - name: Run the verilog tests
@@ -148,12 +148,12 @@ jobs:
         run: ccache -z --max-size=500M
       - name: ccache path
         run: ccache -p | grep cache_dir
-      - name: Get minisat
-        run: make -C lib/cbmc/src minisat2-download
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
         run: |
           # -static-libstdc++ suffices -- tested on CentOS, Fedora, Amazon Linux
-          make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" LINKFLAGS="-static-libstdc++" -C src -j4
+          make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" LINKFLAGS="-static-libstdc++" -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Print ccache stats
         run: ccache -s
       - name: Run the ebmc tests with SAT
diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index 0351e40b..1259340c 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -39,8 +39,7 @@ jobs:
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Get cadical and minisat
-        run: |
-          make -C lib/cbmc/src cadical-download minisat2-download
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
         run: make -C src -j4 CXX="ccache g++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run unit tests
@@ -98,11 +97,10 @@ jobs:
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
-      - name: Get minisat
-        run: |
-          make -C lib/cbmc/src minisat2-download
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
-        run: make CXX="ccache clang++" -C src -j4
+        run: make CXX="ccache clang++" -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run unit tests
         run: make -C unit -j4 CXX="ccache clang++"
       - name: Run the ebmc tests with SAT
@@ -203,10 +201,10 @@ jobs:
         run: ccache -z --max-size=500M
       - name: ccache path
         run: ccache -p | grep cache_dir
-      - name: Get minisat
-        run: make -C lib/cbmc/src minisat2-download
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
-        run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4
+        run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run unit tests
         run: make -C unit -j4 CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs"
       - name: Run the ebmc tests with SAT
@@ -248,10 +246,10 @@ jobs:
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
-      - name: Get minisat
-        run: make -C lib/cbmc/src minisat2-download
+      - name: Get cadical and minisat
+        run: make -C lib/cbmc/src cadical-download minisat2-download
       - name: Build with make
-        run: make YACC="/opt/homebrew/opt/bison/bin/bison" CXX="ccache clang++" -C src -j3
+        run: make YACC="/opt/homebrew/opt/bison/bin/bison" CXX="ccache clang++" -C src -j3 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
       - name: Run unit tests
         run: make -C unit -j3 CXX="ccache g++"
       - name: Run the ebmc tests with SAT
@@ -397,7 +395,7 @@ jobs:
         run: |
           clcache -z
           clcache -M 2147483648
-      - name: Download minisat with make
+      - name: Download minisat
         run: make -C lib/cbmc/src minisat2-download
       - name: Build EBMC with make
         env: