Skip to content

Commit bc8a56a

Browse files
committed
Compile CaDiCaL with -DNDEBUG
Using CaDiCaL with CBMC showed substantially decreased performance between versions 1.8.0 and 1.9.0. This has become apparent with Kani, but also our THOROUGH tests changed from 7 minutes to just under 2 hours in CI. The culprit is arminbiere/cadical@69e7cfb, which introduces expensive checks in `NDEBUG` blocks.
1 parent bf58af8 commit bc8a56a

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

scripts/cadical_CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ add_library(cadical ${sources})
99

1010
# Pass -DNBUILD to disable including the version information, which is not
1111
# needed since cbmc doesn't run the cadical binary
12-
target_compile_options(cadical PUBLIC -DNBUILD -DNFLEXIBLE)
12+
target_compile_options(cadical PUBLIC -DNBUILD -DNFLEXIBLE -DNDEBUG)
1313

1414
set_target_properties(
1515
cadical

src/solvers/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
281281
$(LINKLIB)
282282

283283
../../cadical/build/libcadical$(LIBEXT):
284-
$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE"
284+
$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE -DNDEBUG"
285285

286286
-include smt2/smt2_solver$(DEPEXT)
287287

0 commit comments

Comments
 (0)