From 661edc4948b72a615b04bf0d4cfa41018f29f6be Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 26 Jul 2017 17:05:12 -0700 Subject: -Og for non-opt build, parallel pcvc4 check (#206) -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 | 2 +- configure.ac | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index bb5ce3d17..6ef64f0e2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -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() { diff --git a/configure.ac b/configure.ac index b32bbc9b1..30098305f 100644 --- a/configure.ac +++ b/configure.ac @@ -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]) -- cgit v1.2.3