summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-07-26 17:05:12 -0700
committerGitHub <noreply@github.com>2017-07-26 17:05:12 -0700
commit661edc4948b72a615b04bf0d4cfa41018f29f6be (patch)
tree734395d978d3fa97eb4ec8864eeb3718237ff763
parenta354816a5d6b9026383e9982f3cf25996eddd3ba (diff)
-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.
-rw-r--r--.travis.yml2
-rw-r--r--configure.ac8
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])
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback