Updated dependency build system for KLEE

Provide a single `scripts/build/build.sh` file to build KLEE and its
dependencies.

62 files changed, 2786 insertions, 1309 deletions

diff --git a/scripts/build/Dockerfile_base b/scripts/build/Dockerfile_base
deleted file mode 100644
index 8daee330..00000000
--- a/scripts/build/Dockerfile_base
+++ /dev/null
@@ -1,15 +0,0 @@
-# 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
deleted file mode 100644
index 1872fca6..00000000
--- a/scripts/build/Dockerfile_klee
+++ /dev/null
@@ -1,58 +0,0 @@
-# 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 && ln -s ${BASE}/klee_build* ${BASE}/klee_build
-
-# 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_src /home/klee/ && ln -s ${BASE}/klee_build /home/klee/ && echo "export PATH=\"$PATH:${LLVM_BIN}:/home/klee/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
deleted file mode 100644
index 582d324f..00000000
--- a/scripts/build/Dockerfile_klee_deps
+++ /dev/null
@@ -1,33 +0,0 @@
-# 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
deleted file mode 100644
index 548f0d8a..00000000
--- a/scripts/build/Dockerfile_llvm_build
+++ /dev/null
@@ -1,27 +0,0 @@
-# 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
deleted file mode 100644
index ba2af62a..00000000
--- a/scripts/build/Dockerfile_solver_build
+++ /dev/null
@@ -1,33 +0,0 @@
-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
deleted file mode 100755
index 3a031d22..00000000
--- a/scripts/build/build-docker.sh
+++ /dev/null
@@ -1,100 +0,0 @@
-#!/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[@]}" -t ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} "${KLEEDIR}"
-fi
diff --git a/scripts/build/build-travis-containers.sh b/scripts/build/build-travis-containers.sh
index ad2ac73a..fe80e29f 100755
--- a/scripts/build/build-travis-containers.sh
+++ b/scripts/build/build-travis-containers.sh
@@ -3,20 +3,62 @@
 # also build by TravisCI.
 #
 # Every line starting with " - LLVM_VERSION=" is a single setup
+
 set -e
+#set -x
 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"
+trim() {
+    local var="$*"
+    # remove leading whitespace characters
+    var="${var#"${var%%[![:space:]]*}"}"
+    # remove trailing whitespace characters
+    var="${var%"${var##*[![:space:]]}"}"   
+    echo -n "$var"
+}
 
+# Build dependencies only
+isGlobal=0
+isEnv=0
+commons=()
+experiments=()
 while read -r line
 do
-    name=$(echo $line| grep "\- LLVM" | xargs -L 1 | cut -d "-" -f 2)
-    if [[ "x$name" == "x" ]]; then
+    [[ "${line}" == "env:"* ]] && isEnv=1 && continue
+    [[ "${line}" == "#stop"* ]] && isEnv=0 && break
+ 
+    
+    [[ "${isEnv}" -eq 0 ]] && continue
+    
+    line="$(trim "${line}")"
+
+    # Ignore empty lines
+    [[ -z "${line}" ]] && continue
+    [[ "${line}" == "#"* ]] && continue 
+    
+    [[ "${line}" == "global:"* ]] && isGlobal=1 && continue
+    [[ "${line}" == "matrix:"* ]] && isGlobal=0 && continue
+
+    
+    
+    if [[ "${isGlobal}" -eq 1 ]]; then
+      tmp="${line#*-}"
+      IFS=: read -r key value <<< "${tmp}"
+      key=$(trim "${key}")
+      [[ "${key}" == "secure" ]] && continue
+      [[ -z "${key}" ]] && continue
+      commons+=("${key}=$(trim "${value}")")
       continue
     fi
-    /bin/bash -c "$name ./scripts/build/build-docker.sh"
+
+    experiment=$(echo "$line"| grep "\- " | xargs -L 1 | cut -d "-" -f 2)
+    if [[ "x$experiment" == "x" ]]; then
+      continue
+    fi
+    experiments+=("${experiment}")
 done < "${DIR}/../../.travis.yml"
+
+for experiment in "${experiments[@]}"; do
+  [[ -z "${experiment}" ]] && continue
+  /bin/bash -c "${commons[*]} ${experiment} ${DIR}/build.sh klee --docker --push-docker-deps --debug --create-final-image"
+done
\ No newline at end of file
diff --git a/scripts/build/build.sh b/scripts/build/build.sh
new file mode 100755
index 00000000..feda6bfe
--- /dev/null
+++ b/scripts/build/build.sh
@@ -0,0 +1,803 @@
+#!/usr/bin/env bash
+set -e
+set -u
+# Build script for different components that are needed
+
+DIR="$(cd "$(dirname "$0")" && pwd)"
+
+show_help() {
+  local name="$1"
+  echo "$name [--docker] [--keep-dockerfile] [--install-system-deps] component*" 
+  echo "Available components:"
+  for component_path in "$DIR/v-"*.inc; do
+    [ -e "$component_path" ] || continue
+
+    component_path=${component_path#"$DIR/v-"}
+    component=${component_path%".inc"}
+
+    echo "$component"
+  done
+
+  return 0
+}
+
+function to_upper() {
+  echo "$1" | tr '[:lower:]' '[:upper:]'
+}
+
+function to_lower() {
+  echo "$1" | tr '[:upper:]' '[:lower:]'
+}
+
+to_bool() {
+  [[ "$1" == "1" || "$1" == "ON" || "$1" == "YES" || "$1" == "TRUE" || "$1" == "T" ]] && echo 1 && return 0
+  [[ "$1" == "0" || "$1" == "OFF" || "$1" == "NO" || "$1" == "FALSE" || "$1" == "F" ]] && echo 0 && return 0
+  # Error case - value unknown
+  exit 1
+}
+
+check_bool() {
+  local v="$1"
+  local result
+  result=$(to_bool "${!v}" ) || { echo "${v} has invalid boolean value: ${!v}"; exit 1; }
+}
+
+validate_build_variables() {
+  # Check general default variables
+  if [[ -z ${BASE+x} ]] || [[ -z "${BASE}" ]]; then
+    echo "BASE not set. - BASE directory defines target where every component should be installed"
+    exit 1
+  fi
+}
+
+validate_component() {
+  local component="$1"
+  local c_type="$2"
+
+  local component_path="$DIR/${c_type}-${component}.inc"
+  if [[ ! -f "${component_path}" ]]; then
+    echo "Component ${component} not found."
+    return 1
+  fi
+}
+
+load_component() {
+  local component="$1"
+  local c_type="$2"
+
+  local component_path="$DIR/${c_type}-${component}.inc"
+  if [[ ! -f "${component_path}" ]]; then
+    echo "Component ${component} not found."
+    return 2 # File not found
+  fi
+  source "${component_path}" || { echo "Error in file ${component_path}"; return 1; }
+}
+
+
+check_docker_os() {
+  local docker_base=$1
+  local os_info=""
+  # start docker using the base image, link this directory and get the os information
+  os_info=$(docker run -v "${DIR}:/tmp" "${docker_base}" /tmp/build.sh --check-os) || { echo "Docker execution failed: $os_info"; exit 1;}
+
+  local line
+  while read -r line; do
+  case $line in
+    OS=*)
+    OS="${line#*=}"
+    ;;
+    DISTRIBUTION=*)
+      DISTRIBUTION="${line#*=}"
+    ;;
+    DISTRIBUTION_VER=*)
+      DISTRIBUTION_VER="${line#*=}"
+    ;;
+  esac
+  done <<< "$os_info"
+
+  echo "Docker OS=${OS}"
+  echo "Docker DISTRIBUTION=${DISTRIBUTION}"
+  echo "Docker DISTRIBUTION_VER=${DISTRIBUTION_VER}"
+}
+
+
+build_docker() {
+  local component=$1
+  local is_dependency=$2
+  
+  load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; }
+
+  # Extract repository, image, tag from base image
+  local base_repository="${BASE_IMAGE%/*}"
+  [[ "${base_repository}" == "${BASE_IMAGE}" ]] && base_repository="" # No base repository provided
+  local base_image="${BASE_IMAGE##*/}"
+  local base_tag="${base_image##*:}"
+  if [[ "${base_tag}" == "${base_image}" ]]; then
+    base_tag="" # No tag provided
+  else
+    base_image="${base_image%:*}"
+  fi
+
+  local BASE="/tmp"
+
+  # Check all input variables
+  validate_required_variables "${component}" "required_variables"
+
+  # Get the list of build dependencies and check them
+  local depending_artifact_components=("")
+  check_list artifact_dependency_"${component}"
+  mapfile -t depending_artifact_components <<< "$(get_list artifact_dependency_"${component}")"
+  local v
+  for v in "${depending_artifact_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    { build_docker "${v}" 1; } || { echo "Not all compile dependencies are available: ${v}"; return 1; }
+  done
+
+  # Get the list of runtime dependencies
+  local depending_runtime_artifact_components=("")
+  mapfile -t depending_runtime_artifact_components <<< "$(get_list runtime_artifact_dependency_"${component}")"
+  local v
+  for v in "${depending_runtime_artifact_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    { build_docker "${v}" 1;} || { echo "Not all runtime dependencies are available: ${v}"; return 1; }
+  done
+
+  echo "Build component: ${component}"
+
+  # Setup general component variables
+  gather_dependencies "${component}" "artifact" "setup_variables"
+
+  # Get the docker image id if available
+  local config_id=""
+  config_id=$(execution_action "get_docker_config_id" "${component}")
+  res="$?"
+  [[ "$res" -eq 1 ]] && echo "Building docker dependency ${component} failed: get_docker_config_id_${component}" && return 1
+
+  # An empty config id indicates nothing to build
+  [[ -z "${config_id}" ]] && return 0
+
+  # Use the config id to find a pre-build docker image
+  local target_image="${component}:${config_id}_${base_image}_${base_tag}"
+  [[ -z $(docker images -q "${REPOSITORY}/${target_image}") ]] || { echo "Docker image exists: ${REPOSITORY}/${target_image}"; return 0; }
+  docker pull "${REPOSITORY}/${target_image}" || /bin/true
+  [[ -z $(docker images -q "${REPOSITORY}/${target_image}") ]] || { echo "Docker image exists: ${REPOSITORY}/${target_image}"; return 0; }
+
+  # Gather all indirect depending components
+  local all_depending_artifact_components=("")
+  mapfile -t all_depending_artifact_components <<< "$(get_all_dependencies "${component}" "artifact")"
+
+  local all_depending_runtime_artifact_components=("")
+  mapfile -t all_depending_runtime_artifact_components <<< "$(get_all_dependencies "${component}" "runtime_artifact")"
+
+  local docker_dependencies=("")
+  docker_dependencies+=("${all_depending_artifact_components[@]}")
+
+  for c in "${depending_runtime_artifact_components[@]}"; do
+    local found=0
+    for i in "${docker_dependencies[@]}"; do
+      [[ -z "$i" ]] && continue
+      [[ "$i" == "$c" ]] && found=1 && break
+    done
+
+    # Attach item if new
+    [[ "$found" -eq 0 ]] && docker_dependencies+=("$c")
+  done
+
+  # Start to build image
+  local temp_dir
+  temp_dir="$(mktemp -d)"
+  [[ -d "${temp_dir}" ]] || (echo "Could not create temp_dir"; exit 1)
+
+  local docker_context=""
+  docker_context=$(execution_action "get_docker_context" "${component}") || docker_context=""
+
+  local docker_container_context=""
+  docker_container_context=$(execution_action "get_docker_container_context" "${component}") || docker_container_context=""
+  
+  # Prepare Dockerfile
+  local dockerfile="${temp_dir}/Dockerfile"
+
+  {
+    # Add all depending images as layers
+    for v in "${docker_dependencies[@]}"; do
+      [[ -z "${v}" ]] && continue
+      local dep_config_id
+      dep_config_id=$(execution_action "get_docker_config_id" "${v}") || true
+      # An empty config id indicates nothing to build
+      [[ -z "${dep_config_id}" ]] && continue
+
+      echo "FROM ${REPOSITORY}/${v}:${dep_config_id}_${base_image}_${base_tag} as ${v}_base"
+    done
+
+    # If multiple source images are available use the first one as a base image
+    local hasBaseImage=0
+    for v in "${all_depending_artifact_components[@]}"; do
+      [[ -z "${v}" ]] && continue
+      dep_config_id=$(execution_action "get_docker_config_id" "${v}") || true
+
+      # An empty config id indicates nothing to build
+      [[ -z "${dep_config_id}" ]] && continue
+      
+      if [[ "${hasBaseImage}" -eq 0 ]]; then
+        hasBaseImage=1
+        # Use base image as building base
+        echo "FROM ${v}_base as intermediate"
+      else
+        # Copy artifacts
+        # TODO: maybe get list of specific directories to copys
+        echo "COPY --from=${v}_base ${BASE} ${BASE}/"
+      fi
+    done
+
+    if [[ "${hasBaseImage}" -eq 0 ]]; then
+      hasBaseImage=1
+      # Use base image as building base
+      echo "FROM ${BASE_IMAGE} as intermediate"
+    fi
+
+    # Retrieve list of required variables and make them available in Docker
+    local docker_vars=[]
+    mapfile -t docker_vars <<< "$(get_list required_variables_"$component")"
+    docker_vars+=("BASE")
+    for v in "${all_depending_artifact_components[@]}"; do
+      [[ -z "${v}" ]] && continue
+      local dep_docker_vars=()
+      mapfile -t dep_docker_vars <<< "$(get_list required_variables_"${v}")"
+      docker_vars+=("${dep_docker_vars[@]}")
+    done
+
+    # Export docker variables explicitly
+    for d_v in "${docker_vars[@]}"; do
+      [[ -z "${d_v}" ]] && continue
+      local d_v_value
+      d_v_value=${!d_v}
+      echo "ENV ${d_v}=${d_v_value}"
+    done
+
+    # Run the build script
+    if [[ -z "${docker_context}" ]]; then
+      # Copy content from the temporary directory to the docker image
+      echo "COPY . ."
+      echo "RUN ./build.sh --debug --install-system-deps ${component}"
+    else
+      echo "COPY . ${docker_container_context}"
+      # TODO: this is quite specific to this script: should use common value
+      echo "RUN ${docker_container_context}/scripts/build/build.sh --debug --install-system-deps ${component}"
+    fi
+
+    # Copy all the build artifacts to the final image: build artifact is the full path
+    # and will be the same in the destination docker image
+    if [[ "${is_dependency}" -eq 1 || "${CREATE_FINAL_IMAGE}" -eq 0 ]]; then
+      echo "FROM ${BASE_IMAGE} as final"
+      local build_artifacts
+      mapfile -t build_artifacts <<< "$(execution_action "get_build_artifacts" "${component}")"
+      for artifact in "${build_artifacts[@]}"; do
+        [[ -z "${artifact}" ]] && continue
+        echo "COPY --from=intermediate ${artifact} ${artifact}"
+      done
+    
+      # Copy all the runtime dependencies
+      for dep_component in "${all_depending_runtime_artifact_components[@]}"; do
+        [[ -z "${dep_component}" ]] && continue
+        local build_artifacts
+        mapfile -t build_artifacts <<< "$(execution_action "get_build_artifacts" "${dep_component}")"
+        for artifact in "${build_artifacts[@]}"; do
+          [[ -z "${artifact}" ]] && continue
+          echo "COPY --from=intermediate ${artifact} ${artifact}"
+        done
+      done
+    fi
+    # TODO Add description labels
+    echo "LABEL maintainer=\"KLEE Developers\""
+  } >> "${dockerfile}"
+
+  # Append template file if exists
+  docker_template_files=(
+      "${DIR}/d-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc"
+      "${DIR}/d-${component}-${OS}-${DISTRIBUTION}.inc"
+      "${DIR}/d-${component}-${OS}.inc"
+      "${DIR}/d-${component}.inc"
+    )
+  for f in "${docker_template_files[@]}"; do
+     [[ ! -f "$f" ]] && continue
+     cat "$f" >> "${dockerfile}"
+     break
+  done
+
+  # Copy docker context and dependencies
+  shopt -s nullglob # allow nullglobing
+  echo "${all_depending_artifact_components[@]}"
+  for v in "${all_depending_artifact_components[@]}" "${component}"; do
+    [[ -z "${v}" ]] && continue
+    local files=(
+      "${DIR}/"*"-${v}.inc" \
+      "${DIR}/"*"-${v}-${OS}.inc" \
+      "${DIR}/"*"-${v}-${OS}-${DISTRIBUTION}.inc" \
+      "${DIR}/"*"-${v}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" \
+      "${DIR}/build.sh" \
+      "${DIR}/common-functions"
+    )
+    local f
+    for f in  "${files[@]}"; do
+      [ -f "$f" ] || continue
+      cp -r "$f" "${temp_dir}/"
+    done
+
+    mkdir -p "${temp_dir}/patches"
+    for f in "${DIR}/patches/${v}"*.patch; do
+      cp -r "$f" "${temp_dir}/patches/"
+    done
+  done
+  shopt -u nullglob # disallow nullglobing
+
+  if [[ -z "${docker_context}" ]]; then
+    docker_context="${temp_dir}"
+  fi
+
+  # Build Docker container
+  docker build -t "${REPOSITORY}/${target_image}" -f "${temp_dir}"/Dockerfile "${docker_context}" || return 1
+  if [[ "${PUSH_DOCKER_DEPS}" -eq 1 && "${is_dependency}" -eq 1 ]]; then
+    docker push "${REPOSITORY}/${target_image}" || /usr/bin/true
+  fi
+
+  if [[ "${KEEP_DOCKERFILE}" -eq 0 ]]; then
+    # Clean-up docker build directory
+    rm -rf "${temp_dir}"
+  else
+    echo "Preserved docker directory: ${temp_dir}"
+  fi
+}
+
+check_os() {
+  if [[ "$OSTYPE" == "linux-gnu" ]]; then
+    # Host is Linux
+    OS="linux"
+    DISTRIBUTION="$(grep ^ID= /etc/os-release)"
+    DISTRIBUTION=${DISTRIBUTION#"ID="}
+    DISTRIBUTION_VER="$(grep ^VERSION_ID= /etc/os-release || echo "")"
+    DISTRIBUTION_VER=${DISTRIBUTION_VER#"VERSION_ID="}
+    # Remove `"`, if exists
+    DISTRIBUTION_VER=${DISTRIBUTION_VER#\"}
+    DISTRIBUTION_VER=${DISTRIBUTION_VER%\"}
+
+  elif [[ "$OSTYPE" == "darwin"* ]]; then
+    # Host is Mac OS X
+    OS="osx"
+    DISTRIBUTION="$(sw_vers -productName)"
+    DISTRIBUTION_VER="$(sw_vers -productVersion)"
+  else
+    echo "Operating System unknown $OSTYPE"
+    exit 1
+  fi
+  echo "Detected OS: ${OS}"
+  echo "OS=${OS}"
+  echo "Detected distribution: ${DISTRIBUTION}"
+  echo "DISTRIBUTION=${DISTRIBUTION}"
+  echo "Detected version: ${DISTRIBUTION_VER}"
+  echo "DISTRIBUTION_VER=${DISTRIBUTION_VER}"
+}
+
+
+#
+try_execute() {
+  # Check if a function exists and execute it
+  fct=$1
+  # promote that function does not exist
+  [[ "$(type -t "${fct}")" != "function" ]] && return 2
+
+  # promote the return value of the function
+  local failed=0
+  "${fct}" || failed=1
+  return "${failed}"
+}
+
+try_execute_if_exists() {
+  # Check if a function exists and execute it
+  fct=$1
+  # Ignore if function does not exist
+  [[ "$(type -t "${fct}")" != "function" ]] && return 0
+
+  # promote the return value of the function
+  local failed=0
+  "${fct}" || failed=1
+  return "${failed}"
+}
+
+# Execute the most system specific action possible.
+# If an action executed successfuly, return 0
+# The function will return 1 if an action was not successful
+execution_action() {
+    local action="$1"
+    local component="$2"
+    local found=0
+
+    # Execute most specific action: os + distribution + distribution version
+    if [[ -f "${DIR}/p-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc" ]]; then
+        found=1
+        source "${DIR}/p-${component}-${OS}-${DISTRIBUTION}-${DISTRIBUTION_VER}.inc"
+        local failed=0
+        try_execute "${action}"_"${component}" || failed=1
+        [[ "$failed" -eq 0 ]] && return 0
+    fi
+
+    # Execute most specific action: os + distribution
+    if [[ -f "${DIR}/p-${component}-${OS}-${DISTRIBUTION}.inc" ]]; then
+        found=1
+        source "${DIR}/p-${component}-${OS}-${DISTRIBUTION}.inc"
+        local failed=0
+        try_execute "${action}"_"${component}" || failed=1
+        [[ "$failed" -eq 0 ]] && return 0
+    fi
+
+    # Execute most specific action: os
+    if [[ -f "${DIR}/p-${component}-${OS}.inc" ]]; then
+        found=1
+        source "${DIR}/p-${component}-${OS}.inc";
+        local failed=0
+        try_execute "${action}"_"${component}" || failed=1
+        [[ "$failed" -eq 0 ]] && return 0
+    fi
+
+    # Execute package specific action:
+    if [[ -f "${DIR}/p-${component}.inc" ]]; then
+        found=1
+        source "${DIR}/p-${component}.inc";
+        local failed=0
+        try_execute "${action}"_"${component}" || failed=1
+        [[ "$failed" -eq 0 ]] && return 0
+    fi
+
+    # Found an action file but something didn't work
+    [[ "${found}" -eq 1 ]] && return 1
+
+    # No action found
+    return 2
+}
+
+##
+# Returns a list that is the result of either an array or function call
+get_list(){
+  local list_name=$1
+  local result=("")
+
+  if [[ "$(type -t "${list_name}")" == "function" ]]; then
+    mapfile -t result <<< "$("${list_name}")"
+  elif [[ -n ${!list_name+x} ]]; then
+    list_array="${list_name}[@]"
+    result=("${!list_array}")
+  fi
+
+  for i in "${result[@]}"; do
+    [[ -z "${i}" ]] && continue
+    echo "${i}"
+  done
+
+  return 0
+}
+
+##
+# Check if a lists exist
+##
+check_list(){
+  local list_name=$1
+  if [[ "$(type -t "${list_name}")" == "function" ]]; then
+    return 0
+  fi
+  local list_array="${list_name}[@]"
+  if [[ ${!list_array+x} ]]; then
+    return 0
+  fi
+  echo "Variable or function \"${list_name}\" not found"
+  exit 1
+}
+
+validate_required_variables() {
+    local component="$1"
+    local type="$2"
+    local variables
+    check_list required_variables_"${component}"
+    mapfile -t variables <<< "$(get_list "${type}"_"${component}")"
+
+    if [[ -n "${variables[*]}" ]]; then
+        # Check if variables are defined
+        for v in "${variables[@]}"; do
+            if [[ -z ${!v+x} ]]; then
+                echo "${v} Required but unset"
+                exit 1
+            fi
+        done
+    fi
+
+    try_execute_if_exists required_variables_check_"${component}"
+}
+
+get_all_dependencies_rec() {
+  local component="$1"
+  local type="$2"
+  local depending_components
+  # Get the list of dependencies
+  mapfile -t depending_components <<< "$(get_list "${type}"_dependency_"${component}")"
+  for v in "${depending_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    get_all_dependencies_rec "$v" "$type"
+  done
+  echo "$component"
+}
+
+get_all_dependencies() {
+  local component="$1"
+  local type="$2"
+  local depending_components=("")
+  # Get the list of dependencies
+  mapfile -t depending_components <<< "$(get_list "${type}"_dependency_"${component}")"
+  local final_list=("${depending_components[@]}")
+  for v in "${depending_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    local deps_list=("")
+    local failed=0
+    mapfile -t deps_list <<< "$(get_all_dependencies_rec "$v" "$type")"
+    [[ "${failed}" -eq 1 ]] && continue
+
+    # Make sure items are unique and keep the order of occurence
+    for di in "${deps_list[@]}"; do
+      local found=0
+      for f in "${final_list[@]}"; do
+        [[ -z "$f" ]] && continue
+        [[ "$di" == "$f" ]] && found=1 && break
+      done
+      [[ "$found" -eq 0 ]] && final_list+=("${di}")
+    done
+  done
+
+  for v in "${final_list[@]}"; do
+    echo "${v}"
+  done
+}
+
+gather_dependencies_rec() {
+  local component="$1"
+  local type="$2"
+  local action="$3"
+
+  load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; }
+  validate_required_variables "${component}" "required_variables"
+
+  # Get the list of dependencies
+  local variables
+  check_list "${type}"_dependency_"${component}"
+  mapfile -t variables <<< "$(get_list "${type}"_dependency_"${component}")"
+  for v in "${variables[@]}"; do
+    [[ -z "${v}" ]] && continue
+    gather_dependencies_rec "$v" "${type}" "${action}"
+  done
+
+  try_execute_if_exists "${action}"_"${component}"
+}
+
+gather_dependencies() {
+  local component="$1"
+  local dependency_type="$2"
+  local action="$3"
+
+  local depending_components
+  # Get the list of dependencies
+  check_list "${dependency_type}"_dependency_"${component}"
+  mapfile -t depending_components <<< "$(get_list "${dependency_type}"_dependency_"${component}")"
+
+  for v in "${depending_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    gather_dependencies_rec "$v" "${dependency_type}" "${action}"
+  done
+  try_execute_if_exists "${action}"_"${component}"
+}
+
+check_module() {
+  local module="$1"
+  # Validate module if different functions or arrays exist
+  (
+    load_component "${module}" "v" || return 1
+    list_or_functions=(
+      required_variables
+      artifact_dependency
+    )
+    for item in "${list_or_functions[@]}"; do
+      check_list "${item}_${module}"
+    done
+
+  ) || { echo "Module $1 not valid"; return 1; }
+
+  # Validate build instructions
+  (
+    validate_component "${module}" "p" || { echo "No build instructions found for ${module}"; return 0; }
+    load_component "${module}" "p"
+
+    list_or_functions=(
+      setup_build_variables
+      download
+      build
+      install
+      is_installed
+      setup_artifact_variables
+      get_build_artifacts
+      get_docker_config_id
+    )
+    for item in "${list_or_functions[@]}"; do
+      check_list "${item}_${module}"
+    done
+
+  ) || { echo "Build instructions for ${module} are not valid"; return 1; }
+
+}
+
+##
+## Install the specified component
+install_component() {
+  local component="$1"
+
+  # Load general component information
+  load_component "${component}" "v" || { echo "Loading component failed ${component}"; return 1; }
+
+  # Get the list of dependencies
+  local depending_artifact_components
+  check_list artifact_dependency_"${component}"
+  mapfile -t depending_artifact_components <<< "$(get_list artifact_dependency_"${component}")"
+
+  # Make sure an artefact is available for the depending component
+  for v in "${depending_artifact_components[@]}"; do
+    [[ -z "${v}" ]] && continue
+    install_component "${v}"
+  done
+
+  # Setup general component variables
+  validate_required_variables "${component}" "required_variables"
+
+  # Handle dependencies of required artifacts
+  gather_dependencies "${component}" "artifact" "setup_variables"
+
+  # Check if the artifact is installed ablready
+  execution_action is_installed "${component}" && execution_action setup_artifact_variables "${component}" && validate_required_variables "${component}"  "export_variables" && { echo "Already installed ${component}"; return 0; }
+
+  # Install package if available
+  execution_action install_binary_artifact "${component}" && execution_action setup_artifact_variables "${component}" && validate_required_variables "${component}"  "export_variables" && { echo "Package installed ${component}"; return 0 ;}
+
+  # Validate general build variables
+  validate_build_variables
+
+  # Check if there is build information, if not - this is a meta package, return
+  validate_component "${component}" "p" || return 0
+
+  # Load build description
+  load_component "${component}" "p" || { echo "Loading component failed ${component}"; return 1; }
+
+  # Setup build variables
+  setup_build_variables_"${component}"
+
+  # Check and install runtime-dependencies if needed
+  execution_action "install_runtime_dependencies" "${component}" || true
+
+  # Validate configuration
+  try_execute_if_exists validate_build_config_"${component}"
+
+  # Install build dependencies
+  if [[ "${INSTALL_SYSTEM_DEPS}" == "1" ]]; then
+    execution_action "install_build_dependencies" "${component}" || {
+      echo "Could not install build dependencies for ${component}";
+      return 1;
+    }
+  fi
+
+  # Install build source
+  try_execute_if_exists download_"${component}"
+
+  # Build the package
+  try_execute_if_exists build_"${component}"
+
+  # Install to its final destination
+  try_execute_if_exists install_"${component}"
+}
+
+
+main() {
+  local NAME
+  NAME=$(basename "${0}")
+  local USAGE="usage: ${NAME} "
+  local COMPONENTS=()
+  local BUILD_DOCKER=0
+  local INSTALL_SYSTEM_DEPS=0
+  local KEEP_DOCKERFILE=0
+  local CHECK_MODULE=0
+  local PUSH_DOCKER_DEPS=0
+  local CREATE_FINAL_IMAGE=0
+
+  for i in "$@" ;do
+  case $i in
+    --debug)
+      set -x
+    ;;
+    --docker)
+    BUILD_DOCKER=1
+    ;;
+    --keep-dockerfile)
+      KEEP_DOCKERFILE=1
+    ;;
+    --push-docker-deps)
+      PUSH_DOCKER_DEPS=1
+    ;;
+    --create-final-image)
+      CREATE_FINAL_IMAGE=1
+    ;;
+    --install-system-deps)
+      INSTALL_SYSTEM_DEPS=1
+    ;;
+    --help)
+      show_help "${NAME}"
+      exit 0
+    ;;
+    --check-os)
+      # Checks the operating sytem used
+      check_os
+      exit 0
+    ;;
+    --check-module)
+      # Check the validity of the module
+      CHECK_MODULE=1
+    ;;
+    -*)
+      echo "${NAME}: unknown argument: $i"
+      show_help "${NAME}"
+      exit 1
+    ;;
+    *)
+      COMPONENTS+=("$i")
+    ;;
+  esac
+  done
+
+  if [[ ${#COMPONENTS[@]} -eq 0 ]]; then
+    show_help "${NAME}"
+    exit 1
+  fi
+
+
+  if [[ "${CHECK_MODULE}" -eq 1 ]]; then
+    for m in "${COMPONENTS[@]}"; do
+      check_module "${m}"
+    done
+    exit 0
+  fi
+
+  # Validate selected components: check if they have a v-"component".inc file
+  for c in "${COMPONENTS[@]}"; do
+    validate_component "$c" "v"
+  done
+
+  if [[ "${BUILD_DOCKER}" == "1" ]]; then
+    if [[ -z ${BASE_IMAGE+X} ]]; then
+      echo "No BASE_IMAGE provided"
+      exit 1
+    fi
+    if [[ -z ${REPOSITORY+X} ]]; then
+      echo "No REPOSITORY provided"
+      exit 1
+    fi
+    
+    # Gather information about the base image
+    check_docker_os "${BASE_IMAGE}"
+
+    # Install components
+    for c in "${COMPONENTS[@]}"; do
+      build_docker "$c" 0 || { echo "Building docker image ${c} failed"; return 1; }
+    done
+  else
+    # General Setup
+    check_os
+
+    # Install components
+    for c in "${COMPONENTS[@]}"; do
+      install_component "$c"
+      try_execute_if_exists check_export_variables_"$c"
+    done
+  fi
+}
+
+main "$@"
diff --git a/scripts/build/common-defaults.sh b/scripts/build/common-defaults.sh
deleted file mode 100644
index 5cefef19..00000000
--- a/scripts/build/common-defaults.sh
+++ /dev/null
@@ -1,53 +0,0 @@
-# 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
index 499b51b7..6d810d73 100644
--- a/scripts/build/common-functions
+++ b/scripts/build/common-functions
@@ -16,203 +16,18 @@ function git_clone_or_update() {
   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_VERSION_MAJOR="${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"
+function get_git_hash() {
+  local url="$1"
+  local branch="$2"
+  local commit_id=""
+  
+  # List remote git branches and get the commit id of the branch
+  commit_id="$(git ls-remote -h "$url" |grep "$branch" | cut -d$'\t' -f 1)"
+  
+  # If that doesn't work use the branch instead of the commit id
+  if [[ -z "${commit_id}" ]]; then 
+    echo "${branch}"
   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
+    echo "${commit_id:0:7}"
   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
+}
\ No newline at end of file
diff --git a/scripts/build/d-klee-linux-ubuntu.inc b/scripts/build/d-klee-linux-ubuntu.inc
new file mode 100644
index 00000000..38b8dce5
--- /dev/null
+++ b/scripts/build/d-klee-linux-ubuntu.inc
@@ -0,0 +1,23 @@
+# TODO remove adding sudo package
+# Create ``klee`` user for container with password ``klee``.
+# and give it password-less sudo access (temporarily so we can use the TravisCI scripts)
+RUN apt update && apt -y --no-install-recommends install sudo && \
+    rm -rf /var/lib/apt/lists/* && \
+    useradd -m klee && \
+    echo klee:klee | chpasswd && \
+    cp /etc/sudoers /etc/sudoers.bak && \
+    echo 'klee  ALL=(root) NOPASSWD: ALL' >> /etc/sudoers
+
+ENV BASE=/tmp
+# Copy across source files needed for build
+# Set klee user to be owner
+ADD --chown=klee:klee / ${BASE}/klee_src
+
+USER klee
+WORKDIR /home/klee
+
+# Add KLEE binary directory to PATH
+RUN /bin/bash -c 'ln -s ${BASE}/klee_src /home/klee/ && ln -s ${BASE}/klee_build* /home/klee/klee_build && echo "export PATH=\"$PATH:$(cd /tmp/llvm-*install*/bin && pwd):/home/klee/klee_build/bin\"" >> /home/klee/.bashrc'
+
+# TODO Remove when STP is fixed
+RUN /bin/bash -c 'echo "export LD_LIBRARY_PATH=$(cd ${BASE}/metaSMT-*-deps/stp-git-basic/lib/ && pwd)" >> /home/klee/.bashrc'
diff --git a/scripts/build/dependencies-ubuntu.sh b/scripts/build/dependencies-ubuntu.sh
deleted file mode 100755
index d5d4a36a..00000000
--- a/scripts/build/dependencies-ubuntu.sh
+++ /dev/null
@@ -1,43 +0,0 @@
-#!/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 \
-  curl \
-  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==0.6.0
diff --git a/scripts/build/install-klee-deps.sh b/scripts/build/install-klee-deps.sh
deleted file mode 100755
index 622e621f..00000000
--- a/scripts/build/install-klee-deps.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/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
deleted file mode 100755
index 50dfb612..00000000
--- a/scripts/build/install-local.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/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/scripts/build/klee.sh b/scripts/build/klee.sh
deleted file mode 100755
index 84d7bd63..00000000
--- a/scripts/build/klee.sh
+++ /dev/null
@@ -1,219 +0,0 @@
-#!/bin/bash -x
-# Compile KLEE
-# Make sure we exit if there is a failure
-set -e
-
-DIR="$(cd "$(dirname "$0")" && pwd)"
-source "${DIR}/common-defaults.sh"
-
-: ${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=""
-###############################################################################
-# Handling LLVM configuration
-###############################################################################
-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
-  LLVM_BIN="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin"
-  LLVM_CONFIG="${LLVM_BIN}/llvm-config"
-  LLVM_BUILD_DIR="$(${LLVM_CONFIG} --src-root)"
-  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
-    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)
-fi
-
-COVERAGE_FLAGS=""
-if [ ${COVERAGE} -eq 1 ]; then
-    COVERAGE_FLAGS='-fprofile-arcs -ftest-coverage'
-fi
-
-
-###############################################################################
-# Handle setting up solver configure flags for KLEE
-###############################################################################
-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)
-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="${BASE}/stp-${STP_VERSION}-install")
-    ;;
-  Z3)
-    echo "Z3"
-    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="${BASE}/metaSMT/build" -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}")
-    ;;
-  *)
-    echo "Unknown solver ${solver}"
-    exit 1
-  esac
-done
-
-###############################################################################
-# Handle additional configure flags
-###############################################################################
-
-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
-###############################################################################
-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
-  KLEE_ASSERTS_OPTION="-DENABLE_KLEE_ASSERTS=TRUE"
-fi
-
-if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
-  CMAKE_BUILD_TYPE="RelWithDebInfo"
-else
-  CMAKE_BUILD_TYPE="Debug"
-fi
-
-# TODO: We should support Ninja too
-# Configure KLEE
-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[@]} \
-  -DGTEST_SRC_DIR=${GTEST_SRC_DIR} \
-  -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} \
-  ${KLEE_ASSERTS_OPTION[@]} \
-  -DENABLE_UNIT_TESTS=TRUE \
-  -DENABLE_SYSTEM_TESTS=TRUE \
-  -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()
-{
-  tags=$1
-  codecov_suffix=(${tags// /})
-  # 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.${codecov_suffix}
-  # Debug info
-  lcov --rc lcov_branch_coverage=1 --list coverage_all.info.${codecov_suffix}
-}
-
-COVERAGE=${COVERAGE:=0}
-
-###############################################################################
-# Unit tests
-###############################################################################
-# Prepare coverage information if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverage_setup
-fi
-make unittests
-
-# Generate and upload coverage if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverageup "unittests"
-fi
-
-###############################################################################
-# lit tests
-###############################################################################
-if [ ${COVERAGE} -eq 1 ]; then
-  coverage_setup
-fi
-make systemtests
-
-# If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
-if [ "X${SOLVERS}" == "XmetaSMT" ]; then
-  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
-      if [ "$backend" == "cvc4" ]; then
-        for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done &
-      fi
-      lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/
-    fi
-  done
-fi
-
-# Generate and upload coverage if COVERAGE is set
-if [ ${COVERAGE} -eq 1 ]; then
-  coverageup "systemtests"
-fi
diff --git a/scripts/build/llvm.sh b/scripts/build/llvm.sh
deleted file mode 100755
index 92370159..00000000
--- a/scripts/build/llvm.sh
+++ /dev/null
@@ -1,193 +0,0 @@
-#!/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 "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" ]; then
-     cd "${LLVM_BASE}"
-     patch -p0 -i "${DIR}/patches/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
-  # Use the brew provided package
-  brew install "llvm\@${LLVM_VERSION_MAJOR}"
-else
-  echo "Unhandled TRAVIS_OS_NAME \"${TRAVIS_OS_NAME}\""
-  exit 1
-fi
diff --git a/scripts/build/p-clang-linux-ubuntu-16.04.inc b/scripts/build/p-clang-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..75023628
--- /dev/null
+++ b/scripts/build/p-clang-linux-ubuntu-16.04.inc
@@ -0,0 +1,66 @@
+install_binary_artifact_clang() {
+  local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}"
+
+  # Check versions: no support for LLVM < 3.5
+  [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]] && [[ "${LLVM_VERSION_MINOR}" -lt 5 ]] && return 1
+
+
+  local version=""
+  [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}"
+  [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}"
+
+
+  if [[ "${LLVM_VERSION_MAJOR}" -eq 3 && "${LLVM_VERSION_MINOR}" -gt 7 ]]; then
+    # Add certificate
+    apt update -y
+    dependencies=(
+      ca-certificates
+      wget
+    )
+
+    apt -y --no-install-recommends install "${dependencies[@]}"
+    wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add -
+
+    # Add repository
+    echo "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial${version} main" >> /etc/apt/sources.list
+  fi
+
+  apt update -y
+  dependencies=(
+    "llvm${version}"
+    "clang${version}"
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
+
+setup_artifact_variables_clang() {
+  local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}"
+  local version=""
+  [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}"
+  [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}"
+
+  # Only set LLVM_CONFIG if not set yet
+  if [[ -z ${LLVM_CONFIG+x} ]]; then
+    LLVM_CONFIG=$(which "llvm-config${version}")
+  fi
+
+  BITCODE_CC=$(which "clang${version}")
+  BITCODE_CXX=$(which "clang++${version}")
+
+  SANITIZER_C_COMPILER="${BITCODE_CC}"
+  SANITIZER_CXX_COMPILER="${BITCODE_CXX}"
+}
+
+# Check if the binary artifact is installed
+is_installed_clang() {
+    # Check if llvm-config with the right version exists    
+    which "llvm-config-${LLVM_VERSION}"
+}
+
+get_docker_config_id_clang() {
+  return 0
+}
diff --git a/scripts/build/p-clang-osx.inc b/scripts/build/p-clang-osx.inc
new file mode 100644
index 00000000..fde236ca
--- /dev/null
+++ b/scripts/build/p-clang-osx.inc
@@ -0,0 +1,13 @@
+# Package script for LLVM builds OSX
+install_binary_artifact_clang () {
+  # Use the brew provided package
+  LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  brew install "llvm\@${LLVM_VERSION_MAJOR}"
+}
+
+# Check if the binary artifact is installed
+is_installed_clang() {
+    # Check if llvm-config with the right version exists
+    LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+    [[ -f "/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]]
+}
diff --git a/scripts/build/p-gtest-linux-ubuntu-16.04.inc b/scripts/build/p-gtest-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..f636d321
--- /dev/null
+++ b/scripts/build/p-gtest-linux-ubuntu-16.04.inc
@@ -0,0 +1,12 @@
+install_build_dependencies_gtest() {
+  apt update -y
+
+  dependencies=(
+    ca-certificates
+    wget
+    unzip
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-gtest-osx.inc b/scripts/build/p-gtest-osx.inc
new file mode 100644
index 00000000..3fe48e06
--- /dev/null
+++ b/scripts/build/p-gtest-osx.inc
@@ -0,0 +1,5 @@
+install_build_dependencies_gtest() {
+  # Install essential dependency
+  # Ignore if already installed
+  brew install wget || /usr/bin/true
+}
diff --git a/scripts/build/p-gtest.inc b/scripts/build/p-gtest.inc
new file mode 100644
index 00000000..d4a2d498
--- /dev/null
+++ b/scripts/build/p-gtest.inc
@@ -0,0 +1,45 @@
+setup_build_variables_gtest() {
+  GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}"
+  return 0
+}
+
+download_gtest() {
+  cd "${BASE}" || exit 1
+  wget "https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip"
+  unzip -o "release-${GTEST_VERSION}.zip"
+  rm "release-${GTEST_VERSION}.zip"
+  touch "${GTEST_INSTALL_PATH}"/.is_installed
+}
+
+build_gtest() {
+  return 0
+}
+
+install_gtest() {
+  return 0
+}
+
+is_installed_gtest() {
+  (
+    setup_build_variables_gtest
+    [[ -f "${GTEST_INSTALL_PATH}"/.is_installed ]]
+  )
+}
+
+get_build_artifacts_gtest() {
+  (
+    setup_build_variables_gtest
+    echo "${GTEST_INSTALL_PATH}"
+  )
+}
+
+setup_artifact_variables_gtest() {
+  setup_build_variables_gtest
+}
+
+get_docker_config_id_gtest() {
+  (
+    setup_build_variables_gtest
+    echo "${GTEST_VERSION}"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-klee-linux-ubuntu-16.04.inc b/scripts/build/p-klee-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..b4ba3f33
--- /dev/null
+++ b/scripts/build/p-klee-linux-ubuntu-16.04.inc
@@ -0,0 +1,21 @@
+install_build_dependencies_klee() {
+  apt update -y
+
+  dependencies=(
+    build-essential
+    cmake
+    python-pip #for lit
+    python-setuptools #for lit
+    python-wheel #for lit
+    zlib1g-dev
+    python3
+  )
+
+  if [[ $(to_bool "${COVERAGE}") -eq 1 ]]; then
+    dependencies+=(lcov curl)
+  fi
+
+  apt -y --no-install-recommends install "${dependencies[@]}"
+
+  pip install lit
+}
\ No newline at end of file
diff --git a/scripts/build/build-travis.sh b/scripts/build/p-klee-osx.inc
index a2287a2e..2aa5c3e8 100755..100644
--- a/scripts/build/build-travis.sh
+++ b/scripts/build/p-klee-osx.inc
@@ -1,11 +1,5 @@
-#!/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 install ccache
+# Build dependencies
+install_build_dependencies_klee() {
   set +e
   brew upgrade python               # upgrade to Python 3
   brew install python@2             # install Python 2 (OSX version outdated + pip missing)
@@ -16,10 +10,5 @@ elif [[ "$TRAVIS_OS_NAME" == "osx" ]]; then
   ln -s "${py2path}" /usr/local/bin/python
   ln -s "${pip2path}" /usr/local/bin/pip
   set -e
-  pip install lit==0.6.0
-  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
+  pip install lit
+}
\ No newline at end of file
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc
new file mode 100644
index 00000000..a9982fc0
--- /dev/null
+++ b/scripts/build/p-klee.inc
@@ -0,0 +1,198 @@
+validate_build_config_klee() {
+  return 0
+}
+
+setup_build_variables_klee() {
+  KLEE_SUFFIX="${LLVM_VERSION_SHORT}${SOLVER_SUFFIX}${SANITIZER_SUFFIX}"
+  KLEE_BUILD_DIR="${BASE}/klee_build${KLEE_SUFFIX}"
+  KLEE_SRC="$DIR/../../"
+}
+
+download_klee() {
+  return 0
+}
+
+build_klee() {
+  CMAKE_PREFIX_PATH=("")
+
+  local CMAKE_ARGUMENTS=(
+    -DLLVM_DIR="${LLVM_INSTALL}"
+    -DLLVM_CONFIG_BINARY="${LLVM_CONFIG}"
+    -DLLVMCC="${BITCODE_CC}"
+    -DLLVMCXX="${BITCODE_CXX}"
+    -DGTEST_SRC_DIR="${GTEST_INSTALL_PATH}"
+    -DENABLE_UNIT_TESTS="TRUE"
+    -DENABLE_SYSTEM_TESTS="TRUE"
+    -DLIT_ARGS="-v"
+  )
+
+
+###############################################################################
+# klee-uclibc
+###############################################################################
+  local KLEE_UCLIBC_CONFIGURE_OPTION
+
+  if [ "${UCLIBC_VERSION}" != "0" ]; then
+    CMAKE_ARGUMENTS+=(
+      "-DENABLE_KLEE_UCLIBC=TRUE"
+      "-DKLEE_UCLIBC_PATH=${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}"
+      "-DENABLE_POSIX_RUNTIME=TRUE"
+    )
+  else
+    CMAKE_ARGUMENTS+=(
+      "-DENABLE_KLEE_UCLIBC=FALSE"
+      "-DENABLE_POSIX_RUNTIME=FALSE"
+    )
+  fi
+
+
+
+###############################################################################
+# Handle setting up solver configure flags for KLEE
+###############################################################################
+
+  local KLEE_Z3_CONFIGURE_OPTION=("-DENABLE_SOLVER_Z3=OFF")
+  local KLEE_STP_CONFIGURE_OPTION=("-DENABLE_SOLVER_STP=OFF")
+  local KLEE_METASMT_CONFIGURE_OPTION=("-DENABLE_SOLVER_METASMT=OFF")
+  
+  
+  for solver in "${SELECTED_SOLVERS[@]}"; do
+    echo "Setting CMake configuration option for ${solver}"
+    case "${solver}" in
+    stp)
+      KLEE_STP_CONFIGURE_OPTION=(
+        "-DENABLE_SOLVER_STP=TRUE"
+        "-DSTP_DIR=${STP_INSTALL_PATH}/"
+      )
+      CMAKE_PREFIX_PATH+=("${STP_INSTALL_PATH}")
+      ;;
+    z3)
+      echo "Z3"
+      KLEE_Z3_CONFIGURE_OPTION=(
+        "-DENABLE_SOLVER_Z3=TRUE"
+        "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include"
+        "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so"
+      )
+      ;;
+    metasmt)
+      echo "metaSMT"
+      if [ "X${METASMT_DEFAULT}" == "X" ]; then
+        METASMT_DEFAULT=STP
+      fi
+      KLEE_METASMT_CONFIGURE_OPTION=(
+        -DENABLE_SOLVER_METASMT=TRUE
+        -DmetaSMT_DIR="${METASMT_BUILD_PATH}"
+        -DMETASMT_DEFAULT_BACKEND="${METASMT_DEFAULT}"
+      )
+      ;;
+    *)
+      echo "Unknown solver ${solver}"
+      exit 1
+    esac
+  done
+  
+  CMAKE_ARGUMENTS+=(
+    "${KLEE_Z3_CONFIGURE_OPTION[@]}"
+    "${KLEE_STP_CONFIGURE_OPTION[@]}"
+    "${KLEE_METASMT_CONFIGURE_OPTION[@]}"
+  )
+
+###############################################################################
+# Handle additional configure flags
+###############################################################################
+
+  if [[ $(to_bool "${USE_TCMALLOC}") -eq 1 ]] ; then
+    CMAKE_PREFIX_PATH+=("${TCMALLOC_INSTALL_PATH}")
+    CMAKE_ARGUMENTS+=("-DENABLE_TCMALLOC=TRUE")
+  else
+    CMAKE_ARGUMENTS+=("-DENABLE_TCMALLOC=FALSE")
+  fi
+
+###############################################################################
+# KLEE
+###############################################################################
+
+  if [ "X${DISABLE_ASSERTIONS}" == "X1" ]; then
+    CMAKE_ARGUMENTS+=("-DENABLE_KLEE_ASSERTS=FALSE")
+  else
+    CMAKE_ARGUMENTS+=("-DENABLE_KLEE_ASSERTS=TRUE")
+  fi
+  
+  if [ "X${ENABLE_OPTIMIZED}" == "X1" ]; then
+    CMAKE_ARGUMENTS+=("-DCMAKE_BUILD_TYPE=RelWithDebInfo")
+  else
+    CMAKE_ARGUMENTS+=("-DCMAKE_BUILD_TYPE=Debug")
+  fi
+  
+# TODO: We should support Ninja too
+# Configure KLEE
+
+  local CXX_FLAGS=("")
+  local C_FLAGS=("")
+  local LD_FLAGS=("")
+  
+  if [ "${COVERAGE}" -eq 1 ]; then
+    CXX_FLAGS+=("-fprofile-arcs" "-ftest-coverage")
+    C_FLAGS+=("-fprofile-arcs" "-ftest-coverage")
+    LD_FLAGS+=("-fprofile-arcs" "-ftest-coverage")
+  fi
+
+  if [[ -n "${SANITIZER_BUILD}" ]]; then
+    C_FLAGS+=("${SANITIZER_C_FLAGS[@]}")
+    CXX_FLAGS+=("${SANITIZER_CXX_FLAGS[@]}")
+    LD_FLAGS+=("${SANITIZER_LD_FLAGS[@]}")
+
+    CMAKE_ARGUMENTS+=(
+      "-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}"
+      "-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}"
+    )
+  fi
+
+
+
+  mkdir -p "${KLEE_BUILD_DIR}" || return 1
+  cd "${KLEE_BUILD_DIR}"
+
+  {
+    echo "CXXFLAGS=\"${CXX_FLAGS[*]}\" \\"
+    echo "CFLAGS=\"${C_FLAGS[*]}\" \\"
+    echo "LDFLAGS=\"${LD_FLAGS[*]}\" \\"
+
+    if [[ -n "${CMAKE_PREFIX_PATH[*]}" ]]; then
+      cmake_concatenated=$(IFS=: ; echo "${CMAKE_PREFIX_PATH[*]}")
+      echo "CMAKE_PREFIX_PATH=\"${cmake_concatenated}\" \\"
+    fi
+
+    echo "cmake ${CMAKE_ARGUMENTS[*]} \"${KLEE_SRC}\""
+  } > "${KLEE_BUILD_DIR}/.build_command"
+
+  source "${KLEE_BUILD_DIR}/.build_command"
+  make -j$(nproc) || make || return 1
+}
+
+install_klee() {
+  return 0
+}
+
+get_docker_config_id_klee() {
+  (
+    setup_build_variables_klee
+    echo "${KLEE_SUFFIX}"
+  )
+}
+
+get_docker_context_klee() {
+  # KLEE's source code is two levels above this script
+  echo "${DIR}/../../"
+}
+
+get_docker_container_context_klee() {
+  echo "${BASE}/klee_src/"
+}
+
+get_build_artifacts_klee() {
+  (
+    setup_build_variables_klee
+    echo "${KLEE_BUILD_DIR}"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-llvm-linux-ubuntu-16.04.inc b/scripts/build/p-llvm-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..6bfc3105
--- /dev/null
+++ b/scripts/build/p-llvm-linux-ubuntu-16.04.inc
@@ -0,0 +1,98 @@
+# Build dependencies
+install_build_dependencies_llvm() { 
+  apt update -y
+
+  dependencies=(
+    build-essential
+    autoconf
+    automake
+    groff
+    gcc
+    g++
+    python-dev
+    make
+    subversion # To check out code
+    zlib1g-dev
+    cmake
+  )
+  
+  if [[ "${SANITIZERS[*]}" == "memory" ]]; then
+    dependencies+=(ninja-build)
+  fi
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
+
+install_binary_artifact_llvm() {
+  local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}")
+  local enable_debug=$(to_bool "${ENABLE_DEBUG}")
+  local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}")
+  local requires_rtti=$(to_bool "${REQUIRES_RTTI}")
+  local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}"
+
+
+  # No support for LLVM packages with debug information, incompatible if requested otherwise
+  [[ "${enable_debug}" -eq 1 ]] && return 1
+
+  # Packages are build with assertions disabled, incompatible if requested otherwise
+  [[ "${disable_assertions}" -eq 0 ]] && return 1
+
+  # Packages are build with RTTI enabled, incompatible if requested otherwise
+  [[ "${requires_rtti}" -eq 0 ]] && return 1
+
+  # Enable/Disable optimized does not matter
+  
+  # Check versions: no support for LLVM < 3.8
+  if [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]]; then
+    [[ "${LLVM_VERSION_MINOR}" -lt 8 ]] && return 1
+  fi
+  
+  # Add certificate
+  apt update -y
+  dependencies=(
+    ca-certificates
+    wget
+  )
+  apt -y --no-install-recommends install "${dependencies[@]}"
+  wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key| apt-key add -
+  
+  local version=""
+  [[ "${LLVM_VERSION_MAJOR}" -le 6 ]] && version="-${LLVM_VERSION}"
+  [[ "${LLVM_VERSION_MAJOR}" -ge 7 ]] && version="-${LLVM_VERSION_MAJOR}"
+  
+  # Add repository
+  echo "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial${version} main" >> /etc/apt/sources.list
+  apt update -y
+
+  dependencies=(
+    "llvm${version}"
+    "llvm${version}-dev"
+    "llvm${version}-runtime"
+    "clang${version}"
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
+
+# Check if the binary artifact is installed
+is_installed_llvm() {
+    local lc=""
+    # Check if llvm-config with the right version exists    
+    lc=$(which "llvm-config-${LLVM_VERSION}")
+    
+    [[ -z "${lc}" ]] && return 1
+
+    local rtti
+    rtti="$(${lc} --has-rtti)"
+    local assertion
+    assertion="$(${lc} --assertion-mode)"
+    local build_mode
+    build_mode="$(${lc} --build-mode)"
+
+    # Check requested mode with mode of the found item  
+    [[ $(to_bool "${REQUIRES_RTTI}") -eq $(to_bool "${rtti}") ]] || return 1
+    [[ $(to_bool "${DISABLE_ASSERTIONS}") -ne $(to_bool "${assertion}") ]] || return 1
+}
\ No newline at end of file
diff --git a/scripts/build/p-llvm-linux-ubuntu-18.04.inc b/scripts/build/p-llvm-linux-ubuntu-18.04.inc
new file mode 100644
index 00000000..f83112db
--- /dev/null
+++ b/scripts/build/p-llvm-linux-ubuntu-18.04.inc
@@ -0,0 +1,49 @@
+install_build_dependencies_llvm() { 
+	apt update -y
+
+	dependencies=(
+		build-essential
+
+		autoconf
+		automake
+		groff
+		gcc
+		g++
+		python-dev
+		make
+		subversion # Check out code
+		zlib1g-dev
+	)
+
+	#Install essential dependencies
+	apt -y --no-install-recommends install "${dependencies[@]}"
+}
+
+install_binary_artifact_llvm() {
+  apt update -y
+  
+  dependencies=(
+    "clang-${LLVM_VERSION}"
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
+
+# Check if the binary artifact is installed
+is_installed_llvm() {
+	local lc=""
+	# Check if llvm-config with the right version exists	
+	lc=$(which "llvm-config-${LLVM_VERSION}")
+	
+	local rtti
+	rtti="$(${lc} --has-rtti)"
+	local assertion
+	assertion="$(${lc} --assertion-mode)"
+	local build_mode
+	build_mode="$(${lc} --build-mode)"
+	
+	# Check requested mode with mode of the found item	
+	[[ $(to_bool "${REQUIRES_RTTI}") -eq $(to_bool "${rtti}") ]] || return 1
+	[[ $(to_bool "${DISABLE_ASSERTIONS}") -ne $(to_bool "${assertion}") ]] || return 1
+}
\ No newline at end of file
diff --git a/scripts/build/p-llvm-osx.inc b/scripts/build/p-llvm-osx.inc
new file mode 100644
index 00000000..05e423f3
--- /dev/null
+++ b/scripts/build/p-llvm-osx.inc
@@ -0,0 +1,21 @@
+# Package script for LLVM builds OSX
+install_binary_artifact_llvm () {
+  # Use the brew provided package
+  LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  brew install "llvm\@${LLVM_VERSION_MAJOR}"
+}
+
+# Check if the binary artifact is installed
+is_installed_llvm() {
+    # Check if llvm-config with the right version exists
+    LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+    [[ -f "/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]]
+}
+
+setup_artifact_variables_llvm() {
+  LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  LLVM_CONFIG="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config"
+  BITCODE_CC="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang"
+  BITCODE_CXX="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang++"
+  LLVM_INSTALL="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/"
+}
diff --git a/scripts/build/p-llvm.inc b/scripts/build/p-llvm.inc
new file mode 100644
index 00000000..4e0740a2
--- /dev/null
+++ b/scripts/build/p-llvm.inc
@@ -0,0 +1,366 @@
+validate_build_config_llvm() {
+    # Check variables that are needed for building 
+    [[ -n "${LLVM_SRC_BASE}" ]] || { echo "LLVM_SRC_BASE not set"; exit 1; }
+    [[ -n "${LLVM_VERSION_SHORT}" ]] || { echo "LLVM_VERSION_SHORT not set"; exit 1; }
+}
+
+setup_build_variables_llvm() {
+    LLVM_SUFFIX=""
+
+    local BuildMode=""
+    local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}")
+    local enable_debug=$(to_bool "${ENABLE_DEBUG}")
+    local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}")
+    local requires_rtti=$(to_bool "${REQUIRES_RTTI}")
+
+    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_SRC_BASE="${BASE}/llvm-${LLVM_VERSION_SHORT}"
+    LLVM_BUILD="${LLVM_SRC_BASE}-build${LLVM_SUFFIX}"
+    LLVM_INSTALL="${LLVM_SRC_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
+
+    LLVM_CONFIG="${LLVM_BIN}/llvm-config"
+    BITCODE_CC="${LLVM_BIN}/clang"
+    BITCODE_CXX="${LLVM_BIN}/clang++"
+
+
+    for sanitizer in "${SANITIZERS[@]}"; do
+      [[ -z "${sanitizer}" ]] && continue
+      # Undefined Behaviour Sanitizer
+      if [ "${sanitizer}" == "memory" ]; then
+        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[@]}")
+
+        # Use the uninstrumented compiler
+        BITCODE_CC="${SANITIZER_C_COMPILER}"
+        BITCODE_CXX="${SANITIZER_CXX_COMPILER}"
+        # But point to the instrumented llvm-config
+        LLVM_CONFIG="${LLVM_BIN}/llvm-config"
+        continue
+      fi
+      # Setup default sanitizer arguments
+      SANITIZER_C_COMPILER="${LLVM_BIN}/clang"
+      SANITIZER_CXX_COMPILER="${LLVM_BIN}/clang++"
+    done
+}
+
+download_llvm() {
+  # Skip step if we already checked out code
+  [[ -f "${LLVM_SRC_BASE}/.src_checked_out" ]] && return 0
+
+  # Checkout LLVM code
+  svn co "http://llvm.org/svn/llvm-project/llvm/branches/release_${LLVM_VERSION_SHORT}" "${LLVM_SRC_BASE}"
+  cd "${LLVM_SRC_BASE}/tools" || (echo "Directory does not exist"; exit 1)
+  svn co "http://llvm.org/svn/llvm-project/cfe/branches/release_${LLVM_VERSION_SHORT}" clang
+  cd "${LLVM_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1)
+  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_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1)
+    svn co "http://llvm.org/svn/llvm-project/libcxx/branches/release_${LLVM_VERSION_SHORT}" libcxx
+    cd "${LLVM_SRC_BASE}/projects" || (echo "Directory does not exist"; exit 1)
+    svn co "http://llvm.org/svn/llvm-project/libcxxabi/branches/release_${LLVM_VERSION_SHORT}" libcxxabi
+  fi
+
+  # Apply existing patches if needed
+  if [ -f "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch" ]; then
+     cd "${LLVM_SRC_BASE}" || (echo "Directory does not exist"; exit 1)
+     patch -p0 -i "${DIR}/patches/llvm${LLVM_VERSION_SHORT}.patch"
+  fi
+
+  touch "${LLVM_SRC_BASE}/.src_checked_out" 
+}
+
+build_llvm() {
+    local enable_optimized=$(to_bool "${ENABLE_OPTIMIZED}")
+    local enable_debug=$(to_bool "${ENABLE_DEBUG}")
+    local disable_assertions=$(to_bool "${DISABLE_ASSERTIONS}")
+    local requires_rtti=$(to_bool "${REQUIRES_RTTI}")
+
+    # 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 -p "${SANITIZER_LLVM_UNINSTRUMENTED}"
+       cd "${SANITIZER_LLVM_UNINSTRUMENTED}"
+       cmake -GNinja -DCMAKE_BUILD_TYPE=Release "${LLVM_SRC_BASE}"
+       ninja
+
+       # Build instrumented libc/libc++
+       mkdir -p "${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_SRC_BASE}"
+       ninja cxx cxxabi
+
+       # Build instrumented clang
+       mkdir -p "${LLVM_BUILD}"
+       cd "${LLVM_BUILD}"
+       C_F="${SANITIZER_C_FLAGS[*]}"
+       CXX_F="${SANITIZER_CXX_FLAGS[*]}"
+       LD_F="${SANITIZER_LD_FLAGS[*]}"
+       cmake -GNinja \
+          "${SANITIZER_CMAKE_C_COMPILER[*]}" \
+          "${SANITIZER_CMAKE_CXX_COMPILER[*]}" \
+          -DCMAKE_C_FLAGS="$C_F" \
+          -DCMAKE_CXX_FLAGS="${CXX_F}" \
+          -DCMAKE_BUILD_TYPE=RelWithDebInfo \
+          -DLLVM_ENABLE_ASSERTIONS=On \
+          -DLLVM_USE_SANITIZER=MemoryWithOrigins \
+          -DLLVM_ENABLE_LIBCXX=ON \
+          -DCMAKE_EXE_LINKER_FLAGS="${LD_F}" \
+          -DCMAKE_INSTALL_PREFIX="${LLVM_INSTALL}" \
+          "${LLVM_SRC_BASE}"
+      # Build clang as a dependency and install all needed packages
+      ninja clang
+      return 0
+    fi
+
+  # Configure; build; and install
+  mkdir -p "${LLVM_BUILD}"
+  cd "${LLVM_BUILD}"
+
+  # Skip building if already finished
+  [[ -e "${LLVM_BUILD}/.build_finished" ]] && return 0
+
+
+  # Configure LLVM
+  if [[ ${LLVM_VERSION_SHORT} -le 37 ]]; then
+    local 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
+
+    local variables=()
+    if [[ -n "${CC:-}" ]]; then
+        variables+=("CC=${CC}")
+    fi
+
+    if [[ -n "${CXX:-}" ]]; then
+        variables+=("CXX=${CXX}")
+    fi
+
+    if [[ -n "${LDFLAGS:-}" ]]; then
+        variables+=("LDFLAGS=${LLVM_LDFLAGS}")
+    fi
+
+    if [[ -n "${LLVM_CFLAGS:-}" ]]; then
+        variables+=("CFLAGS=${LLVM_CFLAGS}")
+    fi
+
+    if [[ -n "${LLVM_CXXFLAGS:-}" ]]; then
+        variables+=("CXXFLAGS=${LLVM_CXXFLAGS}")
+    fi
+
+    if [[ -n "${LLVM_LDFLAGS:-}" ]]; then
+        variables+=("LDFLAGS=${LLVM_LDFLAGS}")
+    fi
+    ${variables[@]+"${variables[@]}"} "${LLVM_SRC_BASE}/configure" "${CONFIG[@]}"
+
+  else
+    CONFIG=(
+        "-DCMAKE_INSTALL_PREFIX=${LLVM_INSTALL}"
+        "-LLVM_BUILD_LLVM_DYLIB=TRUE"
+    )
+    # 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 [[ -n "${LLVM_CFLAGS:-}" ]]; then
+      CONFIG+=("-DCMAKE_C_FLAGS=\"$LLVM_CFLAGS\"")
+    fi
+
+    if [[ -n "${LLVM_CXXFLAGS:-}" ]]; then
+      CONFIG+=("-DCMAKE_CXX_FLAGS=\"$LLVM_CXXFLAGS\"")
+    fi
+
+    if [[ "${requires_rtti}" -eq 1 ]]; then
+      CONFIG+=("-DLLVM_ENABLE_RTTI=TRUE")
+    fi
+
+    # Remove unneeded targets
+    CONFIG+=(
+       -DLLVM_INCLUDE_EXAMPLES=OFF
+#       -DLLVM_INCLUDE_TESTS=OFF
+#       -DCLANG_INCLUDE_TESTS=OFF
+       -DLLVM_INCLUDE_BENCHMARKS=OFF
+       -DBUILD_SHARED_LIBS=ON
+    )
+
+    local variables=("")
+
+    if [[ -n "${CC:-}" ]]; then
+        variables+=("CC=${CC}")
+    fi
+
+    if [[ -n "${CXX:-}" ]]; then
+        variables+=("CXX=${CXX}")
+    fi
+
+    if [[ -n "${LDFLAGS:-}" ]]; then
+        variables+=("LDFLAGS=${LLVM_LDFLAGS}")
+    fi
+
+    if [[ -n "${variables[*]}" ]]; then
+      "${variables[*]}" cmake "${CONFIG[@]}" "${LLVM_SRC_BASE}"
+    else
+      cmake "${CONFIG[@]}" "${LLVM_SRC_BASE}"
+    fi
+  fi
+
+  # Linking LLVM can require a lot of memory.
+  # First try multicore - if that doesn't work, try single core
+  (make "-j$(nproc)") || (make) || return 1
+  touch "${LLVM_BUILD}/.build_finished"
+}
+
+install_llvm() {
+  if [[ "${SANITIZER_BUILD}" != "memory" ]]; then
+    cd "${LLVM_BUILD}"
+    make "-j$(nproc)" install
+    cp "${LLVM_BUILD_BIN}/FileCheck" "${LLVM_INSTALL}/bin/"
+    cp "${LLVM_BUILD_BIN}/not" "${LLVM_INSTALL}/bin/"
+  
+    # Remove debug information from binaries
+    strip "${LLVM_INSTALL}/bin/"* || /bin/true
+    strip "${LLVM_INSTALL}/lib/libclang"* || /bin/true
+    strip "${LLVM_INSTALL}/lib/libLTO"* || /bin/true
+  else
+    # Handle memory sanitizer install
+    LLVM_PACKAGES=( \
+      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
+      install-llvm-symbolizer install-LLVMSupport install-lli not FileCheck )
+  
+    if [[ ${LLVM_VERSION_SHORT} -eq 38 ]]; then
+      LLVM_PACKAGES=("${LLVM_PACKAGES[@]}" installhdrs)
+    else
+      LLVM_PACKAGES=("${LLVM_PACKAGES[@]}" install-llvm-headers)
+    fi
+  
+    ninja "${LLVM_PACKAGES[@]}"
+
+    for i in $(ninja -t targets |grep install-LLVM | cut -d : -f 1); do ninja "$i"; done
+    
+    cp "${LLVM_BUILD}/bin/FileCheck" "${LLVM_INSTALL}/bin/"
+    cp "${LLVM_BUILD}/bin/not" "${LLVM_INSTALL}/bin/"
+  fi
+
+  touch "${LLVM_INSTALL}/.install_finished"
+}
+
+# Check if the binary artifact is installed
+is_installed_llvm() {
+  (
+    setup_build_variables_llvm
+    # Check if the specific llvm-config exists
+    [[ -f "${LLVM_BUILD_BIN}/llvm-config" ]]
+    [[ -f "${LLVM_INSTALL}/.install_finished" ]]
+  ) || return 1
+}
+
+# Returns a unique id for this configuration
+get_docker_config_id_llvm() {
+  (
+    setup_build_variables_llvm
+    echo "${LLVM_VERSION_SHORT}${LLVM_SUFFIX}"
+  )
+}
+
+setup_artifact_variables_llvm() {
+  setup_build_variables_llvm
+}
+
+get_build_artifacts_llvm() {
+  (
+    setup_build_variables_llvm
+    echo "${LLVM_INSTALL}"
+    echo "${LLVM_SRC_BASE}"
+    [[ "${sanitizer}" == "memory" ]] && echo "${SANITIZER_LLVM_UNINSTRUMENTED}"
+    [[ "${sanitizer}" == "memory" ]] && echo "${SANITIZER_LLVM_LIBCXX}"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-metasmt-linux-ubuntu-16.04.inc b/scripts/build/p-metasmt-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..063a5cd3
--- /dev/null
+++ b/scripts/build/p-metasmt-linux-ubuntu-16.04.inc
@@ -0,0 +1,27 @@
+setup_build_variables_metasmt() {
+  return 0
+}
+
+install_build_dependencies_metasmt() {
+  apt update -y
+
+  dependencies=(
+    # libgmp, gperf (required by yices2)
+    gperf
+    libgmp-dev
+
+    build-essential
+    git
+    wget
+    ca-certificates
+    cmake
+    zlib1g-dev
+    bison
+    flex
+    unzip
+    python
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-metasmt.inc b/scripts/build/p-metasmt.inc
new file mode 100644
index 00000000..a0b973a4
--- /dev/null
+++ b/scripts/build/p-metasmt.inc
@@ -0,0 +1,64 @@
+setup_build_variables_metasmt() {
+  METASMT_SRC_PATH="${BASE}/metaSMT-${METASMT_VERSION}"
+  METASMT_BUILD_PATH="${BASE}/metaSMT-${METASMT_VERSION}-build"
+  METASMT_INSTALL_PATH="${BASE}/metaSMT-${METASMT_VERSION}-install"
+  METASMT_DEPS_PATH="${BASE}/metaSMT-${METASMT_VERSION}-deps"
+}
+
+download_metasmt() {
+  # Clone
+  git clone --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git "${METASMT_SRC_PATH}"
+  cd "${METASMT_SRC_PATH}"
+  git submodule update --init
+  # Bootstrap
+  git clone https://github.com/agra-uni-bremen/dependencies.git
+}
+
+build_metasmt() {
+  cd "${METASMT_SRC_PATH}"
+  ./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 \
+    --deps "${METASMT_DEPS_PATH}/" \
+    --install "${METASMT_INSTALL_PATH}/" \
+    -j "$(nproc)" \
+    "${METASMT_BUILD_PATH}"
+
+  # Build
+  cd "${METASMT_BUILD_PATH}"
+  make
+}
+
+install_metasmt() {
+  cd "${METASMT_BUILD_PATH}"
+  make install
+  touch "${METASMT_INSTALL_PATH}"/.is_installed
+}
+
+get_docker_config_id_metasmt() {
+  echo "${METASMT_VERSION}"
+}
+
+# Check if the binary artifact is installed
+is_installed_metasmt() {
+  (
+  setup_build_variables_metasmt
+  [[ -f "${METASMT_INSTALL_PATH}"/.is_installed ]]
+  )
+}
+
+get_docker_config_id_metasmt() {
+  (
+    echo "${METASMT_VERSION}"
+  )
+}
+
+get_build_artifacts_metasmt() {
+  (
+    setup_build_variables_metasmt
+    echo "${METASMT_INSTALL_PATH}/"
+    echo "${METASMT_BUILD_PATH}/"
+    echo "${METASMT_DEPS_PATH}/"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-stp-linux-ubuntu-16.04.inc b/scripts/build/p-stp-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..f4030023
--- /dev/null
+++ b/scripts/build/p-stp-linux-ubuntu-16.04.inc
@@ -0,0 +1,19 @@
+#!/bin/bash
+# Build dependencies
+install_build_dependencies_stp() { 
+  apt update -y
+
+  dependencies=(
+    build-essential
+
+    bison
+    ca-certificates
+    cmake
+    flex
+    git
+    zlib1g-dev
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-stp-osx.inc b/scripts/build/p-stp-osx.inc
new file mode 100644
index 00000000..60214b3c
--- /dev/null
+++ b/scripts/build/p-stp-osx.inc
@@ -0,0 +1,7 @@
+install_build_dependencies_stp() {
+   dependencies=(
+     bison
+     flex
+   )
+   brew install "${dependencies[@]}"
+}
diff --git a/scripts/build/p-stp.inc b/scripts/build/p-stp.inc
new file mode 100644
index 00000000..9bbc90d9
--- /dev/null
+++ b/scripts/build/p-stp.inc
@@ -0,0 +1,113 @@
+#!/bin/bash
+# Build scripts for STP
+
+# Variables that any artifact of this package might depend on
+setup_build_variables_stp() {
+  STP_SUFFIX="${SANITIZER_SUFFIX}"
+
+  MINISAT_BUILD_PATH="${BASE}/minisat-build${STP_SUFFIX}"
+  MINISAT_INSTALL_PATH="${BASE}/minisat-install${STP_SUFFIX}"
+
+  STP_BUILD_PATH="${BASE}/stp-${STP_VERSION}-build${STP_SUFFIX}"
+  STP_INSTALL_PATH="${BASE}/stp-${STP_VERSION}-install${STP_SUFFIX}"
+  stp_url="https://github.com/stp/stp.git"
+
+  return 0
+}
+
+download_stp() {
+  source "${DIR}/common-functions"
+  # Download minisat
+  git_clone_or_update https://github.com/stp/minisat "${BASE}/minisat" "master"
+
+  # Download STP
+  git_clone_or_update "${stp_url}" "${BASE}/stp-${STP_VERSION}" "${STP_VERSION}"
+}
+
+build_stp() {
+  local CFLAGS=""
+  local CXXFLAGS=""
+  local LDFLAGS=""
+  local cmake_general_args=()
+
+  # Check if sanitizers should be used to build stp
+  if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then
+    CFLAGS="${SANITIZER_C_FLAGS[*]}"
+    CXXFLAGS="${SANITIZER_CXX_FLAGS[*]}"
+    LDFLAGS="${SANITIZER_LD_FLAGS[*]}"
+
+    cmake_general_args=(
+      "-DCMAKE_C_COMPILER=${SANITIZER_C_COMPILER}"
+      "-DCMAKE_CXX_COMPILER=${SANITIZER_CXX_COMPILER}"
+    )
+  fi
+
+  mkdir -p "${MINISAT_BUILD_PATH}"
+  cd "${MINISAT_BUILD_PATH}" || return 1
+
+  local minisat_cmake_args=(
+    ${cmake_general_args[@]+"${cmake_general_args[@]}"}
+    "-DCMAKE_INSTALL_PREFIX=${MINISAT_INSTALL_PATH}"
+  )
+  CFLAGS="${CFLAGS}" CXXFLAGS="${CXXFLAGS}" LDFLAGS="${LDFLAGS}" \
+    cmake "${minisat_cmake_args[@]}" "${BASE}/minisat"
+
+  # Try to build parallel
+  make "-j$(nproc)" || make 
+  make install
+
+  mkdir -p "${STP_BUILD_PATH}"
+  cd "${STP_BUILD_PATH}" || return 1
+
+  local stp_cmake_args=(
+      ${cmake_general_args[@]+"${cmake_general_args[@]}"}
+      # Don't build against boost because that is broken when mixing packaged boost libraries and gcc 4.8
+      "-DNO_BOOST:BOOL=ON"
+      "-DENABLE_PYTHON_INTERFACE:BOOL=OFF"
+      "-DONLY_SIMPLE:BOOL=ON"
+      "-DCMAKE_PREFIX_PATH=${MINISAT_INSTALL_PATH}"
+      "-DCMAKE_INSTALL_PREFIX=${STP_INSTALL_PATH}"
+  )
+
+  CFLAGS="${CFLAGS}" CXXFLAGS="${CXXFLAGS}" LDFLAGS="${LDFLAGS}" \
+  cmake "${stp_cmake_args[@]}" "${BASE}/stp-${STP_VERSION}"
+
+  # Try to build parallel
+  make "-j$(nproc)" || make
+  make install
+  touch "${STP_INSTALL_PATH}/.stp_installed"
+}
+
+install_stp() {
+  return 0
+}
+
+# Check if the binary artifact is installed
+is_installed_stp() {
+  (
+    setup_build_variables_stp
+    [[ -f "${STP_INSTALL_PATH}/.stp_installed" ]]
+  ) || return 1
+}
+
+setup_artifact_variables_stp() {
+  setup_build_variables_stp
+}
+
+get_build_artifacts_stp() {
+  (
+    setup_build_variables_stp
+    echo "${MINISAT_INSTALL_PATH}"
+    echo "${STP_INSTALL_PATH}"
+  )
+}
+
+get_docker_config_id_stp() {
+  (
+    source "${DIR}/common-functions"
+    setup_build_variables_stp
+
+    stp_remote_commit="$(get_git_hash "${stp_url}" "${STP_VERSION}")"
+    echo "${stp_remote_commit}${STP_SUFFIX}"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc b/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..26bf2da9
--- /dev/null
+++ b/scripts/build/p-tcmalloc-linux-ubuntu-16.04.inc
@@ -0,0 +1,13 @@
+install_build_dependencies_tcmalloc() { 
+  apt update -y
+
+  dependencies=(
+  build-essential
+    ca-certificates
+    cmake
+    git
+    wget
+  )
+
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-tcmalloc.inc b/scripts/build/p-tcmalloc.inc
new file mode 100644
index 00000000..00a97626
--- /dev/null
+++ b/scripts/build/p-tcmalloc.inc
@@ -0,0 +1,49 @@
+setup_build_variables_tcmalloc() {
+  TCMALLOC_SRC_PATH="${BASE}/gperftools-${TCMALLOC_VERSION}"
+  TCMALLOC_INSTALL_PATH="${BASE}/tcmalloc-install-${TCMALLOC_VERSION}"
+  return 0
+}
+
+download_tcmalloc() {
+  # Get tcmalloc release
+  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"
+}
+
+build_tcmalloc() { 
+  cd "${TCMALLOC_SRC_PATH}"
+  ./configure --disable-dependency-tracking --disable-cpu-profiler \
+    --disable-heap-checker --disable-debugalloc  --enable-minimal \
+    --prefix="${TCMALLOC_INSTALL_PATH}"
+  make "-j$(nproc)" || make
+}
+
+install_tcmalloc() {
+  cd "${TCMALLOC_SRC_PATH}"
+  make install
+  touch "${TCMALLOC_INSTALL_PATH}"/.is_installed
+}
+
+is_installed_tcmalloc() {
+  (
+    setup_build_variables_tcmalloc
+    [[ -f "${TCMALLOC_INSTALL_PATH}"/.is_installed ]]
+  ) || return 1
+}
+
+setup_artifact_variables_tcmalloc() {
+  setup_build_variables_tcmalloc
+}
+
+
+get_docker_config_id_tcmalloc() {
+  echo "${TCMALLOC_VERSION}"
+}
+
+get_build_artifacts_tcmalloc() {
+  (
+    setup_build_variables_tcmalloc
+    echo "${TCMALLOC_INSTALL_PATH}"
+  )
+}
\ No newline at end of file
diff --git a/scripts/build/p-uclibc-linux-ubuntu-16.04.inc b/scripts/build/p-uclibc-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..36bdce58
--- /dev/null
+++ b/scripts/build/p-uclibc-linux-ubuntu-16.04.inc
@@ -0,0 +1,17 @@
+#!/bin/bash
+# Build dependencies
+install_build_dependencies_uclibc() { 
+  apt update -y
+
+  dependencies=(
+    build-essential
+    ca-certificates
+    git
+    python
+    libncurses5-dev
+    wget
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-uclibc.inc b/scripts/build/p-uclibc.inc
new file mode 100644
index 00000000..95af9751
--- /dev/null
+++ b/scripts/build/p-uclibc.inc
@@ -0,0 +1,49 @@
+# Build scripts for uclibc
+setup_build_variables_uclibc() {
+  UCLIBC_PATH="${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}"
+  uclibc_url="https://github.com/klee/klee-uclibc.git"
+}
+
+download_uclibc() {
+  source "${DIR}/common-functions"
+  git_clone_or_update "${uclibc_url}" "${UCLIBC_PATH}" "${UCLIBC_VERSION}"
+}
+
+build_uclibc() { 
+  cd "${UCLIBC_PATH}" || return 1
+  ./configure --make-llvm-lib --with-cc "${BITCODE_CC}" --with-llvm-config "${LLVM_CONFIG}"
+  make || return 1
+  touch .is_installed
+}
+
+install_uclibc() {
+  return 0  
+}
+
+# Check if the binary artifact is installed
+is_installed_uclibc() {
+  (
+    setup_build_variables_uclibc
+    [[ -f "${UCLIBC_PATH}"/.is_installed ]]
+  ) || return 1
+}
+
+get_docker_config_id_uclibc() {
+  (
+    source "${DIR}/common-functions"
+    setup_build_variables_uclibc
+    uclibc_remote_commit="$(get_git_hash "${uclibc_url}" "${UCLIBC_VERSION}")"
+    echo "${uclibc_remote_commit}_${LLVM_VERSION_SHORT}"
+  )
+}
+
+get_build_artifacts_uclibc() {
+  (
+    setup_build_variables_uclibc
+    echo "${UCLIBC_PATH}"
+  )
+}
+
+setup_artifact_variables_uclibc() {
+  setup_build_variables_uclibc
+}
\ No newline at end of file
diff --git a/scripts/build/p-z3-linux-ubuntu-16.04.inc b/scripts/build/p-z3-linux-ubuntu-16.04.inc
new file mode 100644
index 00000000..2f5e4086
--- /dev/null
+++ b/scripts/build/p-z3-linux-ubuntu-16.04.inc
@@ -0,0 +1,16 @@
+# Build dependencies Z3
+install_build_dependencies_z3() { 
+  apt update -y
+
+  dependencies=(
+    build-essential
+
+	python
+    git
+    wget
+    ca-certificates
+  )
+
+  #Install essential dependencies
+  apt -y --no-install-recommends install "${dependencies[@]}"
+}
\ No newline at end of file
diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc
new file mode 100644
index 00000000..bce11aab
--- /dev/null
+++ b/scripts/build/p-z3-osx.inc
@@ -0,0 +1,13 @@
+install_binary_artifact_z3 () {
+  set +e
+  brew install python@2
+  if [[ "X$?" != "X0" ]]; then
+     brew link --overwrite python@2
+  fi
+  set -e
+  brew install z3
+}
+
+is_installed_z3() {
+    [[ -f "/usr/local/opt/z3/bin/z3" ]]
+}
\ No newline at end of file
diff --git a/scripts/build/p-z3.inc b/scripts/build/p-z3.inc
new file mode 100644
index 00000000..f6db455b
--- /dev/null
+++ b/scripts/build/p-z3.inc
@@ -0,0 +1,68 @@
+setup_build_variables_z3() {
+  Z3_SUFFIX="${SANITIZER_SUFFIX}"
+  Z3_SRC_PATH="${BASE}/z3-${Z3_VERSION}"
+  Z3_INSTALL_PATH="${BASE}/z3-${Z3_VERSION}-install${Z3_SUFFIX}"
+}
+
+download_z3() {
+  mkdir -p "${Z3_SRC_PATH}"
+  cd "${Z3_SRC_PATH}"
+  wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1
+}
+
+build_z3() {
+  local CFLAGS=""
+  local CXXFLAGS=""
+  local LDFLAGS=""
+  local CC=""
+  local CXX=""
+  
+  # Check if sanitizers should be used to build z3
+  if [[ "${SANITIZER_SUFFIX}x" != "x" ]]; then
+    CFLAGS="${SANITIZER_C_FLAGS[*]}"
+    CXXFLAGS="${SANITIZER_CXX_FLAGS[*]}"
+    LDFLAGS="${SANITIZER_LD_FLAGS[*]}"
+    
+    CC="${SANITIZER_C_COMPILER}"
+    CXX="${SANITIZER_CXX_COMPILER}"
+  fi
+  CFLAGS="${CFLAGS}" \
+  CXXFLAGS="${CXXFLAGS}" \
+  LDFLAGS="${LDFLAGS}" \
+  CC="${CC}" \
+  CXX="${CXX}" \
+  python scripts/mk_make.py --prefix "${Z3_INSTALL_PATH}" -b "build${Z3_SUFFIX}"
+  cd "build${Z3_SUFFIX}"
+  make -j$(nproc) || make
+}
+
+install_z3() {
+  cd "${Z3_SRC_PATH}/build${Z3_SUFFIX}"
+  make install
+  touch "${Z3_INSTALL_PATH}"/.is_installed
+}
+
+is_installed_z3() {
+  (
+    setup_build_variables_z3
+    [[ -f "${Z3_INSTALL_PATH}"/.is_installed ]]
+  ) || return 1
+}
+
+get_build_artifacts_z3() {
+  (
+    setup_build_variables_z3
+    echo "${Z3_INSTALL_PATH}"
+  )
+}
+
+setup_artifact_variables_z3() {
+  setup_build_variables_z3
+}
+
+get_docker_config_id_z3() {
+  (
+    setup_build_variables_z3
+    echo "${Z3_VERSION}${Z3_SUFFIX}"
+  )
+}
diff --git a/scripts/build/patches/llvm40.patch b/scripts/build/patches/llvm40.patch
new file mode 100644
index 00000000..6cc9fe41
--- /dev/null
+++ b/scripts/build/patches/llvm40.patch
@@ -0,0 +1,77 @@
+--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.cc  2018-12-20 22:32:09.636508226 +0000
++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.cc  2018-12-20 22:36:10.752698342 +0000
+@@ -607,8 +607,7 @@ uptr internal_prctl(int option, uptr arg
+ }
+ #endif
+
+-uptr internal_sigaltstack(const struct sigaltstack *ss,
+-                         struct sigaltstack *oss) {
++uptr internal_sigaltstack(const void *ss, void *oss) {
+   return internal_syscall(SYSCALL(sigaltstack), (uptr)ss, (uptr)oss);
+ }
+
+--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.h 2018-12-20 22:32:10.020508531 +0000
++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_linux.h 2018-12-20 22:36:10.752698342 +0000
+@@ -21,7 +21,6 @@
+ #include "sanitizer_platform_limits_posix.h"
+
+ struct link_map;  // Opaque type returned by dlopen().
+-struct sigaltstack;
+
+ namespace __sanitizer {
+ // Dirent structure for getdents(). Note that this structure is different from
+@@ -30,8 +29,7 @@ struct linux_dirent;
+
+ // Syscall wrappers.
+ uptr internal_getdents(fd_t fd, struct linux_dirent *dirp, unsigned int count);
+-uptr internal_sigaltstack(const struct sigaltstack* ss,
+-                          struct sigaltstack* oss);
++uptr internal_sigaltstack(const void* ss, void* oss);
+ uptr internal_sigprocmask(int how, __sanitizer_sigset_t *set,
+     __sanitizer_sigset_t *oldset);
+
+--- ./projects/compiler-rt/lib/sanitizer_common/sanitizer_stoptheworld_linux_libcdep.cc 2018-12-20 22:32:09.456508085 +0000
++++ ../llvm-40-copy/projects/compiler-rt/lib/sanitizer_common/sanitizer_stoptheworld_linux_libcdep.cc 2018-12-20 22:36:10.756698345 +0000
+@@ -275,7 +275,7 @@ static int TracerThread(void* argument)
+
+   // Alternate stack for signal handling.
+   InternalScopedBuffer<char> handler_stack_memory(kHandlerStackSize);
+-  struct sigaltstack handler_stack;
++  stack_t handler_stack;
+   internal_memset(&handler_stack, 0, sizeof(handler_stack));
+   handler_stack.ss_sp = handler_stack_memory.data();
+   handler_stack.ss_size = kHandlerStackSize;
+--- ./projects/compiler-rt/lib/tsan/rtl/tsan_platform_linux.cc  2018-12-20 22:32:15.780513072 +0000
++++ ../llvm-40-copy/projects/compiler-rt/lib/tsan/rtl/tsan_platform_linux.cc  2018-12-20 22:36:10.756698345 +0000
+@@ -289,7 +289,7 @@ void InitializePlatform() {
+ int ExtractResolvFDs(void *state, int *fds, int nfd) {
+ #if SANITIZER_LINUX && !SANITIZER_ANDROID
+   int cnt = 0;
+-  __res_state *statp = (__res_state*)state;
++  struct __res_state *statp = (struct __res_state*)state;
+   for (int i = 0; i < MAXNS && cnt < nfd; i++) {
+     if (statp->_u._ext.nsaddrs[i] && statp->_u._ext.nssocks[i] != -1)
+       fds[cnt++] = statp->_u._ext.nssocks[i];
+diff -rup ./projects/libcxx/include/__locale ../llvm-40-copy/projects/libcxx/include/__locale
+--- ./projects/libcxx/include/__locale  2018-12-20 22:33:14.484559356 +0000
++++ ../llvm-40-copy/projects/libcxx/include/__locale  2018-12-20 22:34:34.432622394 +0000
+@@ -34,7 +34,7 @@
+ # include <support/solaris/xlocale.h>
+ #elif defined(_NEWLIB_VERSION)
+ # include <support/newlib/xlocale.h>
+-#elif (defined(__GLIBC__) || defined(__APPLE__)      || defined(__FreeBSD__) \
++#elif (defined(__APPLE__)      || defined(__FreeBSD__) \
+     || defined(__EMSCRIPTEN__) || defined(__IBMCPP__))
+ # include <xlocale.h>
+ #elif defined(_LIBCPP_HAS_MUSL_LIBC)
+--- ./projects/compiler-rt/lib/esan/esan_sideline_linux.cpp  2018-12-20 22:32:12.368510380 +0000
++++ ../llvm-40-copy/projects/compiler-rt/lib/esan/esan_sideline_linux.cpp 2018-12-21 09:15:03.721823179 +0000
+@@ -70,7 +70,7 @@ int SidelineThread::runSideline(void *Ar
+
+   // Set up a signal handler on an alternate stack for safety.
+   InternalScopedBuffer<char> StackMap(SigAltStackSize);
+-  struct sigaltstack SigAltStack;
++  stack_t SigAltStack;
+   SigAltStack.ss_sp = StackMap.data();
+   SigAltStack.ss_size = SigAltStackSize;
+   SigAltStack.ss_flags = 0;
diff --git a/scripts/build/run-coverage.sh b/scripts/build/run-coverage.sh
deleted file mode 100755
index ceba8216..00000000
--- a/scripts/build/run-coverage.sh
+++ /dev/null
@@ -1,25 +0,0 @@
-#!/bin/bash
-
-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"
-
-if [[ "a$COVERAGE" != "a1" ]]; then
-  exit 0
-fi
-
-function upload_coverage() {
-  file=$1
-  tags=$2
-  ci_env=$(bash <(curl -s https://codecov.io/env))
-  docker run ${ci_env} -ti ${REPOSITORY}/klee:${LLVM_VERSION_SHORT}${LLVM_SUFFIX}${SOLVER_SUFFIX}${DEPS_SUFFIX} /bin/bash -c "cd /home/klee/klee_src && bash <(curl -s https://codecov.io/bash) -X gcov -y /home/klee/klee_src/.codecov.yml -f /home/klee/klee_build/coverage_all.info.${file} -F $tags"
-}
-
-# FIXME Enable separated coverage tags again
-upload_coverage systemtests systemtests_unittests
-upload_coverage unittests systemtests_unittests
diff --git a/scripts/build/run-tests.sh b/scripts/build/run-tests.sh
new file mode 100755
index 00000000..f39dcad8
--- /dev/null
+++ b/scripts/build/run-tests.sh
@@ -0,0 +1,153 @@
+#!/bin/bash
+set -e
+set -u
+DIR="$(cd "$(dirname "$0")" && pwd)"
+
+
+coverage_setup() {
+  local build_dir="$1"
+  # Zero coverage for any file, e.g. previous tests
+  lcov -q --directory "${build_dir}" --no-external --zerocounters
+  # Create a baseline by capturing any file used for compilation, no execution yet
+  lcov -q --rc lcov_branch_coverage=1 --directory "${build_dir}" --base-directory="${KLEE_SRC}" --no-external --capture --initial --output-file coverage_base.info
+  lcov -q --rc lcov_branch_coverage=1 --remove coverage_base.info 'test/*' --output-file coverage_base.info
+  lcov -q --rc lcov_branch_coverage=1 --remove coverage_base.info 'unittests/*' --output-file coverage_base.info
+}
+
+coverage_update() {
+  tags="$2"
+  codecov_suffix=(${tags// /})
+  build_dir="$1"
+  # Create report
+  # (NOTE: "--rc lcov_branch_coverage=1" needs to be added in all calls, otherwise branch coverage gets dropped)
+  lcov -q --rc lcov_branch_coverage=1 --directory "${build_dir}" --base-directory="${KLEE_SRC}" --no-external --capture --output-file coverage.info
+  # Exclude uninteresting coverage goals (LLVM, googletest, and KLEE system and unit tests)
+  lcov -q --rc lcov_branch_coverage=1 --remove coverage.info 'test/*' --output-file coverage.info
+  lcov -q --rc lcov_branch_coverage=1 --remove coverage.info 'unittests/*' --output-file coverage.info
+  # Combine baseline and measured coverage
+  lcov -q --rc lcov_branch_coverage=1 -a coverage_base.info -a coverage.info -o coverage_all.info."${codecov_suffix}"
+  # Debug info
+  lcov -q --rc lcov_branch_coverage=1 --list coverage_all.info."${codecov_suffix}"
+}
+
+run_tests() {
+  build_dir="$1"
+  KLEE_SRC="$(cd "${DIR}"/../../ && pwd)"
+
+  # TODO change to pinpoint specific directory
+  cd "${build_dir}"
+
+  ###############################################################################
+  # Unit tests
+  ###############################################################################
+  # Prepare coverage information if COVERAGE is set
+  if [ "${COVERAGE}" -eq 1 ]; then
+    coverage_setup "${build_dir}"
+  fi
+  make unittests
+  
+  # Generate and upload coverage if COVERAGE is set
+  if [ "${COVERAGE}" -eq 1 ]; then
+    coverage_update "${build_dir}" "unittests"
+  fi
+
+  ###############################################################################
+  # lit tests
+  ###############################################################################
+  if [ "${COVERAGE}" -eq 1 ]; then
+    coverage_setup "${build_dir}"
+  fi
+  make systemtests || return 1
+  
+  # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
+  if [ "X${SOLVERS}" == "XmetaSMT" ]; then
+    available_metasmt_backends="btor stp z3 yices2 cvc4"
+    for backend in $available_metasmt_backends; do
+      if [ "X${METASMT_DEFAULT}" != "X$backend" ]; then
+        if [ "$backend" == "cvc4" ]; then
+          for num in {1..5}; do sleep 120; echo 'Keep Travis alive'; done &
+        fi
+        lit -v --param klee_opts=-metasmt-backend="$backend" --param kleaver_opts=-metasmt-backend="$backend" test/
+      fi
+    done
+  fi
+  
+  # Generate and upload coverage if COVERAGE is set
+  if [ "${COVERAGE}" -eq 1 ]; then
+    coverage_update "${build_dir}" "systemtests"
+  fi
+}
+
+
+
+function upload_coverage() {
+  file="$1"
+  tags="$2"
+  cd /home/klee/klee_src
+  bash <(curl -s https://codecov.io/bash) -X gcov -R /tmp/klee_src/ -y .codecov.yml -f /home/klee/klee_build/coverage_all.info."${file}" -F "$tags"
+}
+
+function run_docker() {
+ docker_arguments=(docker run -u root --cap-add SYS_PTRACE -ti)
+ script_arguments=("--debug" '"/tmp/klee_build"*')
+ if [[ "${COVERAGE}" -eq 1 ]]; then
+   script_arguments+=("--coverage")
+ fi
+ 
+ if [[ "${UPLOAD_COVERAGE}" -eq 1 ]]; then
+   docker_arguments+=($(bash <(curl -s https://codecov.io/env)))
+   script_arguments+=("--upload-coverage")
+ fi
+
+ # Run the image that was build last with extended capabilities to allow tracing tests
+ "${docker_arguments[@]}" "$(docker images -q | head -n 1)" /bin/bash -i -c "ulimit -s 16384; source /home/klee/.bashrc; export; /tmp/klee_src/scripts/build/run-tests.sh ${script_arguments[*]}"
+}
+
+main() {
+  local NAME
+  NAME=$(basename "${0}")
+  local RUN_DOCKER=0
+  local COVERAGE=0
+  local UPLOAD_COVERAGE=0
+  local directory=""
+
+  for i in "$@" ;do
+  case $i in
+    --debug)
+      set -x
+    ;;
+    --run-docker)
+    RUN_DOCKER=1
+    ;;
+    --coverage)
+    COVERAGE=1
+    ;;
+    --upload-coverage)
+    UPLOAD_COVERAGE=1
+    ;;
+    -*)
+      echo "${NAME}: unknown argument: $i"
+      exit 1
+    ;;
+    *)
+    directory="${i}"
+    ;;
+  esac
+  done
+
+
+  if [[ "${RUN_DOCKER}" -eq 1 ]]; then
+    run_docker "${COVERAGE}"
+    return 0
+  fi
+
+  run_tests "${directory}"
+  
+  # FIXME Enable separated coverage tags again
+  if [[ "${UPLOAD_COVERAGE}" -eq 1 ]]; then
+    upload_coverage systemtests systemtests_unittests
+    upload_coverage unittests systemtests_unittests
+  fi
+ }
+
+main "$@"
\ No newline at end of file
diff --git a/scripts/build/solver-metasmt.sh b/scripts/build/solver-metasmt.sh
deleted file mode 100755
index d8626149..00000000
--- a/scripts/build/solver-metasmt.sh
+++ /dev/null
@@ -1,39 +0,0 @@
-#!/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
deleted file mode 100755
index 2e65ca30..00000000
--- a/scripts/build/solver-stp.sh
+++ /dev/null
@@ -1,57 +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
-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
deleted file mode 100755
index c6c3381d..00000000
--- a/scripts/build/solver-z3.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/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/scripts/build/solvers.sh b/scripts/build/solvers.sh
deleted file mode 100755
index 71ad0c2d..00000000
--- a/scripts/build/solvers.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/bin/bash -x
-# Make sure we exit if there is a failure
-set -e
-
-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"
-    "${DIR}/solver-stp.sh"
-    ;;
-  Z3)
-    echo "Z3"
-    "${DIR}/solver-z3.sh"
-    ;;
-  metaSMT)
-    echo "metaSMT"
-    "${DIR}/solver-metasmt.sh"
-    ;;
-  *)
-    echo "Unknown solver ${solver}"
-    exit 1
-  esac
-done
diff --git a/scripts/build/tcmalloc.sh b/scripts/build/tcmalloc.sh
deleted file mode 100755
index ea5596d0..00000000
--- a/scripts/build/tcmalloc.sh
+++ /dev/null
@@ -1,35 +0,0 @@
-#!/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
deleted file mode 100755
index 8a855291..00000000
--- a/scripts/build/testing-utils.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/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
deleted file mode 100755
index 3440bedb..00000000
--- a/scripts/build/uclibc.sh
+++ /dev/null
@@ -1,37 +0,0 @@
-#!/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
diff --git a/scripts/build/v-clang.inc b/scripts/build/v-clang.inc
new file mode 100644
index 00000000..16036f22
--- /dev/null
+++ b/scripts/build/v-clang.inc
@@ -0,0 +1,15 @@
+required_variables_clang=(
+  "LLVM_VERSION"
+)
+
+artifact_dependency_clang=("sanitizer")
+
+setup_variables_clang() {
+  LLVM_VERSION_SHORT="${LLVM_VERSION/./}"
+}
+
+export_variables_clang=(
+  "LLVM_CONFIG"
+  "BITCODE_CC"
+  "BITCODE_CXX"
+)
\ No newline at end of file
diff --git a/scripts/build/v-gtest.inc b/scripts/build/v-gtest.inc
new file mode 100644
index 00000000..a48654f0
--- /dev/null
+++ b/scripts/build/v-gtest.inc
@@ -0,0 +1,7 @@
+# Build information for gtest
+required_variables_gtest=(
+  "GTEST_VERSION"
+)
+
+# Artifacts gtest depends on
+artifact_dependency_gtest=("")
\ No newline at end of file
diff --git a/scripts/build/v-klee.inc b/scripts/build/v-klee.inc
new file mode 100644
index 00000000..d90892f4
--- /dev/null
+++ b/scripts/build/v-klee.inc
@@ -0,0 +1,42 @@
+# Build information for KLEE
+required_variables_klee=(
+  "COVERAGE"
+  "USE_TCMALLOC"
+)
+
+required_variables_check_klee() {
+  check_bool "COVERAGE"
+  check_bool "USE_TCMALLOC"
+}
+
+# On which artifacts does KLEE depend on
+artifact_dependency_klee(){
+  local dependencies=("llvm" "solvers" "gtest")
+  if [[ "${OS}" != "osx" ]]; then
+    dependencies+=(uclibc)
+  fi
+
+  if [[ "${USE_TCMALLOC}" -eq 1 ]]; then
+    dependencies+=("tcmalloc")
+  fi
+
+  for d in "${dependencies[@]}"; do
+    echo "${d}"
+  done
+}
+
+runtime_artifact_dependency_klee(){
+  local dependencies=("")
+  if [[ "${OS}" != "osx" ]]; then
+    echo "uclibc"
+  fi
+  dependencies+=("llvm" "solvers" "gtest")
+
+  if [[ "${USE_TCMALLOC}" -eq 1 ]]; then
+    dependencies+=("tcmalloc")
+  fi
+
+  for d in "${dependencies[@]}"; do
+    echo "${d}"
+  done
+}
diff --git a/scripts/build/v-llvm.inc b/scripts/build/v-llvm.inc
new file mode 100644
index 00000000..5ec6f713
--- /dev/null
+++ b/scripts/build/v-llvm.inc
@@ -0,0 +1,34 @@
+required_variables_llvm=(
+  "LLVM_VERSION"
+  "ENABLE_OPTIMIZED"
+  "ENABLE_DEBUG"
+  "DISABLE_ASSERTIONS"
+  "REQUIRES_RTTI"
+)
+
+required_variables_check_llvm() {
+  check_bool "ENABLE_DEBUG"
+  check_bool "ENABLE_OPTIMIZED"
+  check_bool "DISABLE_ASSERTIONS"
+  check_bool "REQUIRES_RTTI"
+}
+
+export_variables_llvm=(
+  "LLVM_CONFIG"
+  "BITCODE_CC"
+  "BITCODE_CXX"
+)
+
+artifact_dependency_llvm=("sanitizer")
+
+setup_variables_llvm() {
+  LLVM_VERSION_SHORT="${LLVM_VERSION/./}"
+}
+
+check_export_variables_llvm() {
+  # Check for variables set and not empty
+  [[ -n ${LLVM_CONFIG:-} ]] || (echo "LLVM_CONFIG not set"; exit 1)
+  [[ -n ${LLVM_INSTALL:-} ]] || (echo "LLVM_INSTALL not set"; exit 1)
+  [[ -n ${BITCODE_CC:-} ]] || (echo "BITCODE_CC not set"; exit 1)
+  [[ -n ${BITCODE_CXX:-} ]] || (echo "BITCODE_CXX not set"; exit 1)
+}
\ No newline at end of file
diff --git a/scripts/build/v-metasmt.inc b/scripts/build/v-metasmt.inc
new file mode 100644
index 00000000..362126bb
--- /dev/null
+++ b/scripts/build/v-metasmt.inc
@@ -0,0 +1,7 @@
+# Build information for metaSMT solver
+required_variables_metasmt=(
+  "METASMT_VERSION"
+  "METASMT_DEFAULT"
+)
+
+artifact_dependency_metasmt=("")
\ No newline at end of file
diff --git a/scripts/build/v-sanitizer.inc b/scripts/build/v-sanitizer.inc
new file mode 100644
index 00000000..be9b3b39
--- /dev/null
+++ b/scripts/build/v-sanitizer.inc
@@ -0,0 +1,88 @@
+#!/bin/bash
+# Variables for sanitizer handling
+
+required_variables_sanitizer=(
+  "SANITIZER_BUILD"
+)
+
+artifact_dependency_sanitizer=("")
+
+required_variables_check_sanitizer() {
+  # Allowe empty sanitizer builds
+  [[ -z "${SANITIZER_BUILD}" ]] && return 0
+  
+  local sanitizers
+  IFS=":" read -r -a sanitizers <<< "${SANITIZER_BUILD}"
+  for sanitizer in "${sanitizers[@]}"; do
+    [[ -z "${sanitizer}" ]] && continue
+    [[ "${sanitizer}" == "address" ]] && continue
+    [[ "${sanitizer}" == "memory" ]] && continue
+    [[ "${sanitizer}" == "undefined" ]] && continue
+    
+    echo "Unknown sanitizer: $sanitizer"
+    exit 1
+  done
+}
+
+setup_variables_sanitizer() {
+  if [[ -z "${SANITIZER_BUILD}" ]]; then
+    SANITIZERS=("")
+    SANITIZER_SUFFIX=""
+    return 0
+  fi
+  # Remove ":" separator
+  local sanitizers
+  local e
+  local sorted_sanitizers
+  
+  IFS=":" read -r -a sanitizers <<< "${SANITIZER_BUILD}"
+  sorted_sanitizers=( $( for e in "${sanitizers[@]}"; do echo "$e"; done | sort) )
+  
+  	
+  # Set variables used by clients.
+  ## Build variables
+  [[ -z ${SANITIZER_CXX_FLAGS+x} ]] && SANITIZER_CXX_FLAGS=("")
+  [[ -z ${SANITIZER_C_FLAGS+x} ]] && SANITIZER_C_FLAGS=("")
+  [[ -z ${SANITIZER_LD_FLAGS+x} ]] && SANITIZER_LD_FLAGS=("")
+  
+  # Docker_suffix
+  SANITIZER_SUFFIX=""
+  
+  local flags
+  for sanitizer in "${sorted_sanitizers[@]}"; do
+    [[ -z "${sanitizer}" ]] && continue
+    # AddressSanitizer
+    if [ "${sanitizer}" == "address" ]; 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"
+      continue
+    fi
+  
+    # Undefined Behaviour Sanitizer
+    if [ "${sanitizer}" == "undefined" ]; 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"
+      continue
+    fi
+  
+    # Undefined Behaviour Sanitizer
+    if [ "${sanitizer}" == "memory" ]; then
+      echo "Using Memory Sanitizer"
+      SANITIZER_SUFFIX+="_memsan"
+      continue
+    fi
+  
+    echo "Unknown sanitizer: $sanitizer"
+    exit 1
+  done
+  
+  SANITIZERS=("${sorted_sanitizers[@]}")
+  }
\ No newline at end of file
diff --git a/scripts/build/v-sanitizer_compiler.inc b/scripts/build/v-sanitizer_compiler.inc
new file mode 100644
index 00000000..e0cf2468
--- /dev/null
+++ b/scripts/build/v-sanitizer_compiler.inc
@@ -0,0 +1,21 @@
+# Meta-package for solvers
+required_variables_sanitizer_compiler=("")
+
+# On which artifacts does STP depend on
+artifact_dependency_sanitizer_compiler(){
+  echo "sanitizer"
+  if [[ -n ${SANITIZER_BUILD+x} ]]; then
+    [[ "${SANITIZER_BUILD}" == "memory" ]] && echo "llvm"
+    [[ "${SANITIZER_BUILD}" != "memory" ]] && echo "clang"
+  fi
+}
+
+
+# Setup general variables
+setup_variables_sanitizer_compiler() {
+  for sanitizer in "${SANITIZERS[@]}"; do
+    [[ -z "${sanitizer}" ]] && continue
+    SANITIZER_CMAKE_C_COMPILER=[""]
+  done
+
+}
\ No newline at end of file
diff --git a/scripts/build/v-solvers.inc b/scripts/build/v-solvers.inc
new file mode 100644
index 00000000..ad3f43f1
--- /dev/null
+++ b/scripts/build/v-solvers.inc
@@ -0,0 +1,63 @@
+# Meta-package for solvers
+required_variables_solvers=(
+  "SOLVERS"
+)
+
+required_variables_check_solvers() {
+  local solvers
+  IFS=":" read -r -a solvers <<< "${SOLVERS}"
+  [[ -z "${solvers[@]}" ]] && { echo "SOLVERS can't be empty"; exit 1; }
+  
+  for solver in "${solvers[@]}"; do
+    [[ -z "${solver}" ]] && continue
+    solver="$(to_lower ${solver})"
+
+    [[ "${solver}" == "z3" ]] && continue
+    [[ "${solver}" == "stp" ]] && continue
+    [[ "${solver}" == "metasmt" ]] && continue
+    
+    echo "Unknown solver: \"$solver\""
+    exit 1
+  done
+}
+
+# On which artifacts does SOLVERS depend on
+artifact_dependency_solvers() {
+  # Setup variables first to get selected solvers
+  setup_variables_solvers
+  for solver in "${SELECTED_SOLVERS[@]}"; do
+    echo "${solver}"
+  done
+}
+
+# On which artifacts does SOLVERS depend on
+runtime_artifact_dependency_solvers() {
+  # Setup variables first to get selected solvers
+  setup_variables_solvers
+  for solver in "${SELECTED_SOLVERS[@]}"; do
+    echo "${solver}"
+  done
+}
+
+# Setup general variables
+setup_variables_solvers() {
+  local solvers
+  IFS=":" read -r -a solvers <<< "${SOLVERS}"
+
+  SELECTED_SOLVERS=()
+  for solver in "${solvers[@]}"; do
+    [[ -z "${solver}" ]] && continue
+    solver="$(to_lower ${solver})"
+    [[ "${solver}" == "z3" ]] && SELECTED_SOLVERS+=("z3") && continue
+    [[ "${solver}" == "stp" ]] && SELECTED_SOLVERS+=("stp") && continue
+    [[ "${solver}" == "metasmt" ]] && SELECTED_SOLVERS+=("metasmt") && continue
+
+    echo "Unknown solver: \"$solver\""
+    exit 1
+  done
+
+  # Sort solvers
+  SELECTED_SOLVERS=( $( for e in "${SELECTED_SOLVERS[@]}"; do echo "$e"; done | sort|uniq) )
+# TODO Add specific suffix of each solver
+  SOLVER_SUFFIX=$(IFS=_ ; echo "${SELECTED_SOLVERS[*]}")
+}
\ No newline at end of file
diff --git a/scripts/build/v-stp.inc b/scripts/build/v-stp.inc
new file mode 100644
index 00000000..9bbc28f1
--- /dev/null
+++ b/scripts/build/v-stp.inc
@@ -0,0 +1,8 @@
+# Build information for STP solver
+required_variables_stp=(
+  "STP_VERSION"
+  "MINISAT_VERSION"
+)
+
+# On which artifacts does STP depend on
+artifact_dependency_stp=("sanitizer_compiler")
\ No newline at end of file
diff --git a/scripts/build/v-tcmalloc.inc b/scripts/build/v-tcmalloc.inc
new file mode 100644
index 00000000..e49b51c2
--- /dev/null
+++ b/scripts/build/v-tcmalloc.inc
@@ -0,0 +1,5 @@
+artifact_dependency_tcmalloc=("")
+
+required_variables_tcmalloc=(
+  "TCMALLOC_VERSION"
+)
\ No newline at end of file
diff --git a/scripts/build/v-uclibc.inc b/scripts/build/v-uclibc.inc
new file mode 100644
index 00000000..e7a2f720
--- /dev/null
+++ b/scripts/build/v-uclibc.inc
@@ -0,0 +1,17 @@
+required_variables_uclibc=(
+  "UCLIBC_VERSION"
+  "LLVM_VERSION"
+)
+
+artifact_dependency_uclibc(){
+  # Add llvm if needed; otherwise only use clang package
+# TODO this is quite distribution specific; should be handled in a more general case
+  local LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}"
+  local LLVM_VERSION_MINOR="${LLVM_VERSION/*./}"
+  # Check versions: no support for LLVM < 3.5
+  if [[ "${LLVM_VERSION_MAJOR}" -eq 3 ]]; then
+    [[ "${LLVM_VERSION_MINOR}" -lt 5 ]] && echo "llvm"
+  fi
+
+  echo "clang"
+}
\ No newline at end of file
diff --git a/scripts/build/v-z3.inc b/scripts/build/v-z3.inc
new file mode 100644
index 00000000..915336a3
--- /dev/null
+++ b/scripts/build/v-z3.inc
@@ -0,0 +1,7 @@
+# Build information for Z3 solver
+required_variables_z3=(
+  "Z3_VERSION"
+)
+
+# Artifacts Z3 depends on
+artifact_dependency_z3=("sanitizer_compiler")
\ No newline at end of file