diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh index 30a8ce5a4..8cd646ce6 100644 --- a/contrib/ci/scripts/sanitizer_env.sh +++ b/contrib/ci/scripts/sanitizer_env.sh @@ -8,8 +8,21 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then # Use suppression files export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt" + # NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0` + # NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations. + # If the reported stacktraces appear incomplete try increasing the value. export ASAN_OPTIONS="malloc_context_size=100,print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt" : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"} + + # Run command without checking for leaks + function run_no_lsan() { + ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}" + } +else + # In non-ASan build just run directly + function run_no_lsan() { + "${@}" + } fi if [ "X${UBSAN_BUILD}" = "X1" ]; then diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index c188dbcf4..477f7f747 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -42,9 +42,13 @@ run_quiet examples/tptp_build_dir/z3_tptp5 -help # Build an run c_maxsat_example cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" -run_quiet \ - examples/c_maxsat_example_build_dir/c_maxsat_example \ - ${Z3_SRC_DIR}/examples/maxsat/ex.smt +# FIXME: It is known that the maxsat example leaks memory and the +# the Z3 developers have stated this is "wontfix". +# See https://github.com/Z3Prover/z3/issues/1299 +run_no_lsan \ + run_quiet \ + examples/c_maxsat_example_build_dir/c_maxsat_example \ + ${Z3_SRC_DIR}/examples/maxsat/ex.smt if [ "X${UBSAN_BUILD}" = "X1" ]; then # FIXME: We really need libz3 to link against a shared UBSan runtime.