-Og for non-opt build, parallel pcvc4 check (#206)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 27 Jul 2017 00:05:12 +0000 (17:05 -0700)
committerGitHub <noreply@github.com>
Thu, 27 Jul 2017 00:05:12 +0000 (17:05 -0700)
-Og enables optimizations that do not interfere with debugging. This is the new
default for debug builds if the compiler supports the flag. This commit also
enables parallel checking for the portfolio build on Travis.

.travis.yml
configure.ac

index bb5ce3d17d956a252a40208134a038d570afce19..6ef64f0e242209e8c9bd643da3a328e2e229f0d2 100644 (file)
@@ -68,7 +68,7 @@ script:
      make V=1 -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/TEST FAILED";
    }
    makeCheckPortfolio() {
-     make check V=1 BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
+     make V=1 -j2 check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= ||
        error "PORTFOLIO TEST FAILED";
    }
    makeExamples() {
index b32bbc9b1b07eaf5da2f79a7c889502e621121b0..30098305ff4cb1b672692050a3a4617a06608337 100644 (file)
@@ -600,8 +600,12 @@ if test "$enable_optimized" = yes; then
   CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
   CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
 else
-  CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
-  CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
+  # Use -Og if available (optimizations that do not interfere with debugging),
+  # -O0 otherwise
+  debug_optimization_level="-O0"
+  CVC4_CXX_OPTION([-Og], [debug_optimization_level])
+  CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${debug_optimization_level}"
+  CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }${debug_optimization_level}"
 fi
 
 AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])