From 53fc6ac11b25593e3827c943f5d61ce9f28da7ca Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 5 Oct 2017 14:27:56 +0100
Subject: [PATCH 1/7] [TravisCI] Refactor as many CI default options as
 possible so that the Docker and "TravisCI macOS" builds share most of the
 same defaults by sourcing the `ci_defaults.sh` file.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile    | 50 ++++++++---------
 contrib/ci/scripts/ci_defaults.sh             | 54 +++++++++++++++++++
 .../ci/scripts/travis_ci_linux_entry_point.sh |  4 +-
 .../ci/scripts/travis_ci_osx_entry_point.sh   | 30 ++---------
 4 files changed, 86 insertions(+), 52 deletions(-)
 create mode 100644 contrib/ci/scripts/ci_defaults.sh

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 2d16d5394..5f7608cf4 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE
 FROM ${DOCKER_IMAGE_BASE}
 
 
-# Specify defaults. This can be changed when invoking
+# Build arguments. This can be changed when invoking
 # `docker build`.
-ARG ASAN_BUILD=0
-ARG BUILD_DOCS=0
-ARG CC=gcc
-ARG CXX=g++
-ARG DOTNET_BINDINGS=1
-ARG JAVA_BINDINGS=1
-ARG NO_SUPPRESS_OUTPUT=0
-ARG PYTHON_BINDINGS=1
-ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
-ARG RUN_SYSTEM_TESTS=1
-ARG RUN_UNIT_TESTS=1
-ARG TARGET_ARCH=x86_64
-ARG TEST_INSTALL=1
-ARG UBSAN_BUILD=0
-ARG USE_LIBGMP=0
-ARG USE_LTO=0
-ARG USE_OPENMP=1
+ARG ASAN_BUILD
+ARG BUILD_DOCS
+ARG CC
+ARG CXX
+ARG DOTNET_BINDINGS
+ARG JAVA_BINDINGS
+ARG NO_SUPPRESS_OUTPUT
+ARG PYTHON_BINDINGS
+ARG PYTHON_EXECUTABLE
+ARG RUN_SYSTEM_TESTS
+ARG RUN_UNIT_TESTS
+ARG TARGET_ARCH
+ARG TEST_INSTALL
+ARG UBSAN_BUILD
+ARG USE_LIBGMP
+ARG USE_LTO
+ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
-ARG Z3_BUILD_TYPE=RelWithDebInfo
-ARG Z3_CMAKE_GENERATOR=Ninja
-ARG Z3_INSTALL_PREFIX=/usr
-ARG Z3_STATIC_BUILD=0
-# Blank default indicates use latest.
+ARG Z3_BUILD_TYPE
+ARG Z3_CMAKE_GENERATOR
+ARG Z3_INSTALL_PREFIX
+ARG Z3_STATIC_BUILD
 ARG Z3_SYSTEM_TEST_GIT_REVISION
-ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY
-ARG Z3_VERBOSE_BUILD_OUTPUT=0
+ARG Z3_WARNINGS_AS_ERRORS
+ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
@@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
 
 ADD \
   /contrib/ci/scripts/build_z3_cmake.sh \
+  /contrib/ci/scripts/ci_defaults.sh \
   /contrib/ci/scripts/set_compiler_flags.sh \
   /contrib/ci/scripts/set_generator_args.sh \
   ${Z3_SRC_DIR}/contrib/ci/scripts/
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
new file mode 100644
index 000000000..354ea95b7
--- /dev/null
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -0,0 +1,54 @@
+# This file should be sourced by other scripts
+# and not executed directly
+
+# Set CI build defaults
+
+export ASAN_BUILD="${ASAN_BUILD:-0}"
+export BUILD_DOCS="${BUILD_DOCS:-0}"
+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 PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
+export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
+export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
+export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
+export TEST_INSTALL="${TEST_INSTALL:-1}"
+export UBSAN_BUILD="${UBSAN_BUILD:-0}"
+export USE_LIBGMP="${USE_LIBGMP:-0}"
+export USE_LTO="${USE_LTO:-0}"
+export USE_OPENMP="${USE_OPENMP:-1}"
+
+export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
+export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
+export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
+# Default is blank which means get latest revision
+export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}"
+export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
+export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
+
+# Platform specific defaults
+PLATFORM="$(uname -s)"
+case "${PLATFORM}" in
+  Linux*)
+    export C_COMPILER="${C_COMPILER:-gcc}"
+    export CXX_COMPILER="${CXX_COMPILER:-g++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}"
+  ;;
+  Darwin*)
+    export C_COMPILER="${C_COMPILER:-clang}"
+    export CXX_COMPILER="${CXX_COMPILER:-clang++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
+  ;;
+  *)
+    echo "Unknown platform \"${PLATFORM}\""
+    exit 1
+  ;;
+esac
+unset PLATFORM
+
+# NOTE: The following variables are not set here because
+# they are specific to the CI implementation
+# Z3_SRC_DIR
+# Z3_BUILD_DIR
+# Z3_SYSTEM_TEST_DIR
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index 84b2dd400..c0f856faa 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -11,13 +11,15 @@ DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)"
 : ${LINUX_BASE?"LINUX_BASE must be specified"}
 
 
-
 # Sanity check. Current working directory should be repo root
 if [ ! -f "./README.md" ]; then
   echo "Current working directory should be repo root"
   exit 1
 fi
 
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
+
 BUILD_OPTS=()
 # Override options if they have been provided.
 # Otherwise the defaults in the Docker file will be used
diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
index c5e8b4c02..7dd566877 100755
--- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
@@ -6,26 +6,8 @@ set -x
 set -e
 set -o pipefail
 
-# Set defaults
-# FIXME: Refactor this so we don't need to stay in sync with
-# `z3_build.Dockerfile`.
-export ASAN_BUILD="${ASAN_BUILD:-0}"
-export BUILD_DOCS="${BUILD_DOCS:-0}"
-export C_COMPILER="${C_COMPILER:-clang}"
-export CXX_COMPILER="${CXX_COMPILER:-clang++}"
-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 PYTHON_EXECUTABLE="$(which python)"
-export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
-export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
-export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
-export TEST_INSTALL="${TEST_INSTALL:-1}"
-export UBSAN_BUILD="${UBSAN_BUILD:-0}"
-export USE_LIBGMP="${USE_LIBGMP:-0}"
-export USE_LTO="${USE_LTO:-0}"
-export USE_OPENMP="${USE_OPENMP:-1}"
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
 
 if [ -z "${TRAVIS_BUILD_DIR}" ]; then
   echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository"
@@ -37,15 +19,11 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
   exit 1
 fi
 
+# These three variables are specific to the macOS TravisCI
+# implementation and are not set in `ci_defaults.sh`.
 export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}"
 export Z3_BUILD_DIR="${Z3_SRC_DIR}/build"
-export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
-export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
-export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
-export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
 export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"
-export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
-export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
 
 # Overwrite whatever what set in TravisCI
 export CC="${C_COMPILER}"

From eb975a49d606bcdb076b523d0506bf855ef8d267 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 5 Oct 2017 14:44:41 +0100
Subject: [PATCH 2/7] [TravisCI] Fix bug where `Z3_BUILD_TYPE` was not being
 passed as a Docker build argument.

Also update an out of date comment.
---
 contrib/ci/scripts/travis_ci_linux_entry_point.sh | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index c0f856faa..bd2c9d2d1 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -21,8 +21,11 @@ fi
 source "${SCRIPT_DIR}/ci_defaults.sh"
 
 BUILD_OPTS=()
-# Override options if they have been provided.
-# Otherwise the defaults in the Docker file will be used
+# Pass Docker build arguments
+if [ -n "${Z3_BUILD_TYPE}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}")
+fi
+
 if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
   BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
 fi

