From 64ee9f168df650537c6264c1c4e6c16dd315966d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 12:26:35 +0100
Subject: [PATCH 01/32] [TravisCI] Add ASan/LSan/UBSan suppression files and
 use them in CI.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile    |  9 ++++++++-
 contrib/ci/scripts/sanitizer_env.sh           | 19 +++++++++++++++++++
 contrib/ci/scripts/test_z3_examples_cmake.sh  |  3 +++
 contrib/ci/scripts/test_z3_system_tests.sh    |  3 +++
 .../ci/scripts/test_z3_unit_tests_cmake.sh    |  3 +++
 contrib/suppressions/README.md                |  7 +++++++
 contrib/suppressions/maintainers.txt          |  3 +++
 contrib/suppressions/sanitizers/README.md     |  4 ++++
 contrib/suppressions/sanitizers/asan.txt      |  1 +
 contrib/suppressions/sanitizers/lsan.txt      |  1 +
 contrib/suppressions/sanitizers/ubsan.txt     |  1 +
 11 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 contrib/ci/scripts/sanitizer_env.sh
 create mode 100644 contrib/suppressions/README.md
 create mode 100644 contrib/suppressions/maintainers.txt
 create mode 100644 contrib/suppressions/sanitizers/README.md
 create mode 100644 contrib/suppressions/sanitizers/asan.txt
 create mode 100644 contrib/suppressions/sanitizers/lsan.txt
 create mode 100644 contrib/suppressions/sanitizers/ubsan.txt

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 07504e6b9..65cf08087 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -62,7 +62,8 @@ ENV \
 
 # Build Z3
 RUN mkdir -p "${Z3_SRC_DIR}" && \
-  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts"
+  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \
+  mkdir -p "${Z3_SRC_DIR}/contrib/ci/suppressions/sanitizers"
 # Deliberately leave out `contrib`
 ADD /cmake ${Z3_SRC_DIR}/cmake/
 ADD /doc ${Z3_SRC_DIR}/doc/
@@ -89,7 +90,13 @@ RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
 # Test examples
 ADD \
   /contrib/ci/scripts/test_z3_examples_cmake.sh \
+  /contrib/ci/scripts/sanitizer_env.sh \
   ${Z3_SRC_DIR}/contrib/ci/scripts/
+ADD \
+  /contrib/suppressions/sanitizers/asan.txt \
+  /contrib/suppressions/sanitizers/lsan.txt \
+  /contrib/suppressions/sanitizers/ubsan.txt \
+  ${Z3_SRC_DIR}/contrib/suppressions/sanitizers/
 RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
 
 # Run unit tests
diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
new file mode 100644
index 000000000..e9af255d3
--- /dev/null
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -0,0 +1,19 @@
+# This script is intended to be included by other
+# scripts and should not be executed directly
+
+: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
+: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
+
+if [ "X${ASAN_BUILD}" = "X1" ]; then
+  # Use suppression files
+  export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
+  export ASAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+fi
+
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  # `halt_on_error=1,abort_on_error=1` means that on the first UBSan error
+  # the program will terminate by calling `abort(). Without this UBSan will
+  # allow execution to continue. We also use a suppression file.
+  export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
+fi
diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index 2eda3de7b..1b8f988a2 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -21,6 +21,9 @@ source ${SCRIPT_DIR}/set_compiler_flags.sh
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 cd "${Z3_BUILD_DIR}"
 
 # Build and run C example
diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index dfb1084a4..d61a0ef02 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -16,6 +16,9 @@ if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
   exit 0
 fi
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 Z3_EXE="${Z3_BUILD_DIR}/z3"
 Z3_LIB_DIR="${Z3_BUILD_DIR}"
 
diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
index e1c927f58..60c29556b 100755
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
@@ -13,6 +13,9 @@ set -o pipefail
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
+# Sanitizer environment variables
+source ${SCRIPT_DIR}/sanitizer_env.sh
+
 cd "${Z3_BUILD_DIR}"
 
 function build_unit_tests() {
diff --git a/contrib/suppressions/README.md b/contrib/suppressions/README.md
new file mode 100644
index 000000000..90df39084
--- /dev/null
+++ b/contrib/suppressions/README.md
@@ -0,0 +1,7 @@
+# Suppression files
+
+This directory contains suppression files used by various
+program analysis tools.
+
+Suppression files tell a program analysis tool to suppress
+various warnings/errors.
diff --git a/contrib/suppressions/maintainers.txt b/contrib/suppressions/maintainers.txt
new file mode 100644
index 000000000..caa6798c6
--- /dev/null
+++ b/contrib/suppressions/maintainers.txt
@@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)
diff --git a/contrib/suppressions/sanitizers/README.md b/contrib/suppressions/sanitizers/README.md
new file mode 100644
index 000000000..f76f920b2
--- /dev/null
+++ b/contrib/suppressions/sanitizers/README.md
@@ -0,0 +1,4 @@
+# Sanitizer supression files
+
+This directory contains files used to suppress
+ASan/LSan/UBSan warnings/errors.
diff --git a/contrib/suppressions/sanitizers/asan.txt b/contrib/suppressions/sanitizers/asan.txt
new file mode 100644
index 000000000..f058adfe2
--- /dev/null
+++ b/contrib/suppressions/sanitizers/asan.txt
@@ -0,0 +1 @@
+# AddressSanitizer suppression file
diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
new file mode 100644
index 000000000..a4ce0881a
--- /dev/null
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -0,0 +1 @@
+# LeakSanitizer suppression file
diff --git a/contrib/suppressions/sanitizers/ubsan.txt b/contrib/suppressions/sanitizers/ubsan.txt
new file mode 100644
index 000000000..8feef305f
--- /dev/null
+++ b/contrib/suppressions/sanitizers/ubsan.txt
@@ -0,0 +1 @@
+# UndefinedBehavior sanitizer suppression file

From a9fcfc531bda243b7b7cf30f2d6591d6430ac8b6 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 15:25:41 +0100
Subject: [PATCH 02/32] [TravisCI][CMake] Add  `Z3_C_EXAMPLES_FORCE_CXX_LINKER`
 CMake option and propagate its value into the C API examples.

This flag forces the C API examples to use the C++ compiler as the
linker rather than the C compiler. This a workaround to avoid linking
errors when building with UBSan.
---
 README-CMake.md                      |  1 +
 contrib/ci/scripts/build_z3_cmake.sh | 11 +++++++++++
 examples/CMakeLists.txt              | 21 +++++++++++++++++++--
 examples/c/CMakeLists.txt            | 11 +++++++++++
 examples/maxsat/CMakeLists.txt       | 10 ++++++++++
 5 files changed, 52 insertions(+), 2 deletions(-)

diff --git a/README-CMake.md b/README-CMake.md
index 605c14818..0d323e08f 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -270,6 +270,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
 * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
     If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
+* ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh
index 76fd0fb84..c1014d5d5 100755
--- a/contrib/ci/scripts/build_z3_cmake.sh
+++ b/contrib/ci/scripts/build_z3_cmake.sh
@@ -22,6 +22,7 @@ set -o pipefail
 : ${USE_LTO?"USE_LTO must be specified"}
 : ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
 : ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
 
 ADDITIONAL_Z3_OPTS=()
 
@@ -105,6 +106,16 @@ fi
 # Set compiler flags
 source ${SCRIPT_DIR}/set_compiler_flags.sh
 
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  # HACK: When building with UBSan the C++ linker
+  # must be used to avoid the following linker errors.
+  # undefined reference to `__ubsan_vptr_type_cache'
+  # undefined reference to `__ubsan_handle_dynamic_type_cache_miss'
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DZ3_C_EXAMPLES_FORCE_CXX_LINKER=ON' \
+  )
+fi
+
 # Sanity check
 if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
   echo "Z3_SRC_DIR is invalid"
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index ba7f6ee59..338d2e4bb 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -7,6 +7,19 @@ else()
   set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "")
 endif()
 
+option(Z3_C_EXAMPLES_FORCE_CXX_LINKER
+  "Force C++ linker when building C example projects" OFF)
+
+if (Z3_C_EXAMPLES_FORCE_CXX_LINKER)
+  # HACK: This is a workaround for UBSan.
+  message(STATUS "Forcing C++ linker to be used when building example C projects")
+  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG
+    "-DFORCE_CXX_LINKER=ON"
+  )
+else()
+  set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "")
+endif()
+
 ################################################################################
 # Build example project using libz3's C API as an external project
 ################################################################################
@@ -14,7 +27,9 @@ ExternalProject_Add(c_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
@@ -30,7 +45,9 @@ ExternalProject_Add(c_maxsat_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/maxsat"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt
index dd8fa6328..bac08e460 100644
--- a/examples/c/CMakeLists.txt
+++ b/examples/c/CMakeLists.txt
@@ -22,6 +22,17 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
 message(STATUS "Z3_DIR: ${Z3_DIR}")
 
 add_executable(c_example test_capi.c)
+
+option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
+if (FORCE_CXX_LINKER)
+  # This is a hack for avoiding UBSan linking errors
+  message(STATUS "Forcing use of C++ linker")
+  set_target_properties(c_example
+    PROPERTIES
+    LINKER_LANGUAGE CXX
+  )
+endif()
+
 target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
 
diff --git a/examples/maxsat/CMakeLists.txt b/examples/maxsat/CMakeLists.txt
index b48e167ea..019243ecf 100644
--- a/examples/maxsat/CMakeLists.txt
+++ b/examples/maxsat/CMakeLists.txt
@@ -25,6 +25,16 @@ add_executable(c_maxsat_example maxsat.c)
 target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES})
 
+option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
+if (FORCE_CXX_LINKER)
+  # This is a hack for avoiding UBSan linking errors
+  message(STATUS "Forcing use of C++ linker")
+  set_target_properties(c_maxsat_example
+    PROPERTIES
+    LINKER_LANGUAGE CXX
+  )
+endif()
+
 if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable

From f15766baee334b2d045e72b392712ef133c28c3a Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 15:56:43 +0100
Subject: [PATCH 03/32] [TravisCI] Don't run the non-native example when
 building with UBSan.

This a workaround. Right now `libz3` gets linked against a static
UBSan runtime which means none of the non-native language bindings
(e.g. python) can load `libz3` due to undefined symbols. We need
to link `libz3` against a shared UBSan runtime to fix this.
---
 contrib/ci/scripts/test_z3_examples_cmake.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index 1b8f988a2..c188dbcf4 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -14,6 +14,7 @@ set -o pipefail
 : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
 : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
 : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
 
 # Set compiler flags
 source ${SCRIPT_DIR}/set_compiler_flags.sh
@@ -45,6 +46,14 @@ 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.
+  # Right now we link against the static runtime which breaks all the
+  # non-native language bindings.
+  echo "FIXME: Can't run other examples when building with UBSan"
+  exit 0
+fi
+
 
 if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
   # Run python examples

From fb3d4cfed9970e44712a3ee580e6152f7f17f966 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 16:13:57 +0100
Subject: [PATCH 04/32] [TravisCI] Add a UBSan configuration

---
 .travis.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 81ddefb8b..9584d3869 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -17,6 +17,9 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
+    # 64-bit UBSan build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo UBSAN_BUILD=1
+
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
     # 64-bit Clang 3.9 RelWithDebInfo

From f756bf6c86e6ea91aacbcc05b9cb0fa75bdcdef1 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 16:27:31 +0100
Subject: [PATCH 05/32] [TravisCI] Fix undefined SCRIPT_DIR variable

---
 contrib/ci/scripts/test_z3_system_tests.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index d61a0ef02..1b6433806 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -17,6 +17,7 @@ if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
 fi
 
 # Sanitizer environment variables
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
 source ${SCRIPT_DIR}/sanitizer_env.sh
 
 Z3_EXE="${Z3_BUILD_DIR}/z3"

From 9455391f1f60d0f4ff958dd95fb0f74cbe399ad8 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 16:46:26 +0100
Subject: [PATCH 06/32] [TravisCI] Don't run the python binding system tests
 when building with UBSan.

This is a workaround. We can't fix this unless we build libz3 with
a shared UBSan runtime.
---
 contrib/ci/scripts/test_z3_system_tests.sh | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index 1b6433806..71ecf2a1e 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -10,6 +10,7 @@ set -o pipefail
 : ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
 : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
 : ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
 
 if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
   echo "Skipping system tests"
@@ -52,7 +53,13 @@ fi
 
 if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
   # Run python binding tests
-  ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+  if [ "X${UBSAN_BUILD}" = "X1" ]; then
+    # FIXME: We need to build libz3 with a shared UBSan runtime for the bindings
+    # to work.
+    echo "FIXME: Skipping python binding tests when building with UBSan"
+  else
+    ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+  fi
 fi
 
 # FIXME: Run `scripts/test_cs.py` once it has been modified to support mono

From 71dcec311349e37ef5192c331174ab4f7bcb853d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 16:48:12 +0100
Subject: [PATCH 07/32] [UBSan] Update UBSan suppression file to suppress all
 undefined behaviour I have observed running in CI.

---
 contrib/suppressions/sanitizers/ubsan.txt | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/contrib/suppressions/sanitizers/ubsan.txt b/contrib/suppressions/sanitizers/ubsan.txt
index 8feef305f..6ceacd400 100644
--- a/contrib/suppressions/sanitizers/ubsan.txt
+++ b/contrib/suppressions/sanitizers/ubsan.txt
@@ -1 +1,20 @@
 # UndefinedBehavior sanitizer suppression file
+# FIXME: UBSan doesn't usually have false positives so we need to fix all of these!
+
+# Occurs when running C API example (`interpolation_example`)
+# See https://github.com/Z3Prover/z3/issues/1286
+null:iz3mgr.h
+
+# Occurs when running C++ API example
+# See https://github.com/Z3Prover/z3/issues/1287
+function:api_context.cpp
+
+# Occurs when running tptp example
+# See https://github.com/Z3Prover/z3/issues/964
+null:rational.h
+null:mpq.h
+
+# Occurs when running `test-z3 /a`
+# See https://github.com/Z3Prover/z3/issues/1288
+shift-exponent:tbv.cpp
+signed-integer-overflow:mpz.cpp

From 4db5980a234802db1c379f3358230631636edf08 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 19:01:20 +0100
Subject: [PATCH 08/32] [TravisCI] Fix getting proper stack traces for
 ASan/LSan. The `llvm-symbolizer` tool needs to be installed and ASan/LSan
 needs to be told where to find it.

---
 contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile | 3 ++-
 contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile   | 3 ++-
 contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile   | 3 ++-
 contrib/ci/scripts/sanitizer_env.sh                      | 1 +
 4 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
index d8a32edea..87e3c8d67 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
@@ -30,6 +30,7 @@ RUN apt-get update && \
         libgomp1 \
         libomp5 \
         libomp-dev \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -47,4 +48,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
index c28e59e97..c963ce255 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
@@ -16,6 +16,7 @@ RUN apt-get update && \
         libgmp-dev \
         libgomp1 \
         lib32gomp1 \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -32,4 +33,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
index 98a5a3e09..08686e275 100644
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
@@ -18,6 +18,7 @@ RUN apt-get update && \
         libgomp1 \
         libomp5 \
         libomp-dev \
+        llvm-3.9 \
         make \
         mono-devel \
         ninja-build \
@@ -35,4 +36,4 @@ RUN useradd -m user && \
     echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
 USER user
 WORKDIR /home/user
-
+ENV ASAN_SYMBOLIZER_PATH=/usr/lib/llvm-3.9/bin/llvm-symbolizer
diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
index e9af255d3..3b1ff7297 100644
--- a/contrib/ci/scripts/sanitizer_env.sh
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -9,6 +9,7 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then
   # Use suppression files
   export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
   export ASAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+  : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
 fi
 
 if [ "X${UBSAN_BUILD}" = "X1" ]; then

From 157c8064e8f867c134c3979fd574264cf0c990aa Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 19:06:57 +0100
Subject: [PATCH 09/32] [CMake] When building C/C++ API examples use the same
 build type as Z3 if doing a single configuration build.

---
 examples/CMakeLists.txt | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 338d2e4bb..6c50320ed 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -20,6 +20,17 @@ else()
   set(EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG "")
 endif()
 
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  message(WARNING
+    "Cannot set built type of external project when building with a "
+    "multi-configuration generator")
+  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG "")
+else()
+  set(EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG
+    "-DCMAKE_BUILD_TYPE:STRING=${CMAKE_BUILD_TYPE}"
+  )
+endif()
+
 ################################################################################
 # Build example project using libz3's C API as an external project
 ################################################################################
@@ -30,6 +41,7 @@ ExternalProject_Add(c_example
   CMAKE_ARGS
     "-DZ3_DIR=${CMAKE_BINARY_DIR}"
     "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir"
@@ -48,6 +60,7 @@ ExternalProject_Add(c_maxsat_example
   CMAKE_ARGS
     "-DZ3_DIR=${CMAKE_BINARY_DIR}"
     "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir"
@@ -64,7 +77,9 @@ ExternalProject_Add(cpp_example
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir"
@@ -80,7 +95,9 @@ ExternalProject_Add(z3_tptp5
   DEPENDS libz3
   # Configure step
   SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp"
-  CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+  CMAKE_ARGS
+    "-DZ3_DIR=${CMAKE_BINARY_DIR}"
+    "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}"
   # Build step
   ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
   BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir"

From 11f7298c52f2b41eb64775d419f17b4c6333bcf4 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 19:52:25 +0100
Subject: [PATCH 10/32] [TravisCI] Add ASan configuration

---
 .travis.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 9584d3869..bf69573aa 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -17,8 +17,13 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
+    # FIXME: We should probably do unoptimized build to avoid the compiler's
+    # optimizer removing bad behaviour. However we can't run the unit tests
+    # if we do a Debug build because they are too slow.
     # 64-bit UBSan build
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo UBSAN_BUILD=1
+    # 64-bit ASan build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo ASAN_BUILD=1
 
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo

From 38d9e2df8489a16470239369cfc41f313446b755 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 20:02:25 +0100
Subject: [PATCH 11/32] [TravisCI] Make ASan/UBSan configuration a debug build.

---
 .travis.yml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index bf69573aa..534aeacf0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -17,13 +17,11 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
-    # FIXME: We should probably do unoptimized build to avoid the compiler's
-    # optimizer removing bad behaviour. However we can't run the unit tests
-    # if we do a Debug build because they are too slow.
-    # 64-bit UBSan build
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo UBSAN_BUILD=1
-    # 64-bit ASan build
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo ASAN_BUILD=1
+    # FIXME: We should really run the unit tests too under ASan/UBSan but a debug build is too slow.
+    # 64-bit UBSan Debug build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
+    # 64-bit ASan Debug build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP
 
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo

From 5bcdea1ae501d9f7c6ff3759d4a9347ea7075d70 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 20:16:09 +0100
Subject: [PATCH 12/32] [TravisCI] For ASan/LSan use larger context so we get
 larger stack traces if needed.

---
 contrib/ci/scripts/sanitizer_env.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
index 3b1ff7297..30a8ce5a4 100644
--- a/contrib/ci/scripts/sanitizer_env.sh
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -8,7 +8,7 @@
 if [ "X${ASAN_BUILD}" = "X1" ]; then
   # Use suppression files
   export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
-  export ASAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+  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"}
 fi
 

From a991e44a2528bdee40e43c90b7902ec136968d16 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 9 Oct 2017 23:25:53 +0100
Subject: [PATCH 13/32] [TravisCI] Fix typo in created directory for
 suppression files

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 65cf08087..0b6d0ac0d 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -63,7 +63,7 @@ ENV \
 # Build Z3
 RUN mkdir -p "${Z3_SRC_DIR}" && \
   mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" && \
-  mkdir -p "${Z3_SRC_DIR}/contrib/ci/suppressions/sanitizers"
+  mkdir -p "${Z3_SRC_DIR}/contrib/suppressions/sanitizers"
 # Deliberately leave out `contrib`
 ADD /cmake ${Z3_SRC_DIR}/cmake/
 ADD /doc ${Z3_SRC_DIR}/doc/

From bcff86a31606e0410a9295ed8ba35636d4b078a2 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 9 Oct 2017 23:29:08 +0100
Subject: [PATCH 14/32] [LSan] Add suppression for part of #1297.

---
 contrib/suppressions/sanitizers/lsan.txt | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
index a4ce0881a..437358132 100644
--- a/contrib/suppressions/sanitizers/lsan.txt
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -1 +1,5 @@
 # LeakSanitizer suppression file
+
+# FIXME: This looks a bug in Clang/LSan the error reported
+# doesn't make sense. See https://github.com/Z3Prover/z3/issues/1297
+leak:_fini

From f90fe928af7029cb4c2179da5eca6268b1d2efe5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 9 Oct 2017 23:42:10 +0100
Subject: [PATCH 15/32] [LSan] Suppress another leak until I can figure out
 what is going on.

---
 contrib/suppressions/sanitizers/lsan.txt | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
index 437358132..81a3c8b85 100644
--- a/contrib/suppressions/sanitizers/lsan.txt
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -3,3 +3,6 @@
 # FIXME: This looks a bug in Clang/LSan the error reported
 # doesn't make sense. See https://github.com/Z3Prover/z3/issues/1297
 leak:_fini
+# FIXME: I don't understand this leak.
+# See https://github.com/Z3Prover/z3/issues/1297
+leak:error_code_example2

From ff5df20deb0e49a73514906db6491a80932ca5a0 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 11 Oct 2017 08:10:13 +0100
Subject: [PATCH 16/32] [LSan] Don't run `c_maxsat_example` with LeakSanitizer
 because it contains leaks that the Z3 developers don't intend to fix.

---
 contrib/ci/scripts/sanitizer_env.sh          | 13 +++++++++++++
 contrib/ci/scripts/test_z3_examples_cmake.sh | 10 +++++++---
 2 files changed, 20 insertions(+), 3 deletions(-)

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.

From 8d600050dbd9c73c58152259d91f999f33c19a11 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 11 Oct 2017 08:17:57 +0100
Subject: [PATCH 17/32] [LSan] Remove suppression files. The were fixed on
 rebase

---
 contrib/suppressions/sanitizers/lsan.txt | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
index 81a3c8b85..a4ce0881a 100644
--- a/contrib/suppressions/sanitizers/lsan.txt
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -1,8 +1 @@
 # LeakSanitizer suppression file
-
-# FIXME: This looks a bug in Clang/LSan the error reported
-# doesn't make sense. See https://github.com/Z3Prover/z3/issues/1297
-leak:_fini
-# FIXME: I don't understand this leak.
-# See https://github.com/Z3Prover/z3/issues/1297
-leak:error_code_example2

From db7b2e989db5a597812f0153827155a8b909e7c1 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 11 Oct 2017 17:27:39 +0100
Subject: [PATCH 18/32] [TravisCI] Try to run the Python and .NET examples
 under ASan.

---
 .travis.yml                                   |  2 +-
 contrib/ci/Dockerfiles/z3_build.Dockerfile    |  2 ++
 contrib/ci/scripts/ci_defaults.sh             |  1 +
 contrib/ci/scripts/sanitizer_env.sh           | 32 ++++++++++++++++++
 contrib/ci/scripts/test_z3_examples_cmake.sh  | 33 +++++++++++++------
 .../ci/scripts/travis_ci_linux_entry_point.sh |  4 +++
 6 files changed, 63 insertions(+), 11 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 534aeacf0..940f15f98 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,7 +21,7 @@ env:
     # 64-bit UBSan Debug build
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
     # 64-bit ASan Debug build
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
 
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 0b6d0ac0d..5b9ac9442 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -5,6 +5,7 @@ FROM ${DOCKER_IMAGE_BASE}
 # Build arguments. This can be changed when invoking
 # `docker build`.
 ARG ASAN_BUILD
+ARG ASAN_DSO
 ARG BUILD_DOCS
 ARG CC
 ARG CXX
@@ -32,6 +33,7 @@ ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
+  ASAN_DSO=${ASAN_DSO} \
   BUILD_DOCS=${BUILD_DOCS} \
   CC=${CC} \
   CXX=${CXX} \
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
index d8e9376d8..076d70180 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -49,6 +49,7 @@ unset PLATFORM
 # NOTE: The following variables are not set here because
 # they are specific to the CI implementation
 # PYTHON_EXECUTABLE
+# ASAN_DSO
 # Z3_SRC_DIR
 # Z3_BUILD_DIR
 # Z3_SYSTEM_TEST_DIR
diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
index 8cd646ce6..0499eb268 100644
--- a/contrib/ci/scripts/sanitizer_env.sh
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -18,11 +18,43 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then
   function run_no_lsan() {
     ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}"
   }
+
+  # Check path to ASan DSO
+  : ${ASAN_DSO?"ASAN_DSO must be specified"}
+  if [ ! -e "${ASAN_DSO}" ]; then
+    echo "ASAN_DSO (${ASAN_DSO}) does not exist"
+    exit 1
+  fi
+  # FIXME: We'll need to refactor this when we can do UBSan builds
+  # against a UBSan DSO.
+  function run_non_native_binding() {
+    # We need to preload the ASan DSO that libz3
+    # will have undefined references to.
+    # Don't run leak checking because we get lots reported leaks
+    # in the language runtime (e.g. python).
+    PLATFORM="$(uname -s)"
+    case "${PLATFORM}" in
+      Linux*)
+        LD_PRELOAD="${ASAN_DSO}" run_no_lsan "${@}"
+      ;;
+      Darwin*)
+        DYLD_INSERT_LIBRARIES="${ASAN_DSO}" run_no_lsan "${@}"
+      ;;
+      *)
+        echo "Unknown platform \"${PLATFORM}\""
+        exit 1
+      ;;
+    esac
+    unset PLATFORM
+  }
 else
   # In non-ASan build just run directly
   function run_no_lsan() {
     "${@}"
   }
+  function run_non_native_binding() {
+    "${@}"
+  }
 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 477f7f747..515027509 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -64,16 +64,21 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
   # `all_interval_series.py` produces a lot of output so just throw
   # away output.
   # TODO: This example is slow should we remove it from testing?
-  run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py
-  run_quiet ${PYTHON_EXECUTABLE} python/complex.py
-  run_quiet ${PYTHON_EXECUTABLE} python/example.py
+  if [ "X${ASAN_BUILD}" = "X1" -a "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
+    # Too slow when doing ASan Debug build
+    echo "Skipping all_interval_series.py under ASan Debug build"
+  else
+    run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py
+  fi
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/complex.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/example.py
   # FIXME: `hamiltonian.py` example is disabled because its too slow.
   #${PYTHON_EXECUTABLE} python/hamiltonian.py
-  run_quiet ${PYTHON_EXECUTABLE} python/marco.py
-  run_quiet ${PYTHON_EXECUTABLE} python/mss.py
-  run_quiet ${PYTHON_EXECUTABLE} python/socrates.py
-  run_quiet ${PYTHON_EXECUTABLE} python/visitor.py
-  run_quiet ${PYTHON_EXECUTABLE} python/z3test.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/marco.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/mss.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/socrates.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/visitor.py
+  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/z3test.py
 fi
 
 if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
@@ -81,7 +86,7 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
   # FIXME: Move compliation step into CMake target
   mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll
   # Run .NET example
-  run_quiet mono ./dotnet_test.exe
+  run_non_native_binding run_quiet mono ./dotnet_test.exe
 fi
 
 if [ "X${JAVA_BINDINGS}" = "X1" ]; then
@@ -98,6 +103,14 @@ if [ "X${JAVA_BINDINGS}" = "X1" ]; then
     # Assume Linux for now
     export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
   fi
-  run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+  if [ "X${ASAN_BUILD}" = "X1" ]; then
+    # The JVM seems to crash (SEGV) if we pre-load ASan
+    # so don't run it for now.
+    echo "Skipping JavaExample under ASan build"
+  else
+    run_non_native_binding \
+      run_quiet \
+        java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+  fi
 fi
 
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index bd2c9d2d1..d60b06f8f 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -84,6 +84,10 @@ if [ -n "${ASAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
 fi
 
+if [ -n "${ASAN_DSO}" ]; then
+  BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}")
+fi
+
 if [ -n "${UBSAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
 fi

From 675a3ae9dd14f8dbda6d9d017566279e716b0c68 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 14 Oct 2017 22:40:42 +0100
Subject: [PATCH 19/32] [UBSan] Remove a bunch of suppressions.

---
 contrib/suppressions/sanitizers/ubsan.txt | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/contrib/suppressions/sanitizers/ubsan.txt b/contrib/suppressions/sanitizers/ubsan.txt
index 6ceacd400..4d19e40be 100644
--- a/contrib/suppressions/sanitizers/ubsan.txt
+++ b/contrib/suppressions/sanitizers/ubsan.txt
@@ -1,20 +1,7 @@
 # UndefinedBehavior sanitizer suppression file
 # FIXME: UBSan doesn't usually have false positives so we need to fix all of these!
 
-# Occurs when running C API example (`interpolation_example`)
-# See https://github.com/Z3Prover/z3/issues/1286
-null:iz3mgr.h
-
-# Occurs when running C++ API example
-# See https://github.com/Z3Prover/z3/issues/1287
-function:api_context.cpp
-
 # Occurs when running tptp example
 # See https://github.com/Z3Prover/z3/issues/964
 null:rational.h
 null:mpq.h
-
-# Occurs when running `test-z3 /a`
-# See https://github.com/Z3Prover/z3/issues/1288
-shift-exponent:tbv.cpp
-signed-integer-overflow:mpz.cpp

From fd391e75a6afdc997322d87371b2228b419b2296 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 11:54:05 +0100
Subject: [PATCH 20/32] [TravisCI] Fix `Z3_BUILD_TYPE` variable that was not
 propagated into the Docker image as an environment variable.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 5b9ac9442..562c2dfe5 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -52,6 +52,7 @@ ENV \
   USE_OPENMP=${USE_OPENMP} \
   Z3_SRC_DIR=${Z3_SRC_DIR} \
   Z3_BUILD_DIR=/home/user/z3_build \
+  Z3_BUILD_TYPE=${Z3_BUILD_TYPE} \
   Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
   Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
   Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \

From 2dd1a4046d1579a3f953b53cb1b613c289cd51f4 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 12:02:13 +0100
Subject: [PATCH 21/32] [TravisCI] Fix typo

---
 contrib/ci/scripts/test_z3_system_tests.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index 71ecf2a1e..bcffaf56e 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -28,7 +28,7 @@ Z3_LIB_DIR="${Z3_BUILD_DIR}"
 Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}"
 
 # Clone repo to destination
-mkdir -p "${Z3_SYSTEM_TEST_GIT_URL}"
+mkdir -p "${Z3_SYSTEM_TEST_DIR}"
 git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
 cd "${Z3_SYSTEM_TEST_DIR}"
 

From fd98593a5882075df3afa4c63cb47ebd7f73abee Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 12:19:16 +0100
Subject: [PATCH 22/32] [ASan] Ignore Clang OpenMP leaks for now.

---
 contrib/suppressions/sanitizers/lsan.txt | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/contrib/suppressions/sanitizers/lsan.txt b/contrib/suppressions/sanitizers/lsan.txt
index a4ce0881a..1480b7c09 100644
--- a/contrib/suppressions/sanitizers/lsan.txt
+++ b/contrib/suppressions/sanitizers/lsan.txt
@@ -1 +1,5 @@
 # LeakSanitizer suppression file
+
+# Ignore Clang OpenMP leaks.
+# See https://github.com/Z3Prover/z3/issues/1308
+leak:___kmp_allocate

From 35f6746c60a40eeb3c3356e6a8652f72792a1c30 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 13:21:40 +0100
Subject: [PATCH 23/32] Workaround `regressions/smt2/error.smt2` test timing
 out.

When ASan's LeakSanitizer is enabled leak checking is triggered
when `exit()` is called and it returns so many false positives that
it takes a long time to write them to the console.

To workaround this we simply call `_Exit()` instead.
---
 src/parsers/smt2/smt2parser.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b8ad7e610..b43ee9f6e 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -444,7 +444,10 @@ namespace smt2 {
                 m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
             }
             if (m_ctx.exit_on_error()) {
-                exit(1);
+                // WORKAROUND: ASan's LeakSanitizer reports many false positives when
+                // calling `exit()` so call `_Exit()` instead which avoids invoking leak
+                // checking.
+                _Exit(1);
             }
         }
 

From ad2a0a0085773e1279526dce7b7bfaf167caeb40 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 15:27:10 +0100
Subject: [PATCH 24/32] [TravisCI] Don't print sanitizer suppressions by
 default because that breaks Z3's regression tests.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile     |  2 ++
 contrib/ci/README.md                           |  1 +
 contrib/ci/scripts/ci_defaults.sh              |  4 ++++
 contrib/ci/scripts/sanitizer_env.sh            | 18 +++++++++++++++---
 .../ci/scripts/travis_ci_linux_entry_point.sh  |  4 ++++
 5 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 562c2dfe5..152b109d7 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -16,6 +16,7 @@ ARG PYTHON_BINDINGS
 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
 ARG RUN_SYSTEM_TESTS
 ARG RUN_UNIT_TESTS
+ARG SANITIZER_PRINT_SUPPRESSIONS
 ARG TARGET_ARCH
 ARG TEST_INSTALL
 ARG UBSAN_BUILD
@@ -42,6 +43,7 @@ ENV \
   NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
   PYTHON_BINDINGS=${PYTHON_BINDINGS} \
   PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
+  SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
   RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
   RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
   TARGET_ARCH=${TARGET_ARCH} \
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 99bbcd7a6..95ed7f398 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -32,6 +32,7 @@ the future.
 * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
 * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
 * `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
+* `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`)
 * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
 * `TEST_INSTALL` - Test running `install` target (`0` or `1`)
 * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
index 076d70180..2029981c0 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -11,6 +11,10 @@ export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
 export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
 export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
 export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
+# Don't print suppressions by default because that breaks the Z3
+# regression tests because they don't expect them to appear in Z3's
+# output.
+export SANITIZER_PRINT_SUPPRESSIONS="${SANITIZER_PRINT_SUPPRESSIONS:-0}"
 export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
 export TEST_INSTALL="${TEST_INSTALL:-1}"
 export UBSAN_BUILD="${UBSAN_BUILD:-0}"
diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
index 0499eb268..959f136e5 100644
--- a/contrib/ci/scripts/sanitizer_env.sh
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -7,11 +7,18 @@
 
 if [ "X${ASAN_BUILD}" = "X1" ]; then
   # Use suppression files
-  export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
+  export LSAN_OPTIONS="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"
+  export ASAN_OPTIONS="malloc_context_size=100,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
+
+  : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
+  if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
+    export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1"
+    export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1"
+  fi
+
   : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
 
   # Run command without checking for leaks
@@ -61,5 +68,10 @@ if [ "X${UBSAN_BUILD}" = "X1" ]; then
   # `halt_on_error=1,abort_on_error=1` means that on the first UBSan error
   # the program will terminate by calling `abort(). Without this UBSan will
   # allow execution to continue. We also use a suppression file.
-  export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
+  export UBSAN_OPTIONS="halt_on_error=1,abort_on_error=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/ubsan.txt"
+
+  : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
+  if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
+    export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1"
+  fi
 fi
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index d60b06f8f..352e13de0 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -88,6 +88,10 @@ if [ -n "${ASAN_DSO}" ]; then
   BUILD_OPTS+=("--build-arg" "ASAN_DSO=${ASAN_DSO}")
 fi
 
+if [ -n "${SANITIZER_PRINT_SUPPRESSIONS}" ]; then
+  BUILD_OPTS+=("--build-arg" "SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS}")
+fi
+
 if [ -n "${UBSAN_BUILD}" ]; then
   BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
 fi

From ecadef6e48460cdbb271c13817534b357bd92341 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 17:25:12 +0100
Subject: [PATCH 25/32] [TravisCI] Try to fix case in `run_quiet` where the
 script would fail with.

```
-ne: unary operator expected
```
---
 contrib/ci/scripts/run_quiet.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/ci/scripts/run_quiet.sh b/contrib/ci/scripts/run_quiet.sh
index 5abc910e8..0f49da3be 100644
--- a/contrib/ci/scripts/run_quiet.sh
+++ b/contrib/ci/scripts/run_quiet.sh
@@ -34,8 +34,8 @@ function run_quiet() {
     fi
     # Clean up
     rm "${STDOUT}" "${STDERR}"
-    [ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e
-    [ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x
+    [ "$( echo "${OLD_SETTINGS}" | grep -c 'e')" != "0" ] && set -e
+    [ "$( echo "${OLD_SETTINGS}" | grep -c 'x')" != "0" ] && set -x
     return ${EXIT_STATUS}
   fi
 }

From ead6e56d15432384ece80361dd1969c2367a0fe2 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 17:41:40 +0100
Subject: [PATCH 26/32] [TravisCI] Swap `run_quiet` and
 `run_non_native_binding`. In the previous order `grep` inside `run_quiet`
 would get ASan LD_PRELOAD'ed which would sometimes fail.

---
 contrib/ci/scripts/test_z3_examples_cmake.sh | 22 ++++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index 515027509..9979b8773 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -68,17 +68,17 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
     # Too slow when doing ASan Debug build
     echo "Skipping all_interval_series.py under ASan Debug build"
   else
-    run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py
+    run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/all_interval_series.py
   fi
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/complex.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/example.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/complex.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/example.py
   # FIXME: `hamiltonian.py` example is disabled because its too slow.
   #${PYTHON_EXECUTABLE} python/hamiltonian.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/marco.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/mss.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/socrates.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/visitor.py
-  run_non_native_binding run_quiet ${PYTHON_EXECUTABLE} python/z3test.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/marco.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/mss.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/socrates.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/visitor.py
+  run_quiet run_non_native_binding ${PYTHON_EXECUTABLE} python/z3test.py
 fi
 
 if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
@@ -86,7 +86,7 @@ if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
   # FIXME: Move compliation step into CMake target
   mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll
   # Run .NET example
-  run_non_native_binding run_quiet mono ./dotnet_test.exe
+  run_quiet run_non_native_binding mono ./dotnet_test.exe
 fi
 
 if [ "X${JAVA_BINDINGS}" = "X1" ]; then
@@ -108,8 +108,8 @@ if [ "X${JAVA_BINDINGS}" = "X1" ]; then
     # so don't run it for now.
     echo "Skipping JavaExample under ASan build"
   else
-    run_non_native_binding \
-      run_quiet \
+    run_quiet \
+      run_non_native_binding \
         java -cp .:examples/java:com.microsoft.z3.jar JavaExample
   fi
 fi

From e51ce8bcafc585ee23bea555f2c91a22646445ef Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 19:54:50 +0100
Subject: [PATCH 27/32] [TravisCI] Try again to not show suppressions by
 default

---
 contrib/ci/scripts/sanitizer_env.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/contrib/ci/scripts/sanitizer_env.sh b/contrib/ci/scripts/sanitizer_env.sh
index 959f136e5..f1fa87442 100644
--- a/contrib/ci/scripts/sanitizer_env.sh
+++ b/contrib/ci/scripts/sanitizer_env.sh
@@ -17,6 +17,9 @@ if [ "X${ASAN_BUILD}" = "X1" ]; then
   if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
     export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=1"
     export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=1"
+  else
+    export LSAN_OPTIONS="${LSAN_OPTIONS},print_suppressions=0"
+    export ASAN_OPTIONS="${ASAN_OPTIONS},print_suppressions=0"
   fi
 
   : ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
@@ -73,5 +76,7 @@ if [ "X${UBSAN_BUILD}" = "X1" ]; then
   : ${SANITIZER_PRINT_SUPPRESSIONS?"SANITIZER_PRINT_SUPPRESSIONS must be specified"}
   if [ "X${SANITIZER_PRINT_SUPPRESSIONS}" = "X1" ]; then
     export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=1"
+  else
+    export UBSAN_OPTIONS="${UBSAN_OPTIONS},print_suppressions=0"
   fi
 fi

From dbb7f616c157359eaaeee9b9a340217a8b522521 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 15 Oct 2017 21:36:02 +0100
Subject: [PATCH 28/32] More LSan workarounds.

---
 src/cmd_context/cmd_context.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 95c030687..9615e86ce 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1608,7 +1608,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
             throw cmd_exception("check annotation that says unsat");
 #else
             diagnostic_stream() << "BUG: incompleteness" << std::endl;
-            exit(ERR_INCOMPLETENESS);
+            // WORKAROUND: `exit()` causes LSan to be invoked and produce
+            // many false positives.
+            _Exit(ERR_INCOMPLETENESS);
 #endif
         }
         break;
@@ -1618,7 +1620,9 @@ void cmd_context::validate_check_sat_result(lbool r) {
             throw cmd_exception("check annotation that says sat");
 #else
             diagnostic_stream() << "BUG: unsoundness" << std::endl;
-            exit(ERR_UNSOUNDNESS);
+            // WORKAROUND: `exit()` causes LSan to be invoked and produce
+            // many false positives.
+            _Exit(ERR_UNSOUNDNESS);
 #endif
         }
         break;

From 88fb31ac089a4220fc25f3d3917d88a2af746eca Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 16 Oct 2017 08:50:50 +0100
Subject: [PATCH 29/32] [TravisCI] Add `RUN_API_EXAMPLES` option so that we can
 disable building/running examples in some configurations.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile        | 2 ++
 contrib/ci/README.md                              | 1 +
 contrib/ci/scripts/ci_defaults.sh                 | 1 +
 contrib/ci/scripts/test_z3_examples_cmake.sh      | 6 ++++++
 contrib/ci/scripts/travis_ci_linux_entry_point.sh | 4 ++++
 5 files changed, 14 insertions(+)

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 152b109d7..eb2e03a43 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -14,6 +14,7 @@ ARG JAVA_BINDINGS
 ARG NO_SUPPRESS_OUTPUT
 ARG PYTHON_BINDINGS
 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
+ARG RUN_API_EXAMPLES
 ARG RUN_SYSTEM_TESTS
 ARG RUN_UNIT_TESTS
 ARG SANITIZER_PRINT_SUPPRESSIONS
@@ -44,6 +45,7 @@ ENV \
   PYTHON_BINDINGS=${PYTHON_BINDINGS} \
   PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
   SANITIZER_PRINT_SUPPRESSIONS=${SANITIZER_PRINT_SUPPRESSIONS} \
+  RUN_API_EXAMPLES=${RUN_API_EXAMPLES} \
   RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
   RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
   TARGET_ARCH=${TARGET_ARCH} \
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 95ed7f398..bd1c52792 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -30,6 +30,7 @@ the future.
 * `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`)
 * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
 * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
+* `RUN_API_EXAMPLES` - Build and run API examples (`0` or `1`)
 * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
 * `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
 * `SANITIZER_PRINT_SUPPRESSIONS` - Show ASan/UBSan suppressions (`0` or `1`)
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
index 2029981c0..7a4434bd5 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -9,6 +9,7 @@ export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
 export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
 export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
 export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
+export RUN_API_EXAMPLES="${RUN_API_EXAMPLES:-1}"
 export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
 export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
 # Don't print suppressions by default because that breaks the Z3
diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh
index 9979b8773..687efebb4 100755
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@@ -15,6 +15,12 @@ set -o pipefail
 : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
 : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
 : ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
+: ${RUN_API_EXAMPLES?"RUN_API_EXAMPLES must be specified"}
+
+if [ "X${RUN_API_EXAMPLES}" = "X0" ]; then
+  echo "Skipping run of API examples"
+  exit 0
+fi
 
 # Set compiler flags
 source ${SCRIPT_DIR}/set_compiler_flags.sh
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index 352e13de0..731ea9ff0 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -100,6 +100,10 @@ if [ -n "${TEST_INSTALL}" ]; then
   BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
 fi
 
+if [ -n "${RUN_API_EXAMPLES}" ]; then
+  BUILD_OPTS+=("--build-arg" "RUN_API_EXAMPLES=${RUN_API_EXAMPLES}")
+fi
+
 if [ -n "${RUN_SYSTEM_TESTS}" ]; then
   BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
 fi

From 8835b54d1669d54d9595287a015acdf39e84a55c Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 16 Oct 2017 08:55:57 +0100
Subject: [PATCH 30/32] [TravisCI] Add ASan/UBSan configuration that runs unit
 tests.

---
 .travis.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 940f15f98..a3ffb221e 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -17,11 +17,14 @@ env:
 ###############################################################################
 # Ubuntu 16.04 LTS
 ###############################################################################
-    # FIXME: We should really run the unit tests too under ASan/UBSan but a debug build is too slow.
     # 64-bit UBSan Debug build
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug UBSAN_BUILD=1 RUN_UNIT_TESTS=SKIP
     # 64-bit ASan Debug build
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug ASAN_BUILD=1 RUN_UNIT_TESTS=SKIP ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so
+    # Build for running unit tests under ASan/UBSan
+    # FIXME: We should really be doing a debug build but the unit tests run too
+    # slowly when we do that.
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo ASAN_BUILD=1 RUN_UNIT_TESTS=BUILD_AND_RUN ASAN_DSO=/usr/lib/clang/3.9/lib/linux/libclang_rt.asan-x86_64.so UBSAN_BUILD=1 RUN_API_EXAMPLES=0 RUN_SYSTEM_TESTS=0 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
 
     # 64-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo

From a1b6316e2e3ae19e9e8f67af6e17c13771d73c81 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 16 Oct 2017 09:49:54 +0100
Subject: [PATCH 31/32] [TravisCI] Try to unbreak running Python regression
 tests under ASan.

---
 contrib/ci/scripts/test_z3_system_tests.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index bcffaf56e..6f9901687 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -58,7 +58,7 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
     # to work.
     echo "FIXME: Skipping python binding tests when building with UBSan"
   else
-    ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+    run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
   fi
 fi
 

From 7c99721b60e9f5a8e6a2fe502ff56380e808916b Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 16 Oct 2017 13:21:03 +0100
Subject: [PATCH 32/32] [TravisCI] Don't run Python regression tests under ASan
 for now. The script that runs them doesn't propagate LD_PRELOAD and so the
 tests fail.

---
 contrib/ci/scripts/test_z3_system_tests.sh | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh
index 6f9901687..19c179268 100755
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@@ -57,6 +57,11 @@ if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
     # FIXME: We need to build libz3 with a shared UBSan runtime for the bindings
     # to work.
     echo "FIXME: Skipping python binding tests when building with UBSan"
+  elif [ "X${ASAN_BUILD}" = "X1" ]; then
+    # FIXME: The `test_pyscripts.py` doesn't propagate LD_PRELOAD
+    # so under ASan the tests fail to run
+    # to work.
+    echo "FIXME: Skipping python binding tests when building with ASan"
   else
     run_non_native_binding ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
   fi