Extensive updates to the build script for dependencies and docker

Building/managing dependencies of KLEE are not easy. This script should change
this.

Features:
* script install different versions in their specific directories
  This allows:
  - to have different versions in parallel installed: llvm, solvers
  - to have different optimization levels installed (Debug, no-debug,
    assertions, optimized)
  - to have different versions of instrumentation enabled (address, memory,
    leakage, undefined behavior)
* the script is kept distribution agnostic: assuming basic packages are
  installed (a compiler), use `scripts/build/ubuntu-dependencies.sh` to install
  ubuntu specific ones
* the script does not install any file into system directories (sudo is not
  required) files are only installed into a user specified BASE directory

The same scripts are used for either local setup (`scripts/build/local_install.sh`)
or create a docker image based of your current source folder (`scripts/build/build_docker.sh`)
Change the defaults permanently by modifying (`scripts/build/common-defaults.sh`)
or change them on the fly by providing them as environment variables on the
command line.

The same scripts are also used for TravisCI, so we test what we are using.

33 files changed, 1229 insertions, 496 deletions

diff --git a/.dockerignore b/.dockerignore
index 8feca832..11d13733 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -1,4 +1,4 @@
-.git
+#.git - Don't delete git, we need that to generate the correct version number
 autom4te.cache
 **/.*.swp
 Dockerfile
diff --git a/.travis.yml b/.travis.yml
index 5a8a6e45..c8de1292 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,8 @@
 sudo: required
 dist: trusty
 language: cpp
+services:
+    - docker
 compiler:
     # FIXME: For now, building with Clang is disabled because the STP built with
     # it hits an assertion failure during some tests. We should sort this out
@@ -32,25 +34,25 @@ env:
     #   COVERAGE: {0, 1}
     #   USE_TCMALLOC: {0, 1}
 
-    # COVERAGE when set indicates that coverage data should be uploaded to the service, only ONE job should have COVERAGE set
+    # COVERAGE when set indicates that coverage data should be uploaded to the service
 
     matrix:
 
     # TODO: Add Doxygen build
 
     # Check newer LLVMs
-    - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-
-    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
-    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.7 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.6 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.5 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=STP KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1 REQUIRES_RTTI=1
 
     # ASan build. Do unoptimized build otherwise the optimizer might remove problematic code
-    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 ASAN_BUILD=1
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=address
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0 USE_TCMALLOC=0 SANITIZER_BUILD=undefined
 
     # Test just using Z3
-    - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=Z3 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
 
     # Test we can build against STP master
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -59,7 +61,7 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_0_9_29 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
 
     # Test metaSMT support
-    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_VERSION=v4.rc1 METASMT_DEFAULT=BTOR KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 REQUIRES_RTTI=1
 
     # Check at least one build with Asserts disabled.
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=1 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -71,78 +73,38 @@ env:
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
 
     # Coverage build
-    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
+    - LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=1 USE_TCMALLOC=0
     global:
     - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
     - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
     - secure: DQAEQWJblXvIztN/sgH63OtFncI+Qju6wRy1zIV/iLf5KbAmLs1h3itU7EsE/+3+LgV1MVQ5QNJDBUj17A6VHRKNaQ5qnIllTAcC3o0nPDohQkQoCgDG8HZ+M4wtVfr7q2K6byEPB2UbSH+mEjSMTihJufgBBVfKyyozAfYycjg=
+    - KLEE_TRAVIS_BUILD: 1
+    - REPOSITORY: klee
 
 matrix:
   include:
     - os: osx
       osx_image: xcode8.3
-      env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0
-
-addons:
-  apt:
-    sources:
-    - sourceline: 'ppa:ubuntu-toolchain-r/test'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.4 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.5 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.6 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://apt.llvm.org/trusty/ llvm-toolchain-trusty-3.7 main'
-      key_url: 'https://apt.llvm.org/llvm-snapshot.gpg.key'
-    - sourceline: 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /'
-      key_url: 'http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key'
-    packages:
-    - gcc-4.8
-    - g++-4.8
-    - libboost-program-options-dev
-    - libcap-dev
-    - libedit-dev
-    - libselinux1-dev
-    - cmake
-    - lcov
+      env: LLVM_VERSION=3.4 SOLVERS=STP:Z3 STP_VERSION=2.1.2 Z3_VERSION=4.4.1 KLEE_UCLIBC=0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=0
 
 cache:
   ccache: true
   apt: true
   directories:
     - $HOME/Library/Caches/Homebrew
+
 before_install:
     ###########################################################################
     # Set up the locations to get various packages from
     # We assume the Travis image uses Ubuntu 14.04 LTS
     ###########################################################################
     # Update package information
-    - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then sudo apt-get update; fi
-    - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then brew update && brew tap klee/klee && brew install ccache && export PATH="/usr/local/opt/ccache/libexec:$PATH" ; fi
-    ###########################################################################
-    # Set up out of source build directory
-    ###########################################################################
     - export KLEE_SRC=`pwd`
+    - export KLEE_SRC_TRAVIS=`pwd`
     - cd ../
-    - mkdir build
-    - cd build/
-    - export BUILD_DIR=`pwd`
-    ###########################################################################
-    # Install stuff
-    ###########################################################################
-    # Install LLVM and the LLVM bitcode compiler we require to build KLEE
-    - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
-    - ${KLEE_SRC}/.travis/install-tcmalloc.sh
-    # Install lit (llvm-lit is not available)
-    - sudo pip2 install lit
-    # Get SMT solvers
-    - ${KLEE_SRC}/.travis/solvers.sh
-    # Get needed utlities/libraries for testing KLEE
-    - mkdir test-utils/
-    - cd test-utils/
-    - ${KLEE_SRC}/.travis/testing-utils.sh
-    - cd ../
+    - export BASE=`pwd`
+    - ${KLEE_SRC_TRAVIS}/scripts/build/build-travis.sh
 script:
     # Build KLEE and run tests
-    - ${KLEE_SRC}/.travis/klee.sh
+    - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then export PATH="/usr/local/opt/ccache/libexec:$PATH"; ${KLEE_SRC_TRAVIS}/scripts/build/klee.sh; fi
+    - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then ${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh; fi
diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh
deleted file mode 100755
index bd34d843..00000000
--- a/.travis/install-llvm-and-runtime-compiler.sh
+++ /dev/null
@@ -1,27 +0,0 @@
-#!/bin/bash -x
-set -ev
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev
-
-  sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION}
-  sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_VERSION} 20
-  sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_VERSION} 20
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  # We use our own local cache if possible
-  set +e
-  brew install $HOME/Library/Caches/Homebrew/llvm\@${LLVM_VERSION}*.bottle.tar.gz
-  RES=$?
-  set -ev
-  if [ ${RES} -ne 0 ]; then
-    # This might build the llvm package use a time out to avoid dumping log information
-    brew install -v --build-bottle "llvm@${LLVM_VERSION}"
-    # Now bottle the brew
-    brew bottle llvm\@${LLVM_VERSION}
-    # Not make sure it's cached
-    cp llvm\@${LLVM_VERSION}*.bottle.tar.gz $HOME/Library/Caches/Homebrew/
-  fi
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh
deleted file mode 100755
index 0bc26616..00000000
--- a/.travis/install-tcmalloc.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/bash -x
-set -ev
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
-    # Get tcmalloc release
-    wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz
-    tar xfz gperftools-2.4.tar.gz
-    cd gperftools-2.4
-    ./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc  --enable-minimal --prefix=/usr
-    make
-    sudo make install
-  fi
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
-    echo "Error: Requested to install TCMalloc on macOS, which is not supported"
-    exit 1
-  fi
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
deleted file mode 100755
index 5d5b669e..00000000
--- a/.travis/metaSMT.sh
+++ /dev/null
@@ -1,49 +0,0 @@
-#!/bin/bash -x
-
-set -e
-
-: ${METASMT_VERSION?"METASMT_VERSION not specified"}
-
-# Get Z3, libgmp, gperf (required by yices2)
-sudo apt-get -y install libz3 libz3-dev libgmp-dev gperf
-
-# Get Boost
-if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then
-  # Taken from boost/hana/.travis.yml
-  BOOST_URL="http://sourceforge.net/projects/boost/files/boost/${METASMT_BOOST_VERSION}/boost_${METASMT_BOOST_VERSION//\./_}.tar.gz"
-  BOOST_DIR=`pwd`/boost-${METASMT_BOOST_VERSION}
-  mkdir -p ${BOOST_DIR}
-  wget --quiet -O - ${BOOST_URL} | tar --strip-components=1 -xz -C ${BOOST_DIR}
-  sudo ln -s ${BOOST_DIR}/boost /usr/include/boost
-else
-  sudo apt-get -y install libboost1.55-dev
-fi
-
-# Get CVC4
-wget http://www.informatik.uni-bremen.de/agra/systemc-verification/media/snapshots/cvc4-594301e.tar.gz
-tar -xf cvc4-594301e.tar.gz
-sudo mv cvc4 /usr
-
-# Clone
-git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git
-cd metaSMT
-git submodule update --init
-
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
-  echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented"
-  exit 1
-fi
-
-# Bootstrap
-export BOOST_ROOT=/usr
-sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
-./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 -DZ3_DIR=/usr -DCVC4_DIR=/usr/cvc4
-sudo cp deps/boolector-2.2.0/lib/* /usr/lib/              #
-sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ #
-sudo cp deps/minisat-git/lib/* /usr/lib/                  # hack
-sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/          #
-sudo cp deps/yices-2.5.1/lib/* /usr/lib/                  #
-
-# Build
-make -C build install
diff --git a/.travis/sanitizer_flags.sh b/.travis/sanitizer_flags.sh
deleted file mode 100644
index 4d3dce2c..00000000
--- a/.travis/sanitizer_flags.sh
+++ /dev/null
@@ -1,39 +0,0 @@
-# This file is meant to be included by shell scripts
-# that need to do a sanitized build.
-
-# Users of this script can use this variable
-# to detect if a Sanitized build was enabled.
-IS_SANITIZED_BUILD=0
-
-# AddressSanitizer
-if [ "X${ASAN_BUILD}" == "X1" ]; then
-  echo "Using ASan"
-  ASAN_CXX_FLAGS="-fsanitize=address -fno-omit-frame-pointer"
-  ASAN_C_FLAGS="${ASAN_CXX_FLAGS}"
-  ASAN_LD_FLAGS="${ASAN_CXX_FLAGS}"
-  IS_SANITIZED_BUILD=1
-else
-  echo "Not using ASan"
-  ASAN_CXX_FLAGS=""
-  ASAN_C_FLAGS=""
-  ASAN_LD_FLAGS=""
-fi
-
-# Undefined Behaviour Sanitizer
-if [ "X${UBSAN_BUILD}" == "X1" ]; then
-  echo "Using UBSan"
-  UBSAN_CXX_FLAGS="-fsanitize=undefined"
-  UBSAN_C_FLAGS="${UBSAN_CXX_FLAGS}"
-  UBSAN_LD_FLAGS="${UBSAN_CXX_FLAGS}"
-  IS_SANITIZED_BUILD=1
-else
-  echo "Not using UBSan"
-  UBSAN_CXX_FLAGS=""
-  UBSAN_C_FLAGS=""
-  UBSAN_LD_FLAGS=""
-fi
-
-# Set variables to be used by clients.
-SANITIZER_CXX_FLAGS="${ASAN_CXX_FLAGS} ${UBSAN_CXX_FLAGS}"
-SANITIZER_C_FLAGS="${ASAN_C_FLAGS} ${UBSAN_C_FLAGS}"
-SANITIZER_LD_FLAGS="${ASAN_LD_FLAGS} ${UBSAN_LD_FLAGS}"
diff --git a/.travis/stp.sh b/.travis/stp.sh
deleted file mode 100755
index e8647839..00000000
--- a/.travis/stp.sh
+++ /dev/null
@@ -1,72 +0,0 @@
-#!/bin/bash -x
-
-# TODO: For OSX we can prepare bottled formulas for STP and minisat
-
-# Make sure we exit if there is a failure
-set -e
-
-STP_LOG="$(pwd)/stp-build.log"
-
-if [ "x${STP_VERSION}" != "x" ]; then
-  # Get Sanitizer flags
-  source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-
-  # Build minisat
-  git clone https://github.com/stp/minisat
-  cd minisat
-  mkdir build
-  cd build
-  MINISAT_DIR=`pwd`
-  if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-    CFLAGS="${SANITIZER_C_FLAGS}" \
-    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-    cmake -DCMAKE_INSTALL_PREFIX=/usr ..
-  elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-    CFLAGS="${SANITIZER_C_FLAGS}" \
-    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-    cmake -DCMAKE_INSTALL_PREFIX=/usr/local ..
-  else
-    echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-    exit 1
-  fi
-  make
-  sudo make install
-  cd ../../
-
-  # Determine STP build flags
-  if [ "X${STP_VERSION}" = "Xmaster" ]; then
-    # 5e9ca6339a2b3b000aa7a90c18601fdcf1212fe1 Silently BUILD_SHARED_LIBS removed. STATICCOMPILE does something similar
-    STP_CMAKE_FLAGS=( \
-      "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \
-      "-DSTATICCOMPILE:BOOL=ON" \
-    )
-  else
-    STP_CMAKE_FLAGS=( \
-      "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \
-      "-DBUILD_SHARED_LIBS:BOOL=OFF" \
-    )
-  fi
-
-  # Build STP
-  git clone --depth 1 -b "${STP_VERSION}" git://github.com/stp/stp.git src
-  mkdir build
-  cd build
-  # Disabling building of shared libs is a workaround.
-  # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8
-  CFLAGS="${SANITIZER_C_FLAGS}" \
-  CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
-  cmake "${STP_CMAKE_FLAGS[@]}" ../src
-
-  set +e # Do not exit if build fails because we need to display the log
-  make >> "${STP_LOG}" 2>&1
-else
-  echo "No STP_VERSION given or empty"
-  exit 1
-fi
-
-# Only show build output if something went wrong to keep log output short
-if [ $? -ne 0 ]; then
-  echo "Build error"
-  cat "${STP_LOG}"
-  exit 1
-fi
diff --git a/.travis/testing-utils.sh b/.travis/testing-utils.sh
deleted file mode 100755
index eefccdd2..00000000
--- a/.travis/testing-utils.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash -x
-# Make sure we exit if there is a failure
-set -e
-
-# The New CMake build system just needs the GTest sources regardless
-# of LLVM version.
-wget https://github.com/google/googletest/archive/release-1.7.0.zip
-unzip release-1.7.0.zip
-exit 0
diff --git a/.travis/z3.sh b/.travis/z3.sh
deleted file mode 100755
index 315d028c..00000000
--- a/.travis/z3.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash -x
-
-# Make sure we exit if there is a failure
-set -e
-
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
-  echo "Error: Requested Sanitized build but Z3 being used is not sanitized"
-  exit 1
-fi
-
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  # Should we install libz3-dbg too?
-  sudo apt-get -y install libz3 libz3-dev
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  set +e
-  brew install python@2
-  if [[ "X$?" != "X0" ]]; then
-     brew link --overwrite python@2
-  fi
-  set -e
-  brew install z3
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/Dockerfile b/Dockerfile
deleted file mode 100644
index 7d23dc7f..00000000
--- a/Dockerfile
+++ /dev/null
@@ -1,101 +0,0 @@
-FROM ubuntu:14.04
-MAINTAINER Dan Liew <daniel.liew@imperial.ac.uk>
-
-# FIXME: Docker doesn't currently offer a way to
-# squash the layers from within a Dockerfile so
-# the resulting image is unnecessarily large!
-
-ENV LLVM_VERSION=3.4 \
-    SOLVERS=STP:Z3 \
-    STP_VERSION=2.1.2 \
-    DISABLE_ASSERTIONS=0 \
-    ENABLE_OPTIMIZED=1 \
-    KLEE_UCLIBC=klee_uclibc_v1.0.0 \
-    KLEE_SRC=/home/klee/klee_src \
-    COVERAGE=0 \
-    BUILD_DIR=/home/klee/klee_build \
-    ASAN_BUILD=0 \
-    UBSAN_BUILD=0 \
-    TRAVIS_OS_NAME=linux
-
-RUN apt-get update && \
-    apt-get -y --no-install-recommends install \
-        clang-${LLVM_VERSION} \
-        llvm-${LLVM_VERSION} \
-        llvm-${LLVM_VERSION}-dev \
-        llvm-${LLVM_VERSION}-runtime \
-        llvm \
-        libcap-dev \
-        git \
-        subversion \
-        cmake \
-        make \
-        libboost-program-options-dev \
-        python3 \
-        python3-dev \
-        python3-pip \
-        perl \
-        flex \
-        bison \
-        libncurses-dev \
-        zlib1g-dev \
-        patch \
-        wget \
-        unzip \
-        binutils && \
-    pip3 install -U lit tabulate wllvm && \
-    update-alternatives --install /usr/bin/python python /usr/bin/python3 50 && \
-    ( wget -O - http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_14.04/Release.key | apt-key add - ) && \
-    echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_14.04/ /' >> /etc/apt/sources.list.d/z3.list && \
-    apt-get update
-
-# Create ``klee`` user for container with password ``klee``.
-# and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
-RUN useradd -m klee && \
-    echo klee:klee | chpasswd && \
-    cp /etc/sudoers /etc/sudoers.bak && \
-    echo 'klee  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
-USER klee
-WORKDIR /home/klee
-
-# Copy across source files needed for build
-RUN mkdir ${KLEE_SRC}
-ADD / ${KLEE_SRC}
-
-# Set klee user to be owner
-RUN sudo chown --recursive klee: ${KLEE_SRC}
-
-# Create build directory
-RUN mkdir -p ${BUILD_DIR}
-
-# Build/Install SMT solvers (use TravisCI script)
-RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/solvers.sh
-
-# Install testing utils (use TravisCI script)
-RUN cd ${BUILD_DIR} && mkdir test-utils && cd test-utils && \
-    ${KLEE_SRC}/.travis/testing-utils.sh
-
-# FIXME: The current TravisCI script expects clang-${LLVM_VERSION} to exist
-RUN sudo ln -s /usr/bin/clang /usr/bin/clang-${LLVM_VERSION} && \
-    sudo ln -s /usr/bin/clang++ /usr/bin/clang++-${LLVM_VERSION}
-
-# Build KLEE (use TravisCI script)
-RUN cd ${BUILD_DIR} && ${KLEE_SRC}/.travis/klee.sh
-
-# Revoke password-less sudo and Set up sudo access for the ``klee`` user so it
-# requires a password
-USER root
-RUN mv /etc/sudoers.bak /etc/sudoers && \
-    echo 'klee  ALL=(root) ALL' >> /etc/sudoers
-USER klee
-
-# FIXME: Shouldn't we just invoke the `install` target? This will
-# duplicate some files but the Docker image is already pretty bloated
-# so this probably doesn't matter.
-# Add KLEE binary directory to PATH
-RUN echo 'export PATH=$PATH:'${BUILD_DIR}'/klee/bin' >> /home/klee/.bashrc
-
-# Link klee to /usr/bin so that it can be used by docker run
-USER root
-RUN for executable in ${BUILD_DIR}/klee/bin/* ; do ln -s ${executable} /usr/bin/`basename ${executable}`; done
-USER klee
diff --git a/scripts/build/Dockerfile_base b/scripts/build/Dockerfile_base
new file mode 100644
index 00000000..8daee330
--- /dev/null
+++ b/scripts/build/Dockerfile_base
@@ -0,0 +1,15 @@
+# Build dependencies for LLVM
+FROM ubuntu:16.04
+LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>"
+
+ENV DOCKER_BUILD=1
+
+# Define all variables that can be changed as argument to docker build
+ARG BASE=/tmp
+
+# Copy across all source files
+ADD /scripts/build/* scripts/build/
+
+# Install packages
+RUN scripts/build/dependencies-ubuntu.sh && rm -rf /var/lib/apt/lists/*
+WORKDIR $BASE
diff --git a/scripts/build/Dockerfile_klee b/scripts/build/Dockerfile_klee
new file mode 100644
index 00000000..79ad3838
--- /dev/null
+++ b/scripts/build/Dockerfile_klee
@@ -0,0 +1,58 @@
+# Build the final KLEE layer
+ARG REPOSITORY
+ARG LLVM_VERSION_SHORT
+ARG LLVM_SUFFIX
+ARG SOLVER_SUFFIX
+ARG DEPS_SUFFIX
+FROM ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX}
+LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>"
+
+# Define all variables that can be changed as argument to the docker build
+ARG BASE=/tmp
+ARG COVERAGE=0
+ARG DEPS_SUFFIX
+ARG DISABLE_ASSERTIONS
+ARG ENABLE_OPTIMIZED
+ARG ENABLE_DEBUG
+ARG KLEE_TRAVIS_BUILD
+ARG KLEE_UCLIBC
+ARG LLVM_VERSION
+ARG LLVM_SUFFIX
+ARG METASMT_BOOST_VERSION
+ARG METASMT_DEFAULT
+ARG METASMT_VERSION
+ARG REQUIRES_RTTI
+ARG SANITIZER_BUILD
+ARG SANITIZER_SUFFIX
+ARG SOLVER_SUFFIX
+ARG SOLVERS
+ARG STP_VERSION
+ARG TRAVIS_OS_NAME
+ARG USE_TCMALLOC
+ARG Z3_VERSION
+
+ENV DOCKER_BUILD=1
+
+# Copy across source files needed for build
+ADD / ${BASE}/klee_src
+
+# TODO Remove when STP is fixed
+RUN export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/ && export KLEE_SRC=${BASE}/klee_src && ${BASE}/klee_src/scripts/build/klee.sh && rm -rf ${BASE}/klee_src/.git
+
+# Create ``klee`` user for container with password ``klee``.
+# and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
+RUN useradd -m klee && \
+    echo klee:klee | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'klee  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+
+# Set klee user to be owner
+RUN chown --recursive klee: ${BASE}/klee_src
+
+USER klee
+WORKDIR /home/klee
+
+# Add KLEE binary directory to PATH
+RUN /bin/bash -c 'DIR="${BASE}/klee_src/scripts/build" source ${BASE}/klee_src/scripts/build/common-defaults.sh && ln -s ${BASE}/klee_build* ${BASE}/klee_build && echo "export PATH=\"$PATH:${LLVM_BIN}:${BASE}/klee_build/bin\"" >> /home/klee/.bashrc'
+# TODO Remove when STP is fixed
+RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=${BASE}/metaSMT/deps/stp-git-basic/lib/" >> /home/klee/.bashrc'
diff --git a/scripts/build/Dockerfile_klee_deps b/scripts/build/Dockerfile_klee_deps
new file mode 100644
index 00000000..582d324f
--- /dev/null
+++ b/scripts/build/Dockerfile_klee_deps
@@ -0,0 +1,33 @@
+# Build KLEE dependencies except LLVM and solvers
+ARG REPOSITORY
+ARG LLVM_VERSION_SHORT
+ARG LLVM_SUFFIX
+ARG SOLVER_SUFFIX
+FROM ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}
+LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>"
+
+# Define all variables that can be changed as argument to the docker build
+ARG BASE=/tmp
+ARG DISABLE_ASSERTIONS
+ARG ENABLE_OPTIMIZED
+ARG ENABLE_DEBUG
+ARG KEEP_BUILD
+ARG KEEP_SRC
+ARG KLEE_TRAVIS_BUILD
+ARG KLEE_UCLIBC
+ARG LLVM_VERSION
+ARG LLVM_SUFFIX
+ARG REQUIRES_RTTI
+ARG SANITIZER_BUILD
+ARG TRAVIS_OS_NAME
+ARG USE_TCMALLOC
+
+ENV DOCKER_BUILD=1
+
+# Copy across source files needed for build
+ADD /scripts/build/* scripts/build/
+
+# Build KLEE (use TravisCI script)
+RUN ${BASE}/scripts/build/testing-utils.sh
+RUN ${BASE}/scripts/build/tcmalloc.sh
+RUN ${BASE}/scripts/build/uclibc.sh
diff --git a/scripts/build/Dockerfile_llvm_build b/scripts/build/Dockerfile_llvm_build
new file mode 100644
index 00000000..548f0d8a
--- /dev/null
+++ b/scripts/build/Dockerfile_llvm_build
@@ -0,0 +1,27 @@
+# Build LLVM
+ARG LLVM_VERSION_SHORT
+ARG REPOSITORY
+FROM ${REPOSITORY}/base
+LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>"
+
+ENV DOCKER_BUILD=1
+
+# Define all variables that can be changed as argument to the docker build
+ARG BASE=/tmp
+ARG DISABLE_ASSERTIONS
+ARG ENABLE_OPTIMIZED
+ARG ENABLE_DEBUG
+ARG KEEP_BUILD
+ARG KEEP_SRC
+ARG KLEE_TRAVIS_BUILD
+ARG LLVM_VERSION
+ARG PACKAGED
+ARG REQUIRES_RTTI
+ARG SANITIZER_BUILD
+ARG TRAVIS_OS_NAME
+
+WORKDIR $BASE
+
+# Copy across source files needed for build
+ADD /scripts/build/* scripts/build/
+RUN ./scripts/build/llvm.sh
diff --git a/scripts/build/Dockerfile_solver_build b/scripts/build/Dockerfile_solver_build
new file mode 100644
index 00000000..ba2af62a
--- /dev/null
+++ b/scripts/build/Dockerfile_solver_build
@@ -0,0 +1,33 @@
+ARG REPOSITORY
+ARG LLVM_SUFFIX
+ARG LLVM_VERSION_SHORT
+FROM ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}
+LABEL maintainer="Martin Nowack <m.nowack@imperial.ac.uk>"
+
+ENV DOCKER_BUILD=1
+
+# Define all variables that can be changed as argument to docker build
+ARG BASE=/tmp
+ARG DISABLE_ASSERTIONS
+ARG ENABLE_OPTIMIZED
+ARG ENABLE_DEBUG
+ARG KEEP_BUILD
+ARG KEEP_SRC
+ARG KLEE_TRAVIS_BUILD
+ARG LLVM_VERSION
+ARG METASMT_BOOST_VERSION
+ARG METASMT_DEFAULT
+ARG METASMT_VERSION
+ARG REQUIRES_RTTI
+ARG SOLVERS
+ARG SANITIZER_BUILD
+ARG STP_VERSION
+ARG STORAGE_SPACE_OPTIMIZED=1
+ARG TRAVIS_OS_NAME
+ARG Z3_VERSION
+
+WORKDIR $BASE
+
+# Copy across source files needed for build
+ADD /scripts/build/* scripts/build/
+RUN scripts/build/solvers.sh
diff --git a/scripts/build/build-docker.sh b/scripts/build/build-docker.sh
new file mode 100755
index 00000000..a409fb0a
--- /dev/null
+++ b/scripts/build/build-docker.sh
@@ -0,0 +1,100 @@
+#!/bin/bash
+# Build a KLEE docker image. If needed, build all dependent layers as well.
+set -e
+
+# We are going to build docker containers
+export DOCKER_BUILD=1
+
+# All scripts are located relative to this one
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+KLEEDIR="${DIR}/../.."
+
+###############################################################################
+# Setup Docker variables needed to build layers layers
+###############################################################################
+
+add_arg_variable() {
+  name=$1
+  name_var=${!name}
+  if [[ (-z "$name_var") || ($name_var == "") ]] ; then
+    val=""
+  else
+    val="--build-arg ${name}=${name_var} "
+  fi
+  echo "$val"
+}
+
+DOCKER_OPTS=()
+for v in \
+  LLVM_VERSION \
+  LLVM_VERSION_SHORT \
+  ENABLE_OPTIMIZED \
+  DISABLE_ASSERTIONS \
+  ENABLE_DEBUG \
+  REQUIRES_RTTI \
+  LLVM_SUFFIX \
+  REPOSITORY \
+  SANITIZER_BUILD \
+  SANITIZER_SUFFIX \
+  PACKAGED \
+  KLEE_TRAVIS_BUILD \
+  TRAVIS_OS_NAME \
+  METASMT_VERSION \
+  METASMT_DEFAULT \
+  METASMT_BOOST_VERSION \
+  SOLVER_SUFFIX \
+  Z3_VERSION \
+  STP_VERSION \
+  KLEE_UCLIBC \
+  DEPS_SUFFIX \
+  USE_TCMALLOC \
+  COVERAGE \
+  KEEP_SRC \
+  KEEP_BUILD \
+  TCMALLOC_VERSION \
+  GTEST_VERSION \
+  SOLVERS \
+  ; do
+  DOCKER_OPTS+=($(add_arg_variable $v))
+done
+
+echo "DOCKER_OPTS: ${DOCKER_OPTS[@]}"
+docker_build_and_push() {
+  merge=$1
+  image=$2
+  script=$3
+  set +e
+  # Get or build layer
+  echo "$image"
+  if ! docker pull $image ;  then
+    set -e
+    # Update if needed
+    echo "BUILD IMAGE"
+    merge_arg=""
+  #  if [[ "${merge}x" == "1x" ]]; then
+  #    #merge_arg="--squash"
+  #  fi
+    docker build ${merge_arg} -f "${DIR}/$script" ${@:4} -t "$image" "${KLEEDIR}"
+    set +e
+    docker push "$image"
+  fi
+  return 0
+}
+
+###############################################################################
+# Build different layers
+###############################################################################
+
+# Check if the build of dependencies only has been requested
+if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" == "1x" ]]; then
+  echo "Build dependencies"
+  docker_build_and_push 1 ${REPOSITORY}/base Dockerfile_base "${DOCKER_OPTS[@]}"
+  docker_build_and_push 1 ${REPOSITORY}/llvm_built:${LLVM_VERSION_SHORT}${LLVM_SUFFIX} Dockerfile_llvm_build "${DOCKER_OPTS[@]}"
+  docker_build_and_push 1 ${REPOSITORY}/solver:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX} Dockerfile_solver_build "${DOCKER_OPTS[@]}"
+  docker_build_and_push 1 ${REPOSITORY}/klee_deps:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} Dockerfile_klee_deps "${DOCKER_OPTS[@]}"
+fi
+
+if [[ -z ${DOCKER_BUILD_DEPS_ONLY} || "${DOCKER_BUILD_DEPS_ONLY}x" != "1x" ]]; then
+  docker build -f "${DIR}/Dockerfile_klee" "${DOCKER_OPTS[@]}" --build-arg SOLVERS="$SOLVERS" -t ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SANITIZER_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} "${KLEEDIR}"
+fi
diff --git a/scripts/build/build-travis-containers.sh b/scripts/build/build-travis-containers.sh
new file mode 100755
index 00000000..ad2ac73a
--- /dev/null
+++ b/scripts/build/build-travis-containers.sh
@@ -0,0 +1,22 @@
+#!/bin/bash
+# Build all the docker containers utilized, that would be
+# also build by TravisCI.
+#
+# Every line starting with " - LLVM_VERSION=" is a single setup
+set -e
+DIR="$(cd "$(dirname "$0")" && pwd)"
+
+# Build dependencies only
+export DOCKER_BUILD_DEPS_ONLY=1
+export KLEE_TRAVIS_BUILD="1"
+export REPOSITORY="klee"
+export TRAVIS_OS_NAME="linux"
+
+while read -r line
+do
+    name=$(echo $line| grep "\- LLVM" | xargs -L 1 | cut -d "-" -f 2)
+    if [[ "x$name" == "x" ]]; then
+      continue
+    fi
+    /bin/bash -c "$name ./scripts/build/build-docker.sh"
+done < "${DIR}/../../.travis.yml"
diff --git a/scripts/build/build-travis.sh b/scripts/build/build-travis.sh
new file mode 100755
index 00000000..47e3f088
--- /dev/null
+++ b/scripts/build/build-travis.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+# Build/setup all Travis dependencies if needed
+set -e
+if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+  export DOCKER_BUILD_DEPS_ONLY=1
+  "${KLEE_SRC_TRAVIS}/scripts/build/build-docker.sh"
+elif [[ "$TRAVIS_OS_NAME" == "osx" ]]; then
+  brew tap klee/klee
+  brew update
+  brew install ccache
+  set +e
+  brew install python@2
+  if [[ "X$?" != "X0" ]]; then
+     brew link --overwrite python@2
+  fi
+  set -e
+  pip install lit
+  export PATH="/usr/local/opt/ccache/libexec:$PATH"
+  "${KLEE_SRC_TRAVIS}/scripts/build/install-klee-deps.sh"
+else
+  echo "UNKNOWN OS ${TRAVIS_OS_NAME}"
+  exit 1
+fi
diff --git a/scripts/build/common-defaults.sh b/scripts/build/common-defaults.sh
new file mode 100644
index 00000000..5cefef19
--- /dev/null
+++ b/scripts/build/common-defaults.sh
@@ -0,0 +1,53 @@
+# This file is meant to be included by shell scripts to provide common default
+# values.
+# It is used by: travis builds; docker builds and local builds
+# Change defaults to setup different development environment
+# Defines defaults used to build a default docker image outside of Travis
+if [[ "${DOCKER_BUILD}x" == "1x" ]]; then
+  # Default for docker: Do not keep build and source files for small images
+  : "${KEEP_BUILD:=0}"
+  : "${KEEP_SRC:=0}"
+  echo "DOCKER_BUILD"
+fi
+if [[ "${KLEE_TRAVIS_BUILD}x" != "1x" ]]; then
+: "${REPOSITORY:=klee}"
+: "${LLVM_VERSION:=3.4}"
+: "${DISABLE_ASSERTIONS:=0}"
+: "${ENABLE_DEBUG:=1}"
+: "${ENABLE_OPTIMIZED:=1}"
+: "${SOLVERS:=STP}"
+: "${STP_VERSION:=2.1.2}"
+: "${Z3_VERSION:=4.4.1}"
+: "${METASMT_VERSION:=v4.rc1}"
+: "${METASMT_DEFAULT:=STP}"
+: "${METASMT_BOOST_VERSION:=}"
+: "${REQUIRES_RTTI:=0}"
+: "${KLEE_UCLIBC:=klee_uclibc_v1.0.0}"
+: "${USE_TCMALLOC:=1}"
+: "${PACKAGED:=0}"
+# undefined, address, memory
+: "${SANITIZER_BUILD:=}"
+# Defines if source and build artifacts should be preserved
+: "${KEEP_BUILD:=1}"
+: "${KEEP_SRC:=1}"
+OS="$(uname)"
+case $OS in
+  'Linux')
+    TRAVIS_OS_NAME='linux'
+    ;;
+  'Darwin')
+    TRAVIS_OS_NAME='osx'
+    ;;
+  *) ;;
+esac
+fi
+
+# General default values
+: "${TCMALLOC_VERSION:=2.4}"
+: "${GTEST_VERSION:=1.7.0}"
+
+if [[ "${DIR}x" == "x" ]]; then
+  echo "\${DIR} not set"
+  exit 1
+fi
+source "${DIR}/common-functions"
diff --git a/scripts/build/common-functions b/scripts/build/common-functions
new file mode 100644
index 00000000..45c94fef
--- /dev/null
+++ b/scripts/build/common-functions
@@ -0,0 +1,217 @@
+# Defines common function and variables used by the scripts
+
+function git_clone_or_update() {
+  local url="$1"
+  local destination="$2"
+  local branch="$3"
+
+  if [[ ! -e "${destination}/.git" ]]; then
+    git clone $([ "${branch}x" != "x" ] && echo "--depth 1 -b ${branch}" || echo "") "$url" "$destination"
+  else
+    cd "$destination"
+    git pull
+    if [[ ! -z "$branch" ]]; then
+      git checkout "${branch}"
+    fi
+  fi
+}
+
+function to_upper() {
+  echo "$1" | tr '[:lower:]' '[:upper:]'
+}
+
+function to_lower() {
+  echo "$1" | tr '[:upper:]' '[:lower:]'
+}
+
+# This file is meant to be included by shell scripts
+# that need to do a sanitized build.
+
+# Users of this script can use this variable
+# to detect if a Sanitized build was enabled.
+IS_SANITIZED_BUILD=0
+
+# Remove ":" separator
+sanitizers=(${SANITIZER_BUILD//:/ })
+# Sort sanitizers
+IFS=$'\n' sorted_sanitizers=($(sort <<<"${sanitizers[*]}"))
+unset IFS
+
+# Set variables used by clients.
+## Build variables
+SANITIZER_CXX_FLAGS=""
+SANITIZER_C_FLAGS=""
+SANITIZER_LD_FLAGS=""
+# Docker_suffix
+SANITIZER_SUFFIX=""
+
+#
+for sanitizer in ${sorted_sanitizers[@]}; do
+  # AddressSanitizer
+  if [ "X${sanitizer}" == "Xaddress" ]; then
+    echo "Using ASan"
+    flags=" -fsanitize=address -fno-omit-frame-pointer -g"
+    SANITIZER_CXX_FLAGS+=" ${flags}"
+    SANITIZER_C_FLAGS+=" ${flags}"
+    SANITIZER_LD_FLAGS+=" ${flags}"
+    SANITIZER_SUFFIX+="_asan"
+    IS_SANITIZED_BUILD=1
+    continue
+  fi
+
+  # Undefined Behaviour Sanitizer
+  if [ "X${sanitizer}" == "Xundefined" ]; then
+    echo "Using UBSan"
+    flags="-fsanitize=undefined -fno-omit-frame-pointer -g"
+    SANITIZER_CXX_FLAGS+=" ${flags}"
+    SANITIZER_C_FLAGS+=" ${flags}"
+    SANITIZER_LD_FLAGS+=" ${flags} -lubsan -fuse-ld=gold"
+    SANITIZER_SUFFIX+="_ubsan"
+    IS_SANITIZED_BUILD=1
+    continue
+  fi
+
+  # Undefined Behaviour Sanitizer
+  if [ "X${sanitizer}" == "Xmemory" ]; then
+    echo "Using Memory Sanitizer"
+    if [[ "X${PACKAGED}" == "X1" ]]; then
+      echo "simultanously memory sanitizer and packaged is not supported "
+      exit 1
+    fi
+
+    SANITIZER_SUFFIX+="_memsan"
+    SANITIZER_LLVM_UNINSTRUMENTED="${LLVM_BUILD}_uninstrumented"
+    SANITIZER_LLVM_LIBCXX="${LLVM_BUILD}_libcxx"
+
+    SANITIZER_C_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang"
+    SANITIZER_CXX_COMPILER="${SANITIZER_LLVM_UNINSTRUMENTED}/bin/clang++"
+    SANITIZER_CMAKE_C_COMPILER="-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}"
+    SANITIZER_CMAKE_CXX_COMPILER="-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}"
+
+    MSAN_LINK_FLAGS="-lc++abi -Wl,--rpath=${SANITIZER_LLVM_LIBCXX}/lib -L${SANITIZER_LLVM_LIBCXX}/lib";
+    MSAN_FLAGS="$MSAN_LINK_FLAGS -nostdinc++ \
+       -isystem ${SANITIZER_LLVM_LIBCXX}/include \
+       -isystem ${SANITIZER_LLVM_LIBCXX}/include/c++/v1  \
+       -fsanitize=memory \
+       -fsanitize-memory-track-origins \
+       -w -fno-omit-frame-pointer -g";
+
+    SANITIZER_CXX_FLAGS+="${MSAN_FLAGS} -stdlib=libc++"
+    SANITIZER_C_FLAGS+="${MSAN_FLAGS}"
+    SANITIZER_LD_FLAGS+="${MSAN_LINK_FLAGS}"
+
+    IS_SANITIZED_BUILD=1
+    continue
+  fi
+
+  echo "Unknown sanitizer: $sanitizer"
+  exit 1
+done
+
+# This file is meant to be included by shell scripts
+# that need to retrieve llvm-specifi variables
+
+LLVM_VERSION_SHORT="${LLVM_VERSION/./}"
+LLVM_SUFFIX=""
+
+BuildMode=''
+
+# Build from source
+if [[ "${PACKAGED}x" == "1x" ]]; then
+  LLVM_SUFFIX+="_packaged"
+  set +e
+  llvm_config_path=$(which llvm-config-${LLVM_VERSION})
+  if [[ -e "${llvm_config_path}" ]]; then
+    LLVM_BIN="$(llvm-config-${LLVM_VERSION} --bindir)"
+  fi
+  set -e
+else
+  if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then
+    LLVM_SUFFIX+="_O"
+    BuildMode="Release"
+  else
+    LLVM_SUFFIX+="_NO"
+  fi
+
+  if [[ ("${ENABLE_DEBUG}" == "1") || ("${ENABLE_OPTIMIZED}" != "1") ]]; then
+    LLVM_SUFFIX+="_D"
+    [ -z "$BuildMode" ] && BuildMode="Debug" || BuildMode="$BuildMode+Debug"
+  else
+    LLVM_SUFFIX+="_ND"
+  fi
+
+  if [[ "${DISABLE_ASSERTIONS}" == "1" || -z "${DISABLE_ASSERTIONS}" ]]; then
+    LLVM_SUFFIX+="_NA"
+  else
+    LLVM_SUFFIX+="_A"
+    [ -z "$BuildMode" ] && BuildMode="Asserts" || BuildMode="$BuildMode+Asserts"
+  fi
+
+  if [[ "${REQUIRES_RTTI}" == "1" ]]; then
+    LLVM_SUFFIX+="_RTTI"
+  fi
+
+  if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then
+    LLVM_SUFFIX+="${SANITIZER_SUFFIX}"
+  fi
+
+  LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}"
+  LLVM_BUILD="${LLVM_BASE}-build${LLVM_SUFFIX}"
+  LLVM_INSTALL="${LLVM_BASE}-install${LLVM_SUFFIX}"
+  LLVM_BIN="${LLVM_INSTALL}/bin"
+  if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then
+    LLVM_BUILDMODE="$BuildMode"
+    LLVM_BUILD_BIN="${LLVM_BUILD}/${LLVM_BUILDMODE}/bin"
+  else
+    LLVM_BUILD_BIN="${LLVM_BUILD}/bin"
+  fi
+fi
+
+# Generate the suffix used for the solver combination
+# Every solver needs to have a version explicitly specified
+SOLVER_SUFFIX=""
+
+# Remove ":" separator
+solvers=(${SOLVERS//:/ })
+
+# Sort solvers
+IFS=$'\n' sorted_solvers=($(sort <<<"${solvers[*]}"))
+unset IFS
+
+for solver in ${sorted_solvers[@]}; do
+  # Make sure version a solver specific version variable is used
+  solver_var="$(to_upper "$solver")_VERSION"
+  SOLVER_VERSION="${!solver_var}"
+  if [[ -z "${SOLVER_VERSION}" ]] ; then
+  	echo "Solver version for $solver not defined"
+  	exit 1
+  fi
+  # Add the solver to the suffix and lower case it
+  SOLVER_SUFFIX+="_$(to_lower "$solver")$(to_lower "$SOLVER_VERSION")"
+  echo $SOLVER_SUFFIX
+  if [[ "$(to_lower "$solver")" == "metasmt" ]]; then
+    if [[ "${REQUIRES_RTTI}x" != "1x" ]]; then
+      echo "METASMT requires an RTTI build"
+      exit 1
+    fi
+    if [[ -z "${METASMT_DEFAULT}" ]]; then
+      echo "METASMT_DEFAULT not defined"
+      exit 1
+    fi
+    if [[ -z "${METASMT_BOOST_VERSION}" ]] ; then
+      echo "METASMT_BOOST_VERSION not defined - use default"
+      SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_boost-dev"
+    else
+      SOLVER_SUFFIX+="_$(to_lower "$METASMT_DEFAULT")_$(to_lower "$METASMT_BOOST_VERSION")"
+    fi
+  fi
+done
+
+# This file is meant to be included by shell scripts that handle dependencies by
+# KLEE beside LLVM and solvers
+#
+# Generate the suffix used for direct dependencies of KLEE like uclibc
+DEPS_SUFFIX=""
+if [[ "${KLEE_UCLIBC}" != "0" ]]; then
+  DEPS_SUFFIX+="_${KLEE_UCLIBC}"
+fi
diff --git a/scripts/build/dependencies-ubuntu.sh b/scripts/build/dependencies-ubuntu.sh
new file mode 100755
index 00000000..065893cd
--- /dev/null
+++ b/scripts/build/dependencies-ubuntu.sh
@@ -0,0 +1,42 @@
+#!/bin/bash
+# Installs ubuntu dependencies
+set -e
+
+# Update packages
+apt update
+
+# Install essential build tools
+apt -y --no-install-recommends install build-essential software-properties-common wget
+
+# Add repository for additional compilers
+add-apt-repository ppa:ubuntu-toolchain-r/test -y
+add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial main"
+wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add -
+apt update -y
+
+#Install essential dependencies
+apt -y --no-install-recommends install \
+  binutils \
+  bison \
+  cmake \
+  flex \
+  git \
+  groff-base \
+  libboost-program-options-dev \
+  libncurses-dev \
+  ninja-build \
+  patch \
+  perl \
+	python \
+  python3-dev \
+  python3-pip \
+	python3-setuptools \
+  subversion \
+	sudo \
+  unzip \
+  wget \
+  zlib1g-dev
+apt clean
+
+# Install lit for testing
+pip3 install wheel && pip3 install lit
diff --git a/scripts/build/install-klee-deps.sh b/scripts/build/install-klee-deps.sh
new file mode 100755
index 00000000..622e621f
--- /dev/null
+++ b/scripts/build/install-klee-deps.sh
@@ -0,0 +1,26 @@
+#!/bin/bash
+set -e
+###########################################################################
+# Install KLEE dependencies
+###########################################################################
+DIR="$(cd "$(dirname "$0")" && pwd)"
+
+if [[ "${BASE}x" == "x" ]]; then
+  echo "\${BASE} not set"
+  exit 1
+fi
+
+# Install LLVM and the LLVM bitcode compiler we require to build KLEE
+"${DIR}/llvm.sh"
+
+# Install allocators
+"${DIR}/tcmalloc.sh"
+
+# Get SMT solvers
+"${DIR}/solvers.sh"
+
+# Get needed utlities/libraries for testing KLEE
+"${DIR}/testing-utils.sh"
+
+# Install uclibc
+"${DIR}/uclibc.sh"
diff --git a/scripts/build/install-local.sh b/scripts/build/install-local.sh
new file mode 100755
index 00000000..50dfb612
--- /dev/null
+++ b/scripts/build/install-local.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+# Install all dependencies to build KLEE in a directory ${BASE}
+set -e
+if [[ "${BASE}x" == "x" ]]; then
+  echo "\${BASE} not set"
+  exit 1
+fi
+
+# Create base directory if not exists
+mkdir -p "${BASE}"
+DIR=$(dirname "$(readlink -f "$0" || stat -f "$0")")
+
+# Install dependencies
+"${DIR}/install-klee-deps.sh"
+
+# Build KLEE
+"${DIR}/klee.sh"
diff --git a/.travis/klee.sh b/scripts/build/klee.sh
index 5c5a15b5..2b68dd7e 100755
--- a/.travis/klee.sh
+++ b/scripts/build/klee.sh
@@ -1,43 +1,35 @@
 #!/bin/bash -x
+# Compile KLEE
 # Make sure we exit if there is a failure
 set -e
-: ${SOLVERS?"Solvers must be specified"}
 
-coverage_setup()
-{
-  # Zero coverage for any file, e.g. previous tests
-  lcov --directory . --no-external --zerocounters
-  # Create a baseline by capturing any file used for compilation, no execution yet
-  lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --initial --output-file coverage_base.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info
-}
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
 
-coverageup()
-{
-  # Create report
-  # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped)
-  lcov --rc lcov_branch_coverage=1 --directory . --base-directory=${KLEE_SRC} --no-external --capture --output-file coverage.info
-  # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests)
-  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info
-  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info
-  # Combine baseline and measured coverage
-  lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info
-  # Debug info
-  lcov --rc lcov_branch_coverage=1 --list coverage_all.info
-  # Uploading report to CodeCov
-  bash <(curl -s https://codecov.io/bash) -R ${KLEE_SRC} -X gcov -y ${KLEE_SRC}/.codecov.yml -f coverage_all.info -F $1
-}
+: ${SOLVERS?"Solvers must be specified"}
+if [[ -z "${KLEE_UCLIBC}" ]]; then
+  echo "KLEE_UCLIBC must be specified: 0 or branch/tag"
+  exit 1
+fi
+if [[ -z "${KLEE_SRC}" ]]; then
+  # Assumeption: this build script is part of the KLEE source tree
+  KLEE_SRC="${DIR}/../.."
+fi
 
+CMAKE_PREFIX_PATH=""
 ###############################################################################
-# Select the compiler to use to generate LLVM bitcode
+# Handling LLVM configuration
 ###############################################################################
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  KLEE_CC=/usr/bin/clang-${LLVM_VERSION}
-  KLEE_CXX=/usr/bin/clang++-${LLVM_VERSION}
+if [[ "$TRAVIS_OS_NAME" = "linux" ]] ; then
+  LLVM_CONFIG="${LLVM_BIN}/llvm-config"
+  LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION_SHORT}/build"
+  KLEE_CC="${LLVM_BIN}/clang"
+  KLEE_CXX="${LLVM_BIN}/clang++"
 elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  KLEE_CC=/usr/local/bin/clang-${LLVM_VERSION}
-  KLEE_CXX=/usr/local/bin/clang++-${LLVM_VERSION}
+  LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}"
+  LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)"
+  KLEE_CC="/usr/local/bin/clang-${LLVM_VERSION}"
+  KLEE_CXX="/usr/local/bin/clang++-${LLVM_VERSION}"
 else
   echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
   exit 1
@@ -47,14 +39,9 @@ fi
 # klee-uclibc
 ###############################################################################
 if [ "${KLEE_UCLIBC}" != "0" ]; then
-    git clone --depth 1 -b ${KLEE_UCLIBC} git://github.com/klee/klee-uclibc.git
-    cd klee-uclibc
-    ./configure --make-llvm-lib --with-cc "${KLEE_CC}" --with-llvm-config /usr/bin/llvm-config-${LLVM_VERSION}
-    make
-    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH=$(pwd) -DENABLE_POSIX_RUNTIME=TRUE"
-    cd ../
+    KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=TRUE -DKLEE_UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" -DENABLE_POSIX_RUNTIME=TRUE)
 else
-    KLEE_UCLIBC_CONFIGURE_OPTION="-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE"
+    KLEE_UCLIBC_CONFIGURE_OPTION=(-DENABLE_KLEE_UCLIBC=FALSE -DENABLE_POSIX_RUNTIME=FALSE)
 fi
 
 COVERAGE_FLAGS=""
@@ -66,28 +53,31 @@ fi
 ###############################################################################
 # Handle setting up solver configure flags for KLEE
 ###############################################################################
-SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
+SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g')
 
 # Set CMake configure options
-KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=OFF"
-KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=OFF"
-KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=OFF"
+KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=OFF)
+KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=OFF)
+KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=OFF)
 for solver in ${SOLVER_LIST}; do
   echo "Setting CMake configuration option for ${solver}"
   case ${solver} in
   STP)
-    KLEE_STP_CONFIGURE_OPTION="-DENABLE_SOLVER_STP=TRUE -DSTP_DIR=${BUILD_DIR}/stp/build"
+    KLEE_STP_CONFIGURE_OPTION=(-DENABLE_SOLVER_STP=TRUE -DSTP_DIR="${BASE}/stp-${STP_VERSION}-install")
     ;;
   Z3)
     echo "Z3"
-    KLEE_Z3_CONFIGURE_OPTION="-DENABLE_SOLVER_Z3=TRUE"
+    KLEE_Z3_CONFIGURE_OPTION=(-DENABLE_SOLVER_Z3=TRUE)
+    if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+    	KLEE_Z3_CONFIGURE_OPTION+=(-DZ3_INCLUDE_DIRS="${BASE}/z3-${Z3_VERSION}-install/include" -DZ3_LIBRARIES="${BASE}/z3-${Z3_VERSION}-install/lib/libz3.so")
+    fi
     ;;
   metaSMT)
     echo "metaSMT"
     if [ "X${METASMT_DEFAULT}" == "X" ]; then
       METASMT_DEFAULT=STP
     fi
-    KLEE_METASMT_CONFIGURE_OPTION="-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR=${BUILD_DIR}/metaSMT/build -DMETASMT_DEFAULT_BACKEND=${METASMT_DEFAULT}"
+    KLEE_METASMT_CONFIGURE_OPTION=(-DENABLE_SOLVER_METASMT=TRUE -DmetaSMT_DIR="${BASE}/metaSMT/build" -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}")
     ;;
   *)
     echo "Unknown solver ${solver}"
@@ -98,34 +88,22 @@ done
 ###############################################################################
 # Handle additional configure flags
 ###############################################################################
-TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
 
-###############################################################################
-# Handle Sanitizer flags
-###############################################################################
-source ${KLEE_SRC}/.travis/sanitizer_flags.sh
-
-###############################################################################
-# Handling LLVM configuration
-###############################################################################
-if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
-  LLVM_CONFIG="/usr/lib/llvm-${LLVM_VERSION}/bin/llvm-config"
-  LLVM_BUILD_DIR="/usr/lib/llvm-${LLVM_VERSION}/build"
-elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
-  LLVM_CONFIG="/usr/local/bin/llvm-config-${LLVM_VERSION}"
-  LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)"
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
+TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "-DENABLE_TCMALLOC=TRUE" || echo "-DENABLE_TCMALLOC=FALSE")
+if [[ "$TCMALLOC_OPTION" != "0" ]] ; then
+  if [[ ! -z "${CMAKE_PREFIX_PATH}" ]]; then
+    CMAKE_PREFIX_PATH+=":"
+  fi
+  CMAKE_PREFIX_PATH="${CMAKE_PREFIX_PATH}$BASE/tcmalloc-install"
 fi
 
 ###############################################################################
 # KLEE
 ###############################################################################
-mkdir klee
-cd klee
-
-GTEST_SRC_DIR="${BUILD_DIR}/test-utils/googletest-release-1.7.0/"
+KLEE_BUILD="${BASE}/klee_build${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX}"
+mkdir -p "${KLEE_BUILD}"
+cd "${KLEE_BUILD}"
+GTEST_SRC_DIR="${BASE}/googletest-release-${GTEST_VERSION}/"
 if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
   KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=FALSE"
 else
@@ -140,25 +118,63 @@ fi
 
 # TODO: We should support Ninja too
 # Configure KLEE
-CXXFLAGS="${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}" \
-CFLAGS="${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}" \
+echo "CXXFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_CXX_FLAGS}\" \
+CFLAGS=\"${COVERAGE_FLAGS} ${SANITIZER_C_FLAGS}\" \
+LDFLAGS=\"${COVERAGE_LDFLAGS} ${SANITIZER_LD_FLAGS}\" \
 cmake \
-  -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}" \
-  -DLLVMCC="${KLEE_CC}" \
-  -DLLVMCXX="${KLEE_CXX}" \
-  ${KLEE_STP_CONFIGURE_OPTION} \
-  ${KLEE_Z3_CONFIGURE_OPTION} \
-  ${KLEE_METASMT_CONFIGURE_OPTION} \
-  ${KLEE_UCLIBC_CONFIGURE_OPTION} \
-  ${TCMALLOC_OPTION} \
+  -DLLVM_CONFIG_BINARY=\"${LLVM_CONFIG}\" \
+  -DLLVMCC=\"${KLEE_CC}\" \
+  -DLLVMCXX=\"${KLEE_CXX}\" \
+  ${KLEE_STP_CONFIGURE_OPTION[@]} \
+  ${KLEE_Z3_CONFIGURE_OPTION[@]} \
+  ${KLEE_METASMT_CONFIGURE_OPTION[@]} \
+  ${KLEE_UCLIBC_CONFIGURE_OPTION[@]} \
+  ${TCMALLOC_OPTION[@]} \
   -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
   -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
-  ${KLEE_ASSERTS_OPTION} \
+  ${KLEE_ASSERTS_OPTION[@]} \
   -DENABLE_UNIT_TESTS=TRUE \
   -DENABLE_SYSTEM_TESTS=TRUE \
-  -DLIT_ARGS="-v" \
-  ${KLEE_SRC}
-make
+  -DLIT_ARGS=\"-v\" \
+  ${SANITIZER_CMAKE_C_COMPILER[@]} \
+  ${SANITIZER_CMAKE_CXX_COMPILER[@]} \
+  -DCMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH} \
+  ${KLEE_SRC}" > "${KLEE_BUILD}/.build_command"
+source "${KLEE_BUILD}/.build_command"
+make -j$(nproc)
+
+###############################################################################
+# Prepare Coverage functionality
+###############################################################################
+coverage_setup()
+{
+  # TODO Remove it and put it to the proper package install section
+  apt update && apt -y --no-install-recommends install lcov
+  # Zero coverage for any file, e.g. previous tests
+  lcov --directory . --no-external --zerocounters
+  # Create a baseline by capturing any file used for compilation, no execution yet
+  lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info
+}
+
+coverageup()
+{
+  # Create report
+  # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped)
+  lcov --rc lcov_branch_coverage=1 --directory . --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info
+  # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests)
+  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info
+  lcov --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info
+  # Combine baseline and measured coverage
+  lcov --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info
+  # Debug info
+  lcov --rc lcov_branch_coverage=1 --list coverage_all.info
+  # Uploading report to CodeCov
+  bash <(curl -s https://codecov.io/bash) -R "${KLEE_SRC}" -X gcov -y "${KLEE_SRC}/.codecov.yml" -f coverage_all.info -F $1
+}
+
+COVERAGE=${COVERAGE:=0}
 
 ###############################################################################
 # Unit tests
@@ -184,7 +200,7 @@ make systemtests
 
 # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
 if [ "X${SOLVERS}" == "XmetaSMT" ]; then
-  metasmt_default=`echo "${METASMT_DEFAULT,,}"` # klee_opts and kleaver_opts use lowercase
+  metasmt_default=$(to_lower $METASMT_DEFAULT) # klee_opts and kleaver_opts use lowercase
   available_metasmt_backends="btor stp z3 yices2 cvc4"
   for backend in $available_metasmt_backends; do
     if [ "X${metasmt_default}" != "X$backend" ]; then
diff --git a/scripts/build/llvm.sh b/scripts/build/llvm.sh
new file mode 100755
index 00000000..459fdef9
--- /dev/null
+++ b/scripts/build/llvm.sh
@@ -0,0 +1,204 @@
+#!/bin/bash -x
+set -ev
+STAGE="$1"
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+if [[ "${LLVM_VERSION_SHORT}" == "" ]]; then
+  echo "LLVM_VERSION_SHORT not set"
+  exit 1
+fi
+
+if [[ "${BASE}" == "" ]]; then
+  echo "BASE not set"
+  exit 1
+fi
+
+# Install packages if possible
+if [[ "${PACKAGED}x" == "1x" ]]; then
+  apt update
+  apt install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev
+  apt install -y clang-${LLVM_VERSION}
+  exit 0
+fi
+
+if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+  LLVM_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}"
+  # Checkout LLVM code
+  svn co http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_VERSION_SHORT} "${LLVM_BASE}"
+  cd "${LLVM_BASE}/tools"
+  svn co http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_VERSION_SHORT} clang
+  cd "${LLVM_BASE}/projects"
+  svn co http://llvm.org/svn/llvm-project/compiler-rt/branches/release_${LLVM_VERSION_SHORT} compiler-rt
+
+  if [[ ${LLVM_VERSION_SHORT} -gt 37 ]]; then
+    cd "${LLVM_BASE}/projects"
+    svn co http://llvm.org/svn/llvm-project/libcxx/branches/release_${LLVM_VERSION_SHORT} libcxx
+    cd "${LLVM_BASE}/projects"
+    svn co http://llvm.org/svn/llvm-project/libcxxabi/branches/release_${LLVM_VERSION_SHORT} libcxxabi
+  fi
+
+  # Apply existing patches if needed
+  if [ -f "${BASE}/scripts/build/llvm${LLVM_VERSION_SHORT}.patch" ]; then
+     cd "${LLVM_BASE}"
+     patch -p0 -i "${BASE}/scripts/build/llvm${LLVM_VERSION_SHORT}.patch"
+  fi
+fi
+
+
+# For memory sanitizer, we have a multi-stage build process
+if [[ "${SANITIZER_BUILD}" == "memory" ]]; then
+   if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then
+     echo "Memory sanitizer builds for <= LLVM 3.7 are not supported"
+     exit 1
+   fi
+   # Build uninstrumented compiler
+   mkdir "${SANITIZER_LLVM_UNINSTRUMENTED}"
+   cd "${SANITIZER_LLVM_UNINSTRUMENTED}"
+   cmake -GNinja -DCMAKE_BUILD_TYPE=Release "${LLVM_BASE}"
+   ninja
+
+   # Build instrumented libc/libc++
+   mkdir "${SANITIZER_LLVM_LIBCXX}"
+   cd "${SANITIZER_LLVM_LIBCXX}"
+   cmake -GNinja -DCMAKE_BUILD_TYPE=RelWithDebInfo \
+    -DLLVM_USE_SANITIZER=MemoryWithOrigins \
+    ${SANITIZER_CMAKE_C_COMPILER} \
+    ${SANITIZER_CMAKE_CXX_COMPILER} \
+    "${LLVM_BASE}"
+   ninja cxx cxxabi
+
+   # Build instrumented clang
+   mkdir "${LLVM_BUILD}"
+   cd "${LLVM_BUILD}"
+   cmake -GNinja \
+      ${SANITIZER_CMAKE_C_COMPILER} \
+      ${SANITIZER_CMAKE_CXX_COMPILER} \
+      -DCMAKE_C_FLAGS="$SANITIZER_C_FLAGS" \
+      -DCMAKE_CXX_FLAGS="$SANITIZER_CXX_FLAGS" \
+      -DCMAKE_BUILD_TYPE=Release \
+      -DLLVM_USE_SANITIZER=MemoryWithOrigins \
+      -DLLVM_ENABLE_LIBCXX=ON \
+      -DCMAKE_EXE_LINKER_FLAGS="$SANITIZER_LD_FLAGS" \
+      -DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}" \
+      "${LLVM_BASE}"
+  # Build clang as a dependency and install all needed packages
+  ninja clang
+  ninja install-clang install-llvm-config install-llvm-objdump \
+      install-llvm-link install-llvm-ar install-llvm-nm install-llvm-dis \
+      install-clang-headers install-llvm-as installhdrs install-LLVMX86Disassembler \
+      install-LLVMX86AsmParser install-LLVMX86CodeGen install-LLVMSelectionDAG \
+      install-LLVMAsmPrinter install-LLVMX86Desc install-LLVMMCDisassembler \
+      install-LLVMX86Info install-LLVMX86AsmPrinter install-LLVMX86Utils \
+      install-LLVMMCJIT install-LLVMExecutionEngine install-LLVMRuntimeDyld \
+      install-LLVMipo install-LLVMVectorize install-LLVMLinker install-LLVMIRReader \
+      install-LLVMAsmParser install-LLVMCodeGen install-LLVMTarget install-LLVMScalarOpts \
+      install-LLVMInstCombine install-LLVMInstrumentation install-LLVMProfileData \
+      install-LLVMObject install-LLVMMCParser install-LLVMTransformUtils install-LLVMMC \
+      install-LLVMAnalysis install-LLVMBitWriter install-LLVMBitReader install-LLVMCore \
+      install-llvm-symbolizer install-LLVMSupport install-lli not FileCheck
+  cp "${LLVM_BUILD}/bin/FileCheck" "${LLVM_INSTALL}/bin/"
+  cp "${LLVM_BUILD}/bin/not" "${LLVM_INSTALL}/bin/"
+  exit 0
+fi
+
+if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+  # Configure; build; and install
+  mkdir -p "${LLVM_BUILD}"
+  cd "${LLVM_BUILD}"
+
+  # Skip building if already finished
+  if [[ -e "${LLVM_BUILD}/.build_finished" ]]; then
+    exit 0
+  fi
+
+
+  # Configure LLVM
+  if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then
+    CONFIG=(--enable-jit --prefix="${LLVM_INSTALL}")
+    if [[ "${ENABLE_OPTIMIZED}" == "1" ]]; then
+      CONFIG+=(--enable-optimized)
+    else
+      CONFIG+=(--disable-optimized)
+    fi
+
+    if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then
+      CONFIG+=(--disable-assertions)
+    else
+      CONFIG+=(--enable-assertions)
+    fi
+
+    if [[ "${ENABLE_DEBUG}" == "1" ]]; then
+      CONFIG+=(--enable-debug-runtime --enable-debug-symbols)
+    else
+      CONFIG+=(--disable-debug-symbols)
+    fi
+    CC=${CC} CXX=${CXX} CFLAGS="${LLVM_CFLAGS}" CXXFLAGS="${LLVM_CXXFLAGS}" LDFLAGS="${LLVM_LDFLAGS}" "${LLVM_BASE}/configure" "${CONFIG[@]}"
+  else
+    CONFIG=(-DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}")
+    # cmake build
+    if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" != "1" ]]; then
+      CONFIG+=(-DCMAKE_BUILD_TYPE=Release)
+    fi
+    if [[ "${ENABLE_OPTIMIZED}" == "1" && "${ENABLE_DEBUG}" == "1" ]]; then
+      CONFIG+=(-DCMAKE_BUILD_TYPE=RelWithDebInfo)
+    fi
+    if [[ "${ENABLE_OPTIMIZED}" != "1" && "${ENABLE_DEBUG}" == "1" ]]; then
+      CONFIG+=(-DCMAKE_BUILD_TYPE=Debug)
+    fi
+
+    if [[ "${DISABLE_ASSERTIONS}" == "1" ]]; then
+      CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=Off)
+    else
+      CONFIG+=(-DLLVM_ENABLE_ASSERTIONS=On)
+    fi
+
+    if [[ ! -z "${LLVM_CFLAGS}" ]] ; then
+      CONFIG+=(-DCMAKE_C_FLAGS="$LLVM_CFLAGS")
+    fi
+
+    if [[ ! -z "${LLVM_CXXFLAGS}" ]] ; then
+      CONFIG+=(-DCMAKE_CXX_FLAGS="$LLVM_CXXFLAGS")
+    fi
+
+    if [[ ! -z "${LLVM_LDFLAGS}" ]]; then
+       LDFLAGS="${LLVM_LDFLAGS}"
+    fi
+
+    cmake "${CONFIG[@]}" "${LLVM_BASE}"
+  fi
+
+  make -j$(nproc)
+  make install
+
+  touch "${LLVM_BUILD}/.build_finished"
+
+  cp "${LLVM_BUILD_BIN}/FileCheck" "${LLVM_INSTALL}/bin/"
+  cp "${LLVM_BUILD_BIN}/not" "${LLVM_INSTALL}/bin/"
+
+  if [[ "${KEEP_BUILD}x" != "1x" ]]; then
+    rm -rf "${LLVM_BUILD}"
+  fi
+
+  if [[ "${KEEP_SRC}x" != "1x" ]]; then
+    rm -rf "${LLVM_BASE}"
+  fi
+elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
+  # We use our own local cache if possible
+  set +e
+  brew install "$HOME/Library/Caches/Homebrew/llvm\@${LLVM_VERSION}*.bottle.tar.gz"
+  RES=$?
+  set -ev
+  if [ ${RES} -ne 0 ]; then
+    # This might build the llvm package use a time out to avoid dumping log information
+    brew install -v --build-bottle "llvm@${LLVM_VERSION}"
+    # Now bottle the brew
+    brew bottle llvm\@${LLVM_VERSION}
+    # Not make sure it's cached
+    cp llvm\@${LLVM_VERSION}*.bottle.tar.gz $HOME/Library/Caches/Homebrew/
+  fi
+else
+  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
diff --git a/scripts/build/patches/llvm35.patch b/scripts/build/patches/llvm35.patch
new file mode 100644
index 00000000..47744b91
--- /dev/null
+++ b/scripts/build/patches/llvm35.patch
@@ -0,0 +1,14 @@
+*** include/llvm/ADT/IntrusiveRefCntPtr.h       2014-07-06 00:20:59.000000000 +0200
+--- include/llvm/ADT/IntrusiveRefCntPtr_new.h   2016-06-21 10:04:15.610143165 +0200
+***************
+*** 154,159 ****
+--- 154,162 ----
+      }
+
+      template <class X>
++     friend class IntrusiveRefCntPtr;
++
++     template <class X>
+      IntrusiveRefCntPtr(IntrusiveRefCntPtr<X>&& S) : Obj(S.get()) {
+        S.Obj = 0;
+      }
diff --git a/scripts/build/solver-metasmt.sh b/scripts/build/solver-metasmt.sh
new file mode 100755
index 00000000..d8626149
--- /dev/null
+++ b/scripts/build/solver-metasmt.sh
@@ -0,0 +1,39 @@
+#!/bin/bash -x
+set -e
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+: ${METASMT_VERSION?"METASMT_VERSION not specified"}
+
+# Get Z3, libgmp, gperf (required by yices2)
+apt update
+apt -y --no-install-recommends install gperf libgmp-dev
+apt clean
+rm -rf /var/lib/apt/lists/*
+
+# Clone
+git clone --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git "${BASE}/metaSMT"
+cd "${BASE}/metaSMT"
+git submodule update --init
+
+if [ "X${IS_SANITIZED_BUILD}" != "X0" ]; then
+  echo "Error: Requested Sanitized build but sanitized build of metaSMT is not implemented"
+  exit 1
+fi
+
+# Bootstrap
+git clone https://github.com/agra-uni-bremen/dependencies.git
+./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off \
+  --build stp-git-basic --build boolector-2.2.0 --build minisat-git \
+  --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 --build Z3-4.4.1 \
+  --build cvc4-1.5
+
+# Build
+make -C build install
+
+# Cleanup
+if [[ "${STORAGE_SPACE_OPTIMIZED}x" == "1x" ]]; then
+  rm -rf deps/build
+  rm -rf deps/cache
+fi
diff --git a/scripts/build/solver-stp.sh b/scripts/build/solver-stp.sh
new file mode 100755
index 00000000..2e65ca30
--- /dev/null
+++ b/scripts/build/solver-stp.sh
@@ -0,0 +1,57 @@
+#!/bin/bash -x
+
+# TODO: For OSX we can prepare bottled formulas for STP and minisat
+
+# Make sure we exit if there is a failure
+set -e
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+cd ${BASE}
+if [ "x${STP_VERSION}" != "x" ]; then
+  # Build minisat
+  git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat"
+  mkdir -p "${BASE}/minisat/build"
+  cd "${BASE}/minisat/build"
+  MINISAT_DIR="$(pwd)"
+  if [[ "$TRAVIS_OS_NAME" == "linux" || "$TRAVIS_OS_NAME" == "osx" ]]; then
+    CFLAGS="${SANITIZER_C_FLAGS}" \
+    CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
+    LDFLAGS="${SANITIZER_LD_FLAGS}" \
+    cmake -DCMAKE_INSTALL_PREFIX="${BASE}/minisat-install" \
+      ${SANITIZER_CMAKE_C_COMPILER} \
+      ${SANITIZER_CMAKE_CXX_COMPILER} \
+      "${BASE}/minisat"
+  else
+    echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+    exit 1
+  fi
+  make
+  make install
+
+  # Build STP
+  git_clone_or_update git://github.com/stp/stp.git "${BASE}/stp-${STP_VERSION}" ${STP_VERSION}
+  mkdir -p "${BASE}/stp-${STP_VERSION}-build"
+  cd "${BASE}/stp-${STP_VERSION}-build"
+
+  STP_CMAKE_FLAGS=( \
+     "-DENABLE_PYTHON_INTERFACE:BOOL=OFF" \
+     -DNO_BOOST:BOOL=ON \
+     -DENABLE_PYTHON_INTERFACE:BOOL=OFF \
+     ${SANITIZER_CMAKE_C_COMPILER} \
+     ${SANITIZER_CMAKE_CXX_COMPILER} \
+  )
+  # Disabling building of shared libs is a workaround.
+  # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8
+  CFLAGS="${SANITIZER_C_FLAGS}" \
+  CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
+  LDFLAGS="${SANITIZER_LD_FLAGS}" \
+  cmake ${STP_CMAKE_FLAGS} \
+        -DCMAKE_PREFIX_PATH="${BASE}/minisat-install" "${BASE}/stp-${STP_VERSION}" \
+        -DCMAKE_INSTALL_PREFIX="${BASE}/stp-${STP_VERSION}-install"
+  make
+  make install
+else
+  echo "No STP_VERSION given or empty"
+  exit 1
+fi
diff --git a/scripts/build/solver-z3.sh b/scripts/build/solver-z3.sh
new file mode 100755
index 00000000..c6c3381d
--- /dev/null
+++ b/scripts/build/solver-z3.sh
@@ -0,0 +1,34 @@
+#!/bin/bash -x
+
+# Make sure we exit if there is a failure
+set -e
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+if [[ -z "${Z3_VERSION}" ]] ; then
+  echo "Z3_VERSION is not defined"
+  exit 1
+fi
+
+if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+  mkdir -p "${BASE}/z3-${Z3_VERSION}"
+  cd "${BASE}/z3-${Z3_VERSION}"
+  wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1
+  LDFLAGS="${SANITIZER_LD_FLAGS}" \
+  CXXFLAGS="${SANITIZER_CXX_FLAGS}" \
+  python scripts/mk_make.py --prefix "${BASE}/z3-${Z3_VERSION}-install"
+  cd build
+  make -j$(nproc)
+  make install
+elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
+  set +e
+  brew install python@2
+  if [[ "X$?" != "X0" ]]; then
+     brew link --overwrite python@2
+  fi
+  set -e
+  brew install z3
+else
+  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
diff --git a/.travis/solvers.sh b/scripts/build/solvers.sh
index b419d679..71ad0c2d 100755
--- a/.travis/solvers.sh
+++ b/scripts/build/solvers.sh
@@ -1,27 +1,27 @@
 #!/bin/bash -x
 # Make sure we exit if there is a failure
 set -e
-: ${SOLVERS?"Solvers must be specified"}
 
-SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+: ${SOLVERS?"Solvers must be specified"}
+SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /g')
 
 for solver in ${SOLVER_LIST}; do
   echo "Getting solver ${solver}"
   case ${solver} in
   STP)
     echo "STP"
-    mkdir stp
-    cd stp
-    ${KLEE_SRC}/.travis/stp.sh
-    cd ../
+    "${DIR}/solver-stp.sh"
     ;;
   Z3)
     echo "Z3"
-    ${KLEE_SRC}/.travis/z3.sh
+    "${DIR}/solver-z3.sh"
     ;;
   metaSMT)
     echo "metaSMT"
-    ${KLEE_SRC}/.travis/metaSMT.sh
+    "${DIR}/solver-metasmt.sh"
     ;;
   *)
     echo "Unknown solver ${solver}"
diff --git a/scripts/build/tcmalloc.sh b/scripts/build/tcmalloc.sh
new file mode 100755
index 00000000..ea5596d0
--- /dev/null
+++ b/scripts/build/tcmalloc.sh
@@ -0,0 +1,35 @@
+#!/bin/bash -x
+set -ev
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then
+  # Get tcmalloc release
+  if [[ ! -e "${BASE}/gperftools-${TCMALLOC_VERSION}" ]]; then
+    cd "${BASE}"
+    wget "https://github.com/gperftools/gperftools/releases/download/gperftools-${TCMALLOC_VERSION}/gperftools-${TCMALLOC_VERSION}.tar.gz"
+    tar xfz "gperftools-${TCMALLOC_VERSION}.tar.gz"
+  fi
+  cd "${BASE}/gperftools-${TCMALLOC_VERSION}"
+  ./configure --disable-dependency-tracking --disable-cpu-profiler \
+    --disable-heap-checker --disable-debugalloc  --enable-minimal \
+    --prefix="${BASE}/tcmalloc-install"
+  make
+  make install
+  if [[ "${KEEP_BUILD}x" != "1x" ]]; then
+    rm -rf "${BASE}/gperftools-${TCMALLOC_VERSION}"
+  fi
+
+  if [[ "${KEEP_SRC}x" != "1x" ]]; then
+    rm -f "${BASE}/gperftools-${TCMALLOC_VERSION}.tar.gz"
+  fi
+elif [[ "${TRAVIS_OS_NAME}" == "osx" ]]; then
+  if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
+    echo "Error: Requested to install TCMalloc on macOS, which is not supported"
+    exit 1
+  fi
+else
+  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
diff --git a/scripts/build/testing-utils.sh b/scripts/build/testing-utils.sh
new file mode 100755
index 00000000..8a855291
--- /dev/null
+++ b/scripts/build/testing-utils.sh
@@ -0,0 +1,14 @@
+#!/bin/bash -x
+# Make sure we exit if there is a failure
+set -e
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+# The New CMake build system just needs the GTest sources regardless
+# of LLVM version.
+cd "${BASE}"
+
+wget https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip
+unzip -o release-${GTEST_VERSION}.zip
+rm release-${GTEST_VERSION}.zip
diff --git a/scripts/build/uclibc.sh b/scripts/build/uclibc.sh
new file mode 100755
index 00000000..3440bedb
--- /dev/null
+++ b/scripts/build/uclibc.sh
@@ -0,0 +1,37 @@
+#!/bin/bash -x
+# Build the uclibc library
+# Make sure we exit if there is a failure
+set -e
+DIR="$(cd "$(dirname "$0")" && pwd)"
+source "${DIR}/common-defaults.sh"
+
+if [[ -z "${KLEE_UCLIBC}" ]]; then
+  echo "KLEE_UCLIBC must be specified: 0 or branch/tag"
+  exit 1
+fi
+
+###############################################################################
+# Handling LLVM configuration
+###############################################################################
+if [[ "$TRAVIS_OS_NAME" = "linux"  ||  "$TRAVIS_OS_NAME" = "osx" ]] ; then
+  LLVM_CONFIG="${LLVM_BIN}/llvm-config"
+  KLEE_CC="${LLVM_BIN}/clang"
+  KLEE_CXX="${LLVM_BIN}/clang++"
+else
+  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
+  exit 1
+fi
+
+###############################################################################
+# klee-uclibc
+###############################################################################
+if [ "${KLEE_UCLIBC}" != "0" ]; then
+  if [[ "$TRAVIS_OS_NAME" = "osx" ]] ; then
+    echo "UCLibc is not supported Mac OSX"
+    exit 1
+  fi
+  git_clone_or_update git://github.com/klee/klee-uclibc.git "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}" "${KLEE_UCLIBC}"
+  cd "${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}"
+  ./configure --make-llvm-lib --with-cc ${KLEE_CC} --with-llvm-config ${LLVM_CONFIG}
+  make
+fi