Merge pull request #855 from diffblue/ebmc-release-cadical

ebmc release flow: add Cadical
diffblue · Nov 30, 2024 · 1a93509 · 1a93509
2 parents dcdd4a1 + 15fb88b
commit 1a93509
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 19 deletions.
diff --git 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
@@ -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: