Merge branch 'master' of https://github.com/z3prover/z3

2025-04-08 02:15:19 +00:00 · 2017-07-01 11:48:31 -07:00 · 2017-07-01 11:48:31 -07:00 · c66ec9d3f6
parent 08524a2d90 27ad1813b7
commit c66ec9d3f6
21 changed files with 1107 additions and 3 deletions
--- a/.dockerignore
+++ b/.dockerignore
@ -0,0 +1,4 @@
+**/*.swp
+**/*.pyc
+.git
+**/*.Dockerfile
--- a/.travis.yml
+++ b/.travis.yml
@ -0,0 +1,68 @@
+cache:
+  # This persistent cache is used to cache the building of
+  # docker base images.
+  directories:
+    - $DOCKER_TRAVIS_CI_CACHE_DIR
+sudo: required
+language: cpp
+services:
+  - docker
+env:
+  global:
+    # This environment variable tells the `travis_ci_linux_entry_point.sh`
+    # script to look for a cached Docker image.
+    - DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker
+  # Configurations
+  matrix:
+###############################################################################
+# Ubuntu 16.04 LTS
+###############################################################################
+    # 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
+    - 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
+
+    # 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
+    # 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
+
+    # 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
+
+    # Both of the two configurations below build the docs because the current
+    # implementation uses python as part of the building process.
+    # TODO: Teach one of the configurations to upload built docs somewhere.
+    # Test with Python 3 and API docs
+    - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1
+    # Test with LibGMP and API docs
+    - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7
+
+    # Test without OpenMP
+    - 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 USE_OPENMP=0
+
+    # Unix Makefile generator build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles"
+
+    # LTO build
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1
+
+    # Static build. Note we have disable building the bindings because they won't work with a static libz3
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0
+
+###############################################################################
+# Ubuntu 14.04 LTS
+###############################################################################
+    # GCC 4.8
+    # 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
+
+# TODO: OSX support
+#matrix:
+#  include:
+#    - os: osx
+#      osx_image: xcode 8.2
+script:
+  - contrib/ci/scripts/travis_ci_entry_point.sh
--- a/README.md
+++ b/README.md
@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z

 ## Build status

-| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX |
-| ----------- | ----------- | ---------- | ---------- | ---------- | --- |
-![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)
+| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI |
+| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- |
+![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)

 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile
@ -0,0 +1,50 @@
+# This base image is not officially supported by Docker it
+# is generated by running
+# ```
+# ./update.sh xenial
+# ```
+# from git@github.com:daald/docker-brew-ubuntu-core-32bit.git
+# at commit 34ea593b40b423755b7d46b6c8c89fc8162ea74b
+#
+# We could actually store the image generated by this Dockerfile
+# rather than just the bare image. However given we have a TravisCI
+# cache I'm not sure if it faster to use the TravisCI cache or to
+# download from DockerHub everytime.
+FROM z3prover/ubuntu32:16.04
+
+RUN apt-get update && \
+    apt-get -y --no-install-recommends install \
+        binutils \
+        clang \
+        clang-3.9 \
+        cmake \
+        doxygen \
+        default-jdk \
+        gcc \
+        gcc-5 \
+        git \
+        graphviz \
+        g++ \
+        g++ \
+        libgmp-dev \
+        libgomp1 \
+        libomp5 \
+        libomp-dev \
+        make \
+        mono-devel \
+        ninja-build \
+        python3 \
+        python3-setuptools \
+        python2.7 \
+        python-setuptools \
+        sudo
+
+# Create `user` user for container with password `user`.  and give it
+# password-less sudo access
+RUN useradd -m user && \
+    echo user:user | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+USER user
+WORKDIR /home/user
+
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile
@ -0,0 +1,35 @@
+FROM ubuntu:14.04
+
+RUN apt-get update && \
+    apt-get -y --no-install-recommends install \
+        binutils \
+        clang-3.9 \
+        cmake \
+        doxygen \
+        default-jdk \
+        gcc-multilib \
+        gcc-4.8-multilib \
+        git \
+        graphviz \
+        g++-multilib \
+        g++-4.8-multilib \
+        libgmp-dev \
+        libgomp1 \
+        lib32gomp1 \
+        make \
+        mono-devel \
+        ninja-build \
+        python3 \
+        python3-setuptools \
+        python2.7 \
+        python-setuptools
+
+# Create `user` user for container with password `user`.  and give it
+# password-less sudo access
+RUN useradd -m user && \
+    echo user:user | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+USER user
+WORKDIR /home/user
+
--- a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile
@ -0,0 +1,38 @@
+FROM ubuntu:16.04
+
+RUN apt-get update && \
+    apt-get -y --no-install-recommends install \
+        binutils \
+        clang \
+        clang-3.9 \
+        cmake \
+        doxygen \
+        default-jdk \
+        gcc-multilib \
+        gcc-5-multilib \
+        git \
+        graphviz \
+        g++-multilib \
+        g++-5-multilib \
+        libgmp-dev \
+        libgomp1 \
+        libomp5 \
+        libomp-dev \
+        make \
+        mono-devel \
+        ninja-build \
+        python3 \
+        python3-setuptools \
+        python2.7 \
+        python-setuptools \
+        sudo
+
+# Create `user` user for container with password `user`.  and give it
+# password-less sudo access
+RUN useradd -m user && \
+    echo user:user | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'user  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+USER user
+WORKDIR /home/user
+
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@ -0,0 +1,109 @@
+ARG DOCKER_IMAGE_BASE
+FROM ${DOCKER_IMAGE_BASE}
+
+
+# Specify defaults. 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 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_SYSTEM_TEST_GIT_REVISION
+ARG Z3_VERBOSE_BUILD_OUTPUT=0
+
+ENV \
+  ASAN_BUILD=${ASAN_BUILD} \
+  BUILD_DOCS=${BUILD_DOCS} \
+  CC=${CC} \
+  CXX=${CXX} \
+  DOTNET_BINDINGS=${DOTNET_BINDINGS} \
+  JAVA_BINDINGS=${JAVA_BINDINGS} \
+  NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \
+  PYTHON_BINDINGS=${PYTHON_BINDINGS} \
+  PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
+  RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \
+  RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \
+  TARGET_ARCH=${TARGET_ARCH} \
+  TEST_INSTALL=${TEST_INSTALL} \
+  UBSAN_BUILD=${UBSAN_BUILD} \
+  USE_LIBGMP=${USE_LIBGMP} \
+  USE_LTO=${USE_LTO} \
+  USE_OPENMP=${USE_OPENMP} \
+  Z3_SRC_DIR=${Z3_SRC_DIR} \
+  Z3_BUILD_DIR=/home/user/z3_build \
+  Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \
+  Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \
+  Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
+  Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \
+  Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \
+  Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}
+
+# We add context across incrementally to maximal cache reuse
+
+# Build Z3
+RUN mkdir -p "${Z3_SRC_DIR}" && \
+  mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts"
+# Deliberately leave out `contrib`
+ADD /cmake ${Z3_SRC_DIR}/cmake/
+ADD /doc ${Z3_SRC_DIR}/doc/
+ADD /examples ${Z3_SRC_DIR}/examples/
+ADD /scripts ${Z3_SRC_DIR}/scripts/
+ADD /src ${Z3_SRC_DIR}/src/
+ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
+
+ADD \
+  /contrib/ci/scripts/build_z3_cmake.sh \
+  /contrib/ci/scripts/set_compiler_flags.sh \
+  /contrib/ci/scripts/set_generator_args.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh
+
+# Test building docs
+ADD \
+  /contrib/ci/scripts/test_z3_docs.sh \
+  /contrib/ci/scripts/run_quiet.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh
+
+# Test examples
+ADD \
+  /contrib/ci/scripts/test_z3_examples_cmake.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh
+
+# Run unit tests
+ADD \
+  /contrib/ci/scripts/test_z3_unit_tests_cmake.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+
+# Run system tests
+ADD \
+  /contrib/ci/scripts/test_z3_system_tests.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh
+
+# Test install
+ADD \
+  /contrib/ci/scripts/test_z3_install_cmake.sh \
+  ${Z3_SRC_DIR}/contrib/ci/scripts/
+RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@ -0,0 +1,113 @@
+# Continous integration scripts
+
+## TravisCI
+
+For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/)
+
+TravisCI consumes the `.travis.yml` file in the root of the repository
+to tell it how to build and test Z3.
+
+However the logic for building and test Z3 is kept out of this file
+and instead in a set of scripts in `scripts/`. This avoids
+coupling the build to TravisCI tightly so we can migrate to another
+service if required in the future.
+
+The scripts rely on a set of environment variables to control the configuration
+of the build. The `.travis.yml` declares a list of configuration with each
+configuration setting different environment variables.
+
+Note that the build scripts currently only support Z3 built with CMake. Support
+for building Z3 using the older Python/Makefile build system might be added in
+the future.
+
+### Configuration variables
+
+* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`)
+* `BUILD_DOCS` - Build API documentation (`0` or `1`)
+* `C_COMPILER` - Path to C Compiler
+* `CXX_COMPILER` - Path to C++ Compiler
+* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`)
+* `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_SYSTEM_TESTS` - Run system tests (`0` or `1`)
+* `RUN_UNIT_TESTS` - Run unit tests (`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`)
+* `USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`)
+* `USE_LTO` - Link binaries using link time optimization (`0` or `1`)
+* `USE_OPENMP` - Use OpenMP (`0` or `1`)
+* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`)
+* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`)
+* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
+* `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`)
+* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used.
+
+### Linux
+
+For Linux we use Docker to perform the build so that it easily reproducible
+on a local machine and so that we can avoid depending on TravisCI's environment
+and instead use a Linux distribution of our choice.
+
+The `scripts/travis_ci_linux_entry_point.sh` script
+
+1. Creates a base image containing all the dependencies needed to build and test Z3
+2. Builds and tests Z3 using the base image propagating configuration environment
+   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`.
+
+#### Linux specific configuration variables
+
+* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`).
+
+#### 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.
+
+For example lets say we wanted to reproduce the build below.
+
+```yaml
+
+  - 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
+```
+
+This can be done by running the command
+
+```bash
+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 scripts/travis_ci_linux_entry_point.sh
+```
+
+The `docker build` command which we use internally supports caching. What this
+means in practice is that re-running the above command will re-use successfully
+completed stages of the build provided they haven't changed. This requires that
+the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating
+the cache when unrelated files sent to the build context change.
+
+#### TravisCI docker image cache
+
+To improve build times the Z3 base docker images are cached using
+[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching).
+If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`)
+then the directory pointed to by the environment variable is used as a cache
+for Docker images.
+
+The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`.
+The build time improvements are rather modest (~ 2 minutes) and the cache is
+rather large due to TravisCI giving each configuration its own cache. So this
+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.
+
+An [organization](https://hub.docker.com/u/z3prover/) has been created on
+DockerHub for this.
+
+### macOS
+
+Not yet implemented.
--- a/contrib/ci/maintainers.txt
+++ b/contrib/ci/maintainers.txt
@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)
--- a/contrib/ci/scripts/build_z3_cmake.sh
+++ b/contrib/ci/scripts/build_z3_cmake.sh
@ -0,0 +1,128 @@
+#!/bin/bash
+# This script builds Z3
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+set -o pipefail
+
+: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
+: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
+: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
+: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
+: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"}
+: ${USE_OPENMP?"USE_OPENMP must be specified"}
+: ${USE_LIBGMP?"USE_LIBGMP must be specified"}
+: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
+: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
+: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
+: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
+: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
+: ${USE_LTO?"USE_LTO must be specified"}
+: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX"}
+
+ADDITIONAL_Z3_OPTS=()
+
+# Static or dynamic libz3
+if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=OFF')
+else
+  ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=ON')
+fi
+
+# Use OpenMP?
+if [ "X${USE_OPENMP}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=ON')
+else
+  ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=OFF')
+fi
+
+# Use LibGMP?
+if [ "X${USE_LIBGMP}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=ON')
+else
+  ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=OFF')
+fi
+
+# Use link time optimziation?
+if [ "X${USE_LTO}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=ON')
+else
+  ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=OFF')
+fi
+
+# Build API docs?
+if [ "X${BUILD_DOCS}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_DOCUMENTATION=ON' \
+    '-DALWAYS_BUILD_DOCS=OFF' \
+  )
+else
+  ADDITIONAL_Z3_OPTS+=('-DBUILD_DOCUMENTATION=OFF')
+fi
+
+# Python bindings?
+if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_PYTHON_BINDINGS=ON' \
+    '-DINSTALL_PYTHON_BINDINGS=ON' \
+  )
+else
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_PYTHON_BINDINGS=OFF' \
+    '-DINSTALL_PYTHON_BINDINGS=OFF' \
+  )
+fi
+
+# .NET bindings?
+if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_DOTNET_BINDINGS=ON' \
+    '-DINSTALL_DOTNET_BINDINGS=ON' \
+  )
+else
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_DOTNET_BINDINGS=OFF' \
+    '-DINSTALL_DOTNET_BINDINGS=OFF' \
+  )
+fi
+
+# Java bindings?
+if [ "X${JAVA_BINDINGS}" = "X1" ]; then
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_JAVA_BINDINGS=ON' \
+    '-DINSTALL_JAVA_BINDINGS=ON' \
+  )
+else
+  ADDITIONAL_Z3_OPTS+=( \
+    '-DBUILD_JAVA_BINDINGS=OFF' \
+    '-DINSTALL_JAVA_BINDINGS=OFF' \
+  )
+fi
+
+# Set compiler flags
+source ${SCRIPT_DIR}/set_compiler_flags.sh
+
+# Sanity check
+if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then
+  echo "Z3_SRC_DIR is invalid"
+  exit 1
+fi
+
+# Make build tree
+mkdir -p "${Z3_BUILD_DIR}"
+cd "${Z3_BUILD_DIR}"
+
+# Configure
+cmake \
+  -G "${Z3_CMAKE_GENERATOR}" \
+  -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \
+  -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
+  -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \
+  "${ADDITIONAL_Z3_OPTS[@]}" \
+  "${Z3_SRC_DIR}"
+
+# Build
+source ${SCRIPT_DIR}/set_generator_args.sh
+cmake --build $(pwd) "${GENERATOR_ARGS[@]}"
--- a/contrib/ci/scripts/run_quiet.sh
+++ b/contrib/ci/scripts/run_quiet.sh
@ -0,0 +1,41 @@
+# Simple wrapper function that runs a command suppressing
+# it's output. However it's output will be shown in the
+# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command
+# fails.
+#
+# The use case for this trying to avoid large logs on TravisCI
+function run_quiet() {
+  if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then
+    "${@}"
+  else
+    OLD_SETTINGS="$-"
+    set +x
+    set +e
+    TMP_DIR="${TMP_DIR:-/tmp/}"
+    STDOUT="${TMP_DIR}/$$.stdout"
+    STDERR="${TMP_DIR}/$$.stderr"
+    "${@}" > "${STDOUT}" 2> "${STDERR}"
+    EXIT_STATUS="$?"
+    if [ "${EXIT_STATUS}" -ne 0 ]; then
+      echo "Command \"$@\" failed"
+      echo "EXIT CODE: ${EXIT_STATUS}"
+      echo "STDOUT"
+      echo ""
+      echo "\`\`\`"
+      cat ${STDOUT}
+      echo "\`\`\`"
+      echo ""
+      echo "STDERR"
+      echo ""
+      echo "\`\`\`"
+      cat ${STDERR}
+      echo "\`\`\`"
+      echo ""
+    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
+    return ${EXIT_STATUS}
+  fi
+}
--- a/contrib/ci/scripts/set_compiler_flags.sh
+++ b/contrib/ci/scripts/set_compiler_flags.sh
@ -0,0 +1,46 @@
+# This script should is intended to be included by other
+# scripts and should not be executed directly
+
+: ${TARGET_ARCH?"TARGET_ARCH must be specified"}
+: ${ASAN_BUILD?"ASAN_BUILD must be specified"}
+: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"}
+: ${CC?"CC must be specified"}
+: ${CXX?"CXX must be specified"}
+
+case ${TARGET_ARCH} in
+  x86_64)
+    CXXFLAGS="${CXXFLAGS} -m64"
+    CFLAGS="${CFLAGS} -m64"
+    ;;
+  i686)
+    CXXFLAGS="${CXXFLAGS} -m32"
+    CFLAGS="${CFLAGS} -m32"
+    ;;
+  *)
+    echo "Unknown arch \"${TARGET_ARCH}\""
+    exit 1
+esac
+
+if [ "X${ASAN_BUILD}" = "X1" ]; then
+  CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer"
+  CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"
+fi
+
+if [ "X${UBSAN_BUILD}" = "X1" ]; then
+  CXXFLAGS="${CXXFLAGS} -fsanitize=undefined"
+  CFLAGS="${CFLAGS} -fsanitize=undefined"
+fi
+
+# Report flags
+echo "CXXFLAGS: ${CXXFLAGS}"
+echo "CFLAGS: ${CFLAGS}"
+
+# Report compiler
+echo "CC: ${CC}"
+${CC} --version
+echo "CXX: ${CXX}"
+${CXX} --version
+
+# Export the values
+export CFLAGS
+export CXXFLAGS
--- a/contrib/ci/scripts/set_generator_args.sh
+++ b/contrib/ci/scripts/set_generator_args.sh
@ -0,0 +1,20 @@
+# This script should is intended to be included by other
+# scripts and should not be executed directly
+
+: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
+: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"}
+
+GENERATOR_ARGS=('--')
+if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then
+  GENERATOR_ARGS+=("-j$(nproc)")
+  if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
+    GENERATOR_ARGS+=("VERBOSE=1")
+  fi
+elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then
+  if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then
+    GENERATOR_ARGS+=("-v")
+  fi
+else
+  echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\""
+  exit 1
+fi
--- a/contrib/ci/scripts/test_z3_docs.sh
+++ b/contrib/ci/scripts/test_z3_docs.sh
@ -0,0 +1,24 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+. ${SCRIPT_DIR}/run_quiet.sh
+
+set -x
+set -e
+set -o pipefail
+
+: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
+: ${BUILD_DOCS?"BUILD_DOCS must be specified"}
+
+# Set CMake generator args
+source ${SCRIPT_DIR}/set_generator_args.sh
+
+cd "${Z3_BUILD_DIR}"
+
+# Generate documentation
+if [ "X${BUILD_DOCS}" = "X1" ]; then
+  # TODO: Make quiet once we've fixed the build
+  run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}"
+fi
+
+# TODO: Test or perhaps deploy the built docs?
--- a/contrib/ci/scripts/test_z3_examples_cmake.sh
+++ b/contrib/ci/scripts/test_z3_examples_cmake.sh
@ -0,0 +1,87 @@
+#!/bin/bash
+
+# This script tests Z3
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+. ${SCRIPT_DIR}/run_quiet.sh
+
+set -x
+set -e
+set -o pipefail
+: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"}
+: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
+: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"}
+: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"}
+: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
+: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
+
+# Set compiler flags
+source ${SCRIPT_DIR}/set_compiler_flags.sh
+
+# Set CMake generator args
+source ${SCRIPT_DIR}/set_generator_args.sh
+
+cd "${Z3_BUILD_DIR}"
+
+# Build and run C example
+cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}"
+run_quiet examples/c_example_build_dir/c_example
+
+# Build and run C++ example
+cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}"
+run_quiet examples/cpp_example_build_dir/cpp_example
+
+# Build and run tptp5 example
+cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}"
+# FIXME: Do something more useful with example
+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
+
+
+if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
+  # Run python examples
+  # `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
+  # 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
+fi
+
+if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
+  # Build .NET example
+  # 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
+fi
+
+if [ "X${JAVA_BINDINGS}" = "X1" ]; then
+  # Build Java example
+  # FIXME: Move compilation step into CMake target
+  mkdir -p examples/java
+  cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/
+  javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar
+  # Run Java example
+  if [ "$(uname)" = "Darwin" ]; then
+    # macOS
+    export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH}
+  else
+    # Assume Linux for now
+    export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH}
+  fi
+  run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample
+fi
+
--- a/contrib/ci/scripts/test_z3_install_cmake.sh
+++ b/contrib/ci/scripts/test_z3_install_cmake.sh
@ -0,0 +1,24 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+set -o pipefail
+
+: ${TEST_INSTALL?"TEST_INSTALL must be specified"}
+: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
+
+if [ "X${TEST_INSTALL}" != "X1" ]; then
+  echo "Skipping install"
+  exit 0
+fi
+
+# Set CMake generator args
+source ${SCRIPT_DIR}/set_generator_args.sh
+
+cd "${Z3_BUILD_DIR}"
+
+sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}"
+
+# TODO: Test the installed version in some way
--- a/contrib/ci/scripts/test_z3_system_tests.sh
+++ b/contrib/ci/scripts/test_z3_system_tests.sh
@ -0,0 +1,54 @@
+#!/bin/bash
+
+set -x
+set -e
+set -o pipefail
+
+: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
+: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"}
+: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"}
+: ${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"}
+
+if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then
+  echo "Skipping system tests"
+  exit 0
+fi
+
+Z3_EXE="${Z3_BUILD_DIR}/z3"
+Z3_LIB_DIR="${Z3_BUILD_DIR}"
+
+# Set value if not already defined externally
+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}"
+git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}"
+cd "${Z3_SYSTEM_TEST_DIR}"
+
+if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
+  # If a particular revision is requested then check it out.
+  # This is useful for reproducible builds
+  git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}"
+fi
+
+###############################################################################
+# Run system tests
+###############################################################################
+
+# SMTLIBv2 tests
+${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2
+
+${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra
+
+if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then
+  ${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug
+fi
+
+if [ "X${PYTHON_BINDINGS}" = "X1" ]; then
+  # Run python binding tests
+  ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/
+fi
+
+# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
@ -0,0 +1,24 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+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[@]}"
+./test-z3
--- a/contrib/ci/scripts/travis_ci_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_entry_point.sh
@ -0,0 +1,18 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+set -o pipefail
+
+: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"}
+
+if [ "${TRAVIS_OS_NAME}" = "osx" ]; then
+  ${SCRIPT_DIR}/travis_ci_osx_entry_point.sh
+elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then
+  ${SCRIPT_DIR}/travis_ci_linux_entry_point.sh
+else
+  echo "Unsupported OS \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@ -0,0 +1,208 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+set -o pipefail
+
+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
+
+BUILD_OPTS=()
+# Override options if they have been provided.
+# Otherwise the defaults in the Docker file will be used
+if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
+fi
+
+if [ -n "${USE_OPENMP}" ]; then
+  BUILD_OPTS+=("--build-arg" "USE_OPENMP=${USE_OPENMP}")
+fi
+
+if [ -n "${USE_LIBGMP}" ]; then
+  BUILD_OPTS+=("--build-arg" "USE_LIBGMP=${USE_LIBGMP}")
+fi
+
+if [ -n "${BUILD_DOCS}" ]; then
+  BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}")
+fi
+
+if [ -n "${PYTHON_EXECUTABLE}" ]; then
+  BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}")
+fi
+
+if [ -n "${PYTHON_BINDINGS}" ]; then
+  BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}")
+fi
+
+if [ -n "${DOTNET_BINDINGS}" ]; then
+  BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}")
+fi
+
+if [ -n "${JAVA_BINDINGS}" ]; then
+  BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}")
+fi
+
+if [ -n "${USE_LTO}" ]; then
+  BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}")
+fi
+
+if [ -n "${Z3_INSTALL_PREFIX}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}")
+fi
+
+# TravisCI reserves CC for itself so use a different name
+if [ -n "${C_COMPILER}" ]; then
+  BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}")
+fi
+
+# TravisCI reserves CXX for itself so use a different name
+if [ -n "${CXX_COMPILER}" ]; then
+  BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}")
+fi
+
+if [ -n "${TARGET_ARCH}" ]; then
+  BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}")
+fi
+
+if [ -n "${ASAN_BUILD}" ]; then
+  BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}")
+fi
+
+if [ -n "${UBSAN_BUILD}" ]; then
+  BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}")
+fi
+
+if [ -n "${TEST_INSTALL}" ]; then
+  BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}")
+fi
+
+if [ -n "${RUN_SYSTEM_TESTS}" ]; then
+  BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}")
+fi
+
+if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then
+  BUILD_OPTS+=( \
+    "--build-arg" \
+    "Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \
+  )
+fi
+
+if [ -n "${RUN_UNIT_TESTS}" ]; then
+  BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}")
+fi
+
+if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then
+  BUILD_OPTS+=( \
+    "--build-arg" \
+    "Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \
+  )
+fi
+
+if [ -n "${Z3_STATIC_BUILD}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}")
+fi
+
+if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then
+  BUILD_OPTS+=( \
+    "--build-arg" \
+    "NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \
+  )
+fi
+
+case ${LINUX_BASE} in
+  ubuntu_14.04)
+    BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile"
+    BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:14.04"
+    ;;
+  ubuntu_16.04)
+    BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_16.04.Dockerfile"
+    BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:16.04"
+    ;;
+  ubuntu32_16.04)
+    BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu32_16.04.Dockerfile"
+    BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu32:16.04"
+    ;;
+  *)
+    echo "Unknown Linux base ${LINUX_BASE}"
+    exit 1
+    ;;
+esac
+
+# Initially assume that we need to build the base Docker image
+MUST_BUILD=1
+
+# Travis CI persistent cache.
+#
+# This inspired by http://rundef.com/fast-travis-ci-docker-build .
+# The idea is to cache the built image for subsequent builds to
+# reduce build time.
+if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
+  CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum"
+  CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz"
+  if [ -f "${CACHED_DOCKER_IMAGE}" ]; then
+    # There's a cached image to use. Check the checksums of the Dockerfile
+    # match. If they don't that implies we need to build a fresh image.
+    if [ -f "${CHECKSUM_FILE}" ]; then
+      CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }')
+      CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}")
+      if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then
+        # Load the cached image
+        MUST_BUILD=0
+        gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load
+      fi
+    fi
+  fi
+fi
+
+if [ "${MUST_BUILD}" -eq 1 ]; then
+  # The base image contains all the dependencies we want to build
+  # Z3.
+  docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}"
+
+  if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then
+    # Write image and checksum to cache
+    docker save "${BASE_DOCKER_IMAGE_NAME}" | \
+      gzip > "${CACHED_DOCKER_IMAGE}"
+    sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \
+      "${CHECKSUM_FILE}"
+  fi
+fi
+
+
+DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/')
+DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/')
+DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile"
+
+if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then
+  # Workaround limitation in older Docker versions where the FROM
+  # command cannot be parameterized with an ARG.
+  sed \
+    -e '/^ARG DOCKER_IMAGE_BASE/d' \
+    -e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \
+    "${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched"
+  DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched"
+else
+  # This feature landed in Docker 17.05
+  # See https://github.com/moby/moby/pull/31352
+  BUILD_OPTS+=( \
+    "--build-arg" \
+    "DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \
+  )
+fi
+
+# Now build Z3 and test it using the created base image
+docker build \
+  -f "${DOCKER_BUILD_FILE}" \
+  "${BUILD_OPTS[@]}" \
+  .
--- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
@ -0,0 +1,10 @@
+#!/bin/bash
+
+SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )"
+
+set -x
+set -e
+set -o pipefail
+
+echo "Not implemented"
+exit 1