Merge pull request #7734 from tautschnig/cadical-1.5.3

Update CaDiCaL from 1.4.1 to 1.5.3

Author: kroening

scripts/cadical-1.4.1-patch scripts/cadical-1.5.3-patchscripts/cadical-1.4.1-patch renamed to scripts/cadical-1.5.3-patch

@@ -32,3 +32,14 @@ index 9e8a16b..3d5721a 100644
      cubes.cubes.push_back(std::vector<int>());
      return cubes;
    }
+diff -urN cadical-rel-1.5.3/src/solver.cpp cadical-rel-1.5.3.patched/src/solver.cpp
+--- cadical-rel-1.5.3/src/solver.cpp	2023-02-13 09:11:26.000000000 +0000
++++ cadical-rel-1.5.3.patched/src/solver.cpp	2023-05-29 09:42:55.871965742 +0000
+@@ -258,7 +258,6 @@
+
+ #define TRACE(...) \
+ do { \
+-  if ((this == 0)) break; \
+   if ((internal == 0)) break; \
+   LOG_API_CALL_BEGIN (__VA_ARGS__); \
+   if (!trace_api_file) break; \

src/Makefile

@@ -174,17 +174,17 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@$(RM) $(glucose_rev).tar.gz
 
-cadical_release = rel-1.4.1
+cadical_release = rel-1.5.3
 cadical-download:
 	@echo "Downloading CaDiCaL $(cadical_release)"
 	@$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz
 	@$(TAR) xfz $(cadical_release).tar.gz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@(cd ../cadical; patch -p1 < ../scripts/cadical-1.4.1-patch)
+	@(cd ../cadical; patch -p1 < ../scripts/cadical-1.5.3-patch)
 	@(cd ../cadical && ./configure)
-  # Need to rename VERSION so that it isn't picked up by `#include<version>` on
-  # macOS which is case insensitive
+	# Need to rename VERSION so that it isn't picked up by `#include<version>` on
+	# macOS which is case insensitive
 	@(cd ../cadical && mv VERSION VERSION.txt)
 	@$(RM) $(cadical_release).tar.gz
 

src/solvers/CMakeLists.txt

@@ -124,11 +124,11 @@ foreach(SOLVER ${sat_impl})
         message(STATUS "Building solvers with cadical")
 
         download_project(PROJ cadical
-            URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.4.1-patch
+            URL https://github.com/arminbiere/cadical/archive/rel-1.5.3.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.5.3-patch
             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
             COMMAND ./configure
-            URL_MD5 b44874501a175106424f4bd5de29aa59
+            URL_MD5 265b1a715000ed3c5b6de36ddd1278a0
         )
 
         add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
@@ -147,10 +147,10 @@ foreach(SOLVER ${sat_impl})
         message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
 
         download_project(PROJ cadical
-            URL https://github.com/arminbiere/cadical/archive/rel-1.4.1.tar.gz
-            PATCH_COMMAND true
-            COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s CXXFLAGS=-std=c++14
-            URL_MD5 b44874501a175106424f4bd5de29aa59
+            URL https://github.com/arminbiere/cadical/archive/rel-1.5.3.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.5.3-patch
+            COMMAND ./configure
+            URL_MD5 265b1a715000ed3c5b6de36ddd1278a0
         )
 
         message(STATUS "Building CaDiCaL")