From 0633d5819f8b996b3300f177efe6b1406a1285a5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 5 Oct 2017 15:09:16 +0100
Subject: [PATCH 3/7] [TravisCI] Fix bug. `PYTHON_EXECUTABLE` should not be in
 common defaults. The location is dependent on the implementation.

This triggered a build failure on TravisCI because the location
of the default Python binary is different to what is in the Docker
container.
---
 contrib/ci/Dockerfiles/z3_build.Dockerfile      | 2 +-
 contrib/ci/scripts/ci_defaults.sh               | 2 +-
 contrib/ci/scripts/travis_ci_osx_entry_point.sh | 3 ++-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 5f7608cf4..07504e6b9 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -12,7 +12,7 @@ ARG DOTNET_BINDINGS
 ARG JAVA_BINDINGS
 ARG NO_SUPPRESS_OUTPUT
 ARG PYTHON_BINDINGS
-ARG PYTHON_EXECUTABLE
+ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
 ARG RUN_SYSTEM_TESTS
 ARG RUN_UNIT_TESTS
 ARG TARGET_ARCH
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
index 354ea95b7..2fb3fa52a 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -9,7 +9,6 @@ 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 PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
 export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
 export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
 export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
@@ -49,6 +48,7 @@ unset PLATFORM
 
 # NOTE: The following variables are not set here because
 # they are specific to the CI implementation
+# PYTHON_EXECUTABLE
 # Z3_SRC_DIR
 # Z3_BUILD_DIR
 # Z3_SYSTEM_TEST_DIR
diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
index 7dd566877..ad3b0c7ab 100755
--- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
@@ -19,8 +19,9 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
   exit 1
 fi
 
-# These three variables are specific to the macOS TravisCI
+# These variables are specific to the macOS TravisCI
 # implementation and are not set in `ci_defaults.sh`.
+export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
 export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}"
 export Z3_BUILD_DIR="${Z3_SRC_DIR}/build"
 export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"

From d47aea398730634444bd31172fd2a04739a9efa7 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 11:23:44 +0100
Subject: [PATCH 4/7] [TravisCI] Workaround slow unit test execution for Debug
 builds.

Unit tests execute very slowly in Debug (i.e. unoptimized) builds.  This
causes TravisCI to terminate the job due to no console output being
seen.

To workaround this for the debug builds the tests are just compiled
but not executed. To implement this the `RUN_UNIT_TESTS` environment
variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`,
and `SKIP` rather than `0` or `1`.
---
 .travis.yml                                   | 11 ++++--
 contrib/ci/README.md                          |  2 +-
 contrib/ci/scripts/ci_defaults.sh             |  2 +-
 .../ci/scripts/test_z3_unit_tests_cmake.sh    | 36 ++++++++++++++-----
 4 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 50d63e593..ac00ef918 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,10 +22,17 @@ env:
     # 64-bit Clang 3.9 RelWithDebInfo
     - 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
 
+    # Debug builds
+    #
+    # Note the unit tests for the debug builds are compiled but **not**
+    # executed. This is because the debug build of unit tests takes a large
+    # amount of time to execute compared to the optimized builds. The hope is
+    # that just running the optimized unit tests is sufficient.
+    #
     # 64-bit GCC 5.4 Debug
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
     # 64-bit Clang Debug
-    - 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
+    - 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 RUN_UNIT_TESTS=BUILD_ONLY
 
     # 32-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 2e117c8b1..e4c9aecfd 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -31,7 +31,7 @@ the future.
 * `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_SYSTEM_TESTS` - Run system tests (`0` or `1`)
-* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`)
+* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
 * `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 2fb3fa52a..d8e9376d8 100644
--- a/contrib/ci/scripts/ci_defaults.sh
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -10,7 +10,7 @@ export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
 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:-1}"
+export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
 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/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
index 666673328..e1c927f58 100755
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
@@ -10,17 +10,35 @@ set -o pipefail
 : ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
 : ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
 
-if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then
-  echo "Skipping unit tests"
-  exit 0
-fi
-
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
 cd "${Z3_BUILD_DIR}"
 
-# Build and run internal tests
-cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
-# Run all tests that don't require arguments
-run_quiet ./test-z3 /a
+function build_unit_tests() {
+  # Build internal tests
+  cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
+}
+
+function run_unit_tests() {
+  # Run all tests that don't require arguments
+  run_quiet ./test-z3 /a
+}
+
+case "${RUN_UNIT_TESTS}" in
+  BUILD_AND_RUN)
+    build_unit_tests
+    run_unit_tests
+  ;;
+  BUILD_ONLY)
+    build_unit_tests
+  ;;
+  SKIP)
+    echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run"
+    exit 0
+  ;;
+  *)
+    echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\""
+    exit 1
+  ;;
+esac

From 2519719d3f452eb2cbbaf0db822e58b671e4e74f Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 11:30:06 +0100
Subject: [PATCH 5/7] Fix typo

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

diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh
index 0ef7b76aa..a704c518b 100644
--- a/contrib/ci/scripts/set_generator_args.sh
+++ b/contrib/ci/scripts/set_generator_args.sh
@@ -1,4 +1,4 @@
-# This script should is intended to be included by other
+# This script is intended to be included by other
 # scripts and should not be executed directly
 
 : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}

From 0be28b66fe3319be01492a0391514727e099916c Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 11:48:20 +0100
Subject: [PATCH 6/7] [TravisCI] Update out of date `README.md` file.

---
 contrib/ci/README.md | 46 ++++++++++++++++++++++++++++++++++++++------
 1 file changed, 40 insertions(+), 6 deletions(-)

diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index e4c9aecfd..99bbcd7a6 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script
    variables (if set) into the build using the `--build-arg` argument of the `docker run`
    command.
 
-If an environemnt variable is not set a defaults value is used which can be
-found in `Dockerfiles/z3_build.Dockerfile`.
+The default values of the configuration environment variables
+can be found in
+[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh).
 
 #### Linux specific configuration variables
 
@@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`.
 
 #### Reproducing a build locally
 
-A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh`
-script and setting the appropriate environment variable.
+A build can be reproduced locally by using the
+`scripts/travis_ci_linux_entry_point.sh` script and setting the appropriate
+environment variable.
 
 For example lets say we wanted to reproduce the build below.
 
@@ -104,11 +106,43 @@ feature might be removed in the future.
 
 It may be better to just build the base image once (outside of TravisCI), upload
 it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built
-image everytime.
+image every time.
 
 An [organization](https://hub.docker.com/u/z3prover/) has been created on
 DockerHub for this.
 
 ### macOS
 
-Not yet implemented.
+For macOS we execute directly on TravisCI's macOS environment.  The entry point
+for the TravisCI builds is the
+[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh)
+scripts.
+
+#### macOS specific configuration variables
+
+* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies
+  is skipped. This is useful for local testing if the dependencies are already installed.
+* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded.
+
+#### Reproducing a build locally
+
+To reproduce a build (e.g. like the one shown below)
+
+```yaml
+- os: osx
+  osx_image: xcode8.3
+  # Note: Apple Clang does not support OpenMP
+  env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
+```
+
+Run the following:
+
+```bash
+TRAVIS_BUILD_DIR=$(pwd) \
+Z3_BUILD_TYPE=RelWithDebInfo \
+USE_OPEN_MP=0 \
+contrib/ci/scripts/travis_ci_osx_entry_point.sh
+```
+
+Note this assumes that the current working directory is the root of the Z3
+git repository.

From ba8bff76ae9a68bef78c88913cbc2c62a193b299 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 6 Oct 2017 15:52:01 +0100
Subject: [PATCH 7/7] [TravisCI] Modify Debug configuration that I forgot to
 change with `RUN_UNIT_TESTS=BUILD_ONLY`.

---
 .travis.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index ac00ef918..81ddefb8b 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -64,7 +64,7 @@ env:
     # 64-bit GCC 4.8 RelWithDebInfo
     - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
     # 64-bit GCC 4.8 Debug
-    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
 
 # macOS (a.k.a OSX) support
 matrix: