From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 10 Mar 2021 19:40:15 +0000 (-0800)
Subject: cmake: Fix optimization level for debug builds. (#6097)
X-Git-Tag: cvc5-1.0.0~2115
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27fb04bc96999e101b45458c549345e864e085e9;p=cvc5.git

cmake: Fix optimization level for debug builds. (#6097)

Further cleans up some unused variables and moves the configuration of
best to configure.sh.
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 3f5100cd4..dc244917d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -271,16 +271,6 @@ else()
 endif()
 
 #-----------------------------------------------------------------------------#
-# Set options for best configuration
-
-if(ENABLE_BEST)
-  cvc4_set_option(USE_ABC ON)
-  cvc4_set_option(USE_CADICAL ON)
-  cvc4_set_option(USE_CLN ON)
-  cvc4_set_option(USE_CRYPTOMINISAT ON)
-  cvc4_set_option(USE_GLPK ON)
-  cvc4_set_option(USE_EDITLINE ON)
-endif()
 
 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 # that expect AssertionException to be thrown will fail.
@@ -671,7 +661,6 @@ endif()
 message("")
 print_config("GPL                       :" ENABLE_GPL)
 print_config("Best configuration        :" ENABLE_BEST)
-print_config("Optimization level        :" OPTIMIZATION_LEVEL)
 message("")
 print_config("Assertions                :" ENABLE_ASSERTIONS)
 print_config("Debug symbols             :" ENABLE_DEBUG_SYMBOLS)
@@ -706,7 +695,7 @@ print_config("Kissat                    :" USE_KISSAT)
 print_config("LFSC                      :" USE_LFSC)
 print_config("LibPoly                   :" USE_POLY)
 message("")
-print_config("BUILD_LIB_ONLY            :" BUILD_LIB_ONLY)
+print_config("Build libcvc4 only        :" BUILD_LIB_ONLY)
 
 if(CVC4_USE_CLN_IMP)
   message("MP library                : cln")
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index 723ed9236..b01c2bb23 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -9,10 +9,8 @@
 ## directory for licensing information.
 ##
 add_definitions(-DCVC4_DEBUG)
-set(CVC4_DEBUG 1)
 add_check_c_cxx_flag("-fno-inline")
-set(OPTIMIZATION_LEVEL 0)
-add_c_cxx_flag("-Og")
+set(OPTIMIZATION_LEVEL "g")
 # enable_debug_symbols=yes
 cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
 # enable_statistics=yes
diff --git a/configure.sh b/configure.sh
index f39cbfb00..ed84a7270 100755
--- a/configure.sh
+++ b/configure.sh
@@ -33,7 +33,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --static-binary          statically link against system libraries
                            (must be disabled for static macOS builds) [default=yes]
   --proofs                 support for proof generation
-  --optimized              optimize the build
   --debug-symbols          include debug symbols
   --valgrind               Valgrind instrumentation
   --debug-context-mm       use the debug context memory manager
@@ -117,7 +116,6 @@ buildtype=default
 abc=default
 asan=default
 assertions=default
-best=default
 cadical=default
 cln=default
 comp_inc=default
@@ -134,7 +132,6 @@ lfsc=default
 poly=default
 muzzle=default
 ninja=default
-optimized=default
 profiling=default
 proofs=default
 python2=default
@@ -193,8 +190,15 @@ do
     --assertions) assertions=ON;;
     --no-assertions) assertions=OFF;;
 
-    --best) best=ON;;
-    --no-best) best=OFF;;
+    # Best configuration
+    --best)
+      abc=ON
+      cadical=ON
+      cln=ON
+      cryptominisat=ON
+      glpk=ON
+      editline=ON
+      ;;
 
     --prefix) die "missing argument to $1 (try -h)" ;;
     --prefix=*)
@@ -261,9 +265,6 @@ do
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
-    --optimized) optimized=ON;;
-    --no-optimized) optimized=OFF;;
-
     --proofs) proofs=ON;;
     --no-proofs) proofs=OFF;;
 
@@ -389,8 +390,6 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
 [ $assertions != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
-[ $best != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_BEST=$best"
 [ $comp_inc != default ] \
   && cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
 [ $coverage != default ] \
@@ -410,8 +409,6 @@ cmake_opts=""
 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $optimized != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized"
 [ $proofs != default ] \
   && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs"
 [ $shared != default ] \
diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
index 61150799c..0d481ea4f 100644
--- a/test/unit/expr/node_black.cpp
+++ b/test/unit/expr/node_black.cpp
@@ -107,9 +107,12 @@ TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
 TEST_F(TestNodeBlackNode, dtor)
 {
   /* No access to internals? Only test that this is crash free. */
-  Node* n;
+  Node* n = nullptr;
   ASSERT_NO_FATAL_FAILURE(n = new Node());
-  delete n;
+  if (n)
+  {
+    delete n;
+  }
 }
 
 /* operator== */