diff --git a/.travis.yml b/.travis.yml
index 50d63e593..81ddefb8b 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,10 +22,17 @@ env:
     # 64-bit Clang 3.9 RelWithDebInfo
     - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
 
+    # Debug builds
+    #
+    # Note the unit tests for the debug builds are compiled but **not**
+    # executed. This is because the debug build of unit tests takes a large
+    # amount of time to execute compared to the optimized builds. The hope is
+    # that just running the optimized unit tests is sufficient.
+    #
     # 64-bit GCC 5.4 Debug
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
     # 64-bit Clang Debug
-    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
 
     # 32-bit GCC 5.4 RelWithDebInfo
     - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo
@@ -57,7 +64,7 @@ env:
     # 64-bit GCC 4.8 RelWithDebInfo
     - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo
     # 64-bit GCC 4.8 Debug
-    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug
+    - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug RUN_UNIT_TESTS=BUILD_ONLY
 
 # macOS (a.k.a OSX) support
 matrix:
diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 2d16d5394..07504e6b9 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE
 FROM ${DOCKER_IMAGE_BASE}
 
 
-# Specify defaults. This can be changed when invoking
+# Build arguments. This can be changed when invoking
 # `docker build`.
-ARG ASAN_BUILD=0
-ARG BUILD_DOCS=0
-ARG CC=gcc
-ARG CXX=g++
-ARG DOTNET_BINDINGS=1
-ARG JAVA_BINDINGS=1
-ARG NO_SUPPRESS_OUTPUT=0
-ARG PYTHON_BINDINGS=1
+ARG ASAN_BUILD
+ARG BUILD_DOCS
+ARG CC
+ARG CXX
+ARG DOTNET_BINDINGS
+ARG JAVA_BINDINGS
+ARG NO_SUPPRESS_OUTPUT
+ARG PYTHON_BINDINGS
 ARG PYTHON_EXECUTABLE=/usr/bin/python2.7
-ARG RUN_SYSTEM_TESTS=1
-ARG RUN_UNIT_TESTS=1
-ARG TARGET_ARCH=x86_64
-ARG TEST_INSTALL=1
-ARG UBSAN_BUILD=0
-ARG USE_LIBGMP=0
-ARG USE_LTO=0
-ARG USE_OPENMP=1
+ARG RUN_SYSTEM_TESTS
+ARG RUN_UNIT_TESTS
+ARG TARGET_ARCH
+ARG TEST_INSTALL
+ARG UBSAN_BUILD
+ARG USE_LIBGMP
+ARG USE_LTO
+ARG USE_OPENMP
 ARG Z3_SRC_DIR=/home/user/z3_src
-ARG Z3_BUILD_TYPE=RelWithDebInfo
-ARG Z3_CMAKE_GENERATOR=Ninja
-ARG Z3_INSTALL_PREFIX=/usr
-ARG Z3_STATIC_BUILD=0
-# Blank default indicates use latest.
+ARG Z3_BUILD_TYPE
+ARG Z3_CMAKE_GENERATOR
+ARG Z3_INSTALL_PREFIX
+ARG Z3_STATIC_BUILD
 ARG Z3_SYSTEM_TEST_GIT_REVISION
-ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY
-ARG Z3_VERBOSE_BUILD_OUTPUT=0
+ARG Z3_WARNINGS_AS_ERRORS
+ARG Z3_VERBOSE_BUILD_OUTPUT
 
 ENV \
   ASAN_BUILD=${ASAN_BUILD} \
@@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/
 
 ADD \
   /contrib/ci/scripts/build_z3_cmake.sh \
+  /contrib/ci/scripts/ci_defaults.sh \
   /contrib/ci/scripts/set_compiler_flags.sh \
   /contrib/ci/scripts/set_generator_args.sh \
   ${Z3_SRC_DIR}/contrib/ci/scripts/
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 2e117c8b1..99bbcd7a6 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -31,7 +31,7 @@ the future.
 * `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
 * `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
 * `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
-* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`)
+* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
 * `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
 * `TEST_INSTALL` - Test running `install` target (`0` or `1`)
 * `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)
@@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script
    variables (if set) into the build using the `--build-arg` argument of the `docker run`
    command.
 
-If an environemnt variable is not set a defaults value is used which can be
-found in `Dockerfiles/z3_build.Dockerfile`.
+The default values of the configuration environment variables
+can be found in
+[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh).
 
 #### Linux specific configuration variables
 
@@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`.
 
 #### Reproducing a build locally
 
-A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh`
-script and setting the appropriate environment variable.
+A build can be reproduced locally by using the
+`scripts/travis_ci_linux_entry_point.sh` script and setting the appropriate
+environment variable.
 
 For example lets say we wanted to reproduce the build below.
 
@@ -104,11 +106,43 @@ feature might be removed in the future.
 
 It may be better to just build the base image once (outside of TravisCI), upload
 it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built
-image everytime.
+image every time.
 
 An [organization](https://hub.docker.com/u/z3prover/) has been created on
 DockerHub for this.
 
 ### macOS
 
-Not yet implemented.
+For macOS we execute directly on TravisCI's macOS environment.  The entry point
+for the TravisCI builds is the
+[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh)
+scripts.
+
+#### macOS specific configuration variables
+
+* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies
+  is skipped. This is useful for local testing if the dependencies are already installed.
+* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded.
+
+#### Reproducing a build locally
+
+To reproduce a build (e.g. like the one shown below)
+
+```yaml
+- os: osx
+  osx_image: xcode8.3
+  # Note: Apple Clang does not support OpenMP
+  env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
+```
+
+Run the following:
+
+```bash
+TRAVIS_BUILD_DIR=$(pwd) \
+Z3_BUILD_TYPE=RelWithDebInfo \
+USE_OPEN_MP=0 \
+contrib/ci/scripts/travis_ci_osx_entry_point.sh
+```
+
+Note this assumes that the current working directory is the root of the Z3
+git repository.
diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh
new file mode 100644
index 000000000..d8e9376d8
--- /dev/null
+++ b/contrib/ci/scripts/ci_defaults.sh
@@ -0,0 +1,54 @@
+# This file should be sourced by other scripts
+# and not executed directly
+
+# Set CI build defaults
+
+export ASAN_BUILD="${ASAN_BUILD:-0}"
+export BUILD_DOCS="${BUILD_DOCS:-0}"
+export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
+export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
+export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
+export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
+export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
+export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
+export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
+export TEST_INSTALL="${TEST_INSTALL:-1}"
+export UBSAN_BUILD="${UBSAN_BUILD:-0}"
+export USE_LIBGMP="${USE_LIBGMP:-0}"
+export USE_LTO="${USE_LTO:-0}"
+export USE_OPENMP="${USE_OPENMP:-1}"
+
+export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
+export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
+export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
+# Default is blank which means get latest revision
+export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}"
+export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
+export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
+
+# Platform specific defaults
+PLATFORM="$(uname -s)"
+case "${PLATFORM}" in
+  Linux*)
+    export C_COMPILER="${C_COMPILER:-gcc}"
+    export CXX_COMPILER="${CXX_COMPILER:-g++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}"
+  ;;
+  Darwin*)
+    export C_COMPILER="${C_COMPILER:-clang}"
+    export CXX_COMPILER="${CXX_COMPILER:-clang++}"
+    export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
+  ;;
+  *)
+    echo "Unknown platform \"${PLATFORM}\""
+    exit 1
+  ;;
+esac
+unset PLATFORM
+
+# NOTE: The following variables are not set here because
+# they are specific to the CI implementation
+# PYTHON_EXECUTABLE
+# Z3_SRC_DIR
+# Z3_BUILD_DIR
+# Z3_SYSTEM_TEST_DIR
diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh
index 0ef7b76aa..a704c518b 100644
--- a/contrib/ci/scripts/set_generator_args.sh
+++ b/contrib/ci/scripts/set_generator_args.sh
@@ -1,4 +1,4 @@
-# This script should is intended to be included by other
+# This script is intended to be included by other
 # scripts and should not be executed directly
 
 : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"}
diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
index 666673328..e1c927f58 100755
--- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
+++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh
@@ -10,17 +10,35 @@ set -o pipefail
 : ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
 : ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
 
-if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then
-  echo "Skipping unit tests"
-  exit 0
-fi
-
 # Set CMake generator args
 source ${SCRIPT_DIR}/set_generator_args.sh
 
 cd "${Z3_BUILD_DIR}"
 
-# Build and run internal tests
-cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
-# Run all tests that don't require arguments
-run_quiet ./test-z3 /a
+function build_unit_tests() {
+  # Build internal tests
+  cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
+}
+
+function run_unit_tests() {
+  # Run all tests that don't require arguments
+  run_quiet ./test-z3 /a
+}
+
+case "${RUN_UNIT_TESTS}" in
+  BUILD_AND_RUN)
+    build_unit_tests
+    run_unit_tests
+  ;;
+  BUILD_ONLY)
+    build_unit_tests
+  ;;
+  SKIP)
+    echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run"
+    exit 0
+  ;;
+  *)
+    echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\""
+    exit 1
+  ;;
+esac
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index 84b2dd400..bd2c9d2d1 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -11,16 +11,21 @@ DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)"
 : ${LINUX_BASE?"LINUX_BASE must be specified"}
 
 
-
 # Sanity check. Current working directory should be repo root
 if [ ! -f "./README.md" ]; then
   echo "Current working directory should be repo root"
   exit 1
 fi
 
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
+
 BUILD_OPTS=()
-# Override options if they have been provided.
-# Otherwise the defaults in the Docker file will be used
+# Pass Docker build arguments
+if [ -n "${Z3_BUILD_TYPE}" ]; then
+  BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}")
+fi
+
 if [ -n "${Z3_CMAKE_GENERATOR}" ]; then
   BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}")
 fi
diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
index c5e8b4c02..ad3b0c7ab 100755
--- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh
@@ -6,26 +6,8 @@ set -x
 set -e
 set -o pipefail
 
-# Set defaults
-# FIXME: Refactor this so we don't need to stay in sync with
-# `z3_build.Dockerfile`.
-export ASAN_BUILD="${ASAN_BUILD:-0}"
-export BUILD_DOCS="${BUILD_DOCS:-0}"
-export C_COMPILER="${C_COMPILER:-clang}"
-export CXX_COMPILER="${CXX_COMPILER:-clang++}"
-export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}"
-export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
-export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
-export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
-export PYTHON_EXECUTABLE="$(which python)"
-export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
-export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
-export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
-export TEST_INSTALL="${TEST_INSTALL:-1}"
-export UBSAN_BUILD="${UBSAN_BUILD:-0}"
-export USE_LIBGMP="${USE_LIBGMP:-0}"
-export USE_LTO="${USE_LTO:-0}"
-export USE_OPENMP="${USE_OPENMP:-1}"
+# Get defaults
+source "${SCRIPT_DIR}/ci_defaults.sh"
 
 if [ -z "${TRAVIS_BUILD_DIR}" ]; then
   echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository"
@@ -37,15 +19,12 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then
   exit 1
 fi
 
+# These variables are specific to the macOS TravisCI
+# implementation and are not set in `ci_defaults.sh`.
+export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}"
 export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}"
 export Z3_BUILD_DIR="${Z3_SRC_DIR}/build"
-export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}"
-export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}"
-export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}"
-export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}"
 export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test"
-export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}"
-export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}"
 
 # Overwrite whatever what set in TravisCI
 export CC="${C_COMPILER}"
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 8938fb1b5..2200874d3 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -140,7 +140,7 @@ namespace z3 {
     class context {
         bool       m_enable_exceptions;
         Z3_context m_ctx;
-        static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
+        static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
         void init(config & c) {
             m_ctx = Z3_mk_context_rc(c);
             m_enable_exceptions = true;
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index c98307ee0..cac12413e 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) {
             compare_arrays(to_quantifier(n1)->get_decl_sorts(),
                            to_quantifier(n2)->get_decl_sorts(),
                            to_quantifier(n1)->get_num_decls()) &&
+            compare_arrays(to_quantifier(n1)->get_decl_names(),
+                           to_quantifier(n2)->get_decl_names(),
+                           to_quantifier(n1)->get_num_decls()) &&
             to_quantifier(n1)->get_expr()            == to_quantifier(n2)->get_expr() &&
             to_quantifier(n1)->get_weight()          == to_quantifier(n2)->get_weight() &&
             to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&
diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp
index 46682eed6..43035e203 100644
--- a/src/ast/expr_abstract.cpp
+++ b/src/ast/expr_abstract.cpp
@@ -19,6 +19,7 @@ Notes:
 
 #include "ast/expr_abstract.h"
 #include "util/map.h"
+#include "ast/ast_pp.h"
 
 void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
     
@@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
 void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result) {
     expr_abstractor abs(m);
     abs(base, num_bound, bound, n, result);
+    TRACE("expr_abstract",
+          tout << expr_ref(n, m) << "\n";
+          tout << result << "\n";);
 }
 
 expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
@@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app*
         }
         result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
     }
+    TRACE("expr_abstract",
+          tout << expr_ref(n, m) << "\n";
+          for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " ";
+          tout << "\n";
+          tout << result << "\n";);
     return result;
 
 }
diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index 149a59ce5..f9333c443 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -16,8 +16,9 @@ Author:
 Notes:
 
 --*/
-#include "ast/expr_substitution.h"
 #include "util/ref_util.h"
+#include "ast/expr_substitution.h"
+#include "ast/ast_pp.h"
 
 typedef obj_map<expr, proof*> expr2proof;
 typedef obj_map<expr, expr_dependency*> expr2expr_dependency;
@@ -56,6 +57,13 @@ expr_substitution::~expr_substitution() {
     reset();
 }
 
+std::ostream& expr_substitution::display(std::ostream& out) {
+    for (auto & kv : m_subst) {
+        out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(kv.m_value, m()) << "\n";
+    }
+    return out;
+}
+
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
     obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); 
     if (entry->get_data().m_value == 0) {
diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h
index d360356eb..90154d163 100644
--- a/src/ast/expr_substitution.h
+++ b/src/ast/expr_substitution.h
@@ -50,6 +50,8 @@ public:
     bool contains(expr * s);
     void reset();
     void cleanup();
+
+    std::ostream& display(std::ostream& out);
 };
 
 class scoped_expr_substitution {
@@ -84,6 +86,7 @@ public:
     bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
     bool contains(expr * s) { return m_subst.contains(s); }
     void cleanup() { m_subst.cleanup(); }
+    std::ostream& display(std::ostream& out) { return m_subst.display(out); }
 };
 
 #endif
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index f09ddcd42..13a7599a9 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1180,8 +1180,6 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
 
 void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
 
     expr * x = args[0], * y = args[1];
 
@@ -1227,8 +1225,6 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
 
 void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
 
     expr * x = args[0], *y = args[1];
 
@@ -3081,8 +3077,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     mk_is_nan(x, x_is_nan);
 
     sort * fp_srt = m.get_sort(x);
-    unsigned ebits = m_util.get_ebits(fp_srt);
-    unsigned sbits = m_util.get_sbits(fp_srt);
 
     expr_ref unspec(m);
     mk_to_ieee_bv_unspecified(f, num, args, unspec);
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 6ca8fae34..e4c294059 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -96,7 +96,7 @@ class ast_r : public ast_i {
 
  ast_r(const ast_r &other) : ast_i(other) {
         _m = other._m;
-        _m->inc_ref(_ast);
+        if (_m) _m->inc_ref(_ast);
     }
 
     ast_r &operator=(const ast_r &other) {
@@ -104,7 +104,7 @@ class ast_r : public ast_i {
             _m->dec_ref(_ast);
         _ast = other._ast;
         _m = other._m;
-        _m->inc_ref(_ast);
+        if (_m) _m->inc_ref(_ast);
         return *this;
     }
 
diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index f94558097..833c254c3 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -86,18 +86,22 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
 void model_core::unregister_decl(func_decl * d) {
     decl2expr::obj_map_entry * ec = m_interp.find_core(d);
     if (ec && ec->get_data().m_value != 0) {
-        m_manager.dec_ref(ec->get_data().m_key);
-        m_manager.dec_ref(ec->get_data().m_value);
+        auto k = ec->get_data().m_key;
+        auto v = ec->get_data().m_value;
         m_interp.remove(d);
         m_const_decls.erase(d);
+        m_manager.dec_ref(k);
+        m_manager.dec_ref(v);
         return;
     }
 
     decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
     if (ef && ef->get_data().m_value != 0) {
-        m_manager.dec_ref(ef->get_data().m_key);
-        dealloc(ef->get_data().m_value);
+        auto k = ef->get_data().m_key;
+        auto v = ef->get_data().m_value;
         m_finterp.remove(d);
         m_func_decls.erase(d);
+        m_manager.dec_ref(k);
+        dealloc(v);
     }
 }
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 7475750db..69cc4819a 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) {
 }
 tbv* tbv_manager::allocate(uint64 val) {
     tbv* v = allocate0();
-    for (unsigned bit = num_tbits(); bit > 0;) {
-        --bit;
+    for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) {
         if (val & (1ULL << bit)) {                        
             set(*v, bit, BIT_1);
         } else {
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index d38324db9..3a6d55569 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -91,21 +91,27 @@ bool expr_dominators::compute_dominators() {
     unsigned iterations = 1;
     while (change) {
         change = false;
+        TRACE("simplify", 
+              for (auto & kv : m_doms) {
+                  tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n";
+              });
+
         SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
         for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
             expr * child = m_post2expr[i];
             ptr_vector<expr> const& p = m_parents[child];
-            SASSERT(!p.empty());
             expr * new_idom = 0, *idom2 = 0;
-            for (unsigned j = 0; j < p.size(); ++j) {
-                if (!new_idom) {
-                    m_doms.find(p[j], new_idom);
-                }
-                else if (m_doms.find(p[j], idom2)) {
-                    new_idom = intersect(new_idom, idom2);
+
+            for (expr * pred : p) {
+                if (m_doms.contains(pred)) {
+                    new_idom = !new_idom ? pred : intersect(new_idom, pred);
                 }
             }
-            if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) {
+            if (!new_idom) {
+                m_doms.insert(child, p[0]);
+                change = true;
+            }
+            else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
                 m_doms.insert(child, new_idom);
                 change = true;
             }
@@ -130,6 +136,7 @@ bool expr_dominators::compile(expr * e) {
     compute_post_order();
     if (!compute_dominators()) return false;
     extract_tree();
+    TRACE("simplify", display(tout););
     return true;
 }
 
@@ -147,11 +154,31 @@ void expr_dominators::reset() {
     m_root.reset();
 }
 
+std::ostream& expr_dominators::display(std::ostream& out) {
+    return display(out, 0, m_root);
+}
+
+std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) {
+    for (unsigned i = 0; i < indent; ++i) out << " ";
+    out << expr_ref(r, m);
+    if (m_tree.contains(r)) {
+        for (expr* child : m_tree[r]) {
+            if (child != r) 
+                display(out, indent + 1, child);
+        }
+    }
+    out << "\n";
+    return out;
+}
 
 
 // -----------------------
 // dom_simplify_tactic
 
+dom_simplify_tactic::~dom_simplify_tactic() {
+    dealloc(m_simplifier);
+}
+
 tactic * dom_simplify_tactic::translate(ast_manager & m) {
     return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
 }
@@ -183,32 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
     expr * c = 0, *t = 0, *e = 0;
     VERIFY(m.is_ite(ite, c, t, e));
     unsigned old_lvl = scope_level();
-    expr_ref new_c = simplify(c);
+    expr_ref new_c = simplify_arg(c);
     if (m.is_true(new_c)) {
-        r = simplify(t);
+        r = simplify_arg(t);
     } 
     else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
-        r = simplify(e);
+        r = simplify_arg(e);
     } 
     else {
         for (expr * child : tree(ite)) {
             if (is_subexpr(child, t) && !is_subexpr(child, e)) {
-                simplify(child);
+                simplify_rec(child);
             }
         }
-
         pop(scope_level() - old_lvl);
-        expr_ref new_t = simplify(t);
+        expr_ref new_t = simplify_arg(t);
         if (!assert_expr(new_c, true)) {
             return new_t;
         }
         for (expr * child : tree(ite)) {
             if (is_subexpr(child, e) && !is_subexpr(child, t)) {
-                simplify(child);
+                simplify_rec(child);
             }
         }
         pop(scope_level() - old_lvl);
-        expr_ref new_e = simplify(e);
+        expr_ref new_e = simplify_arg(e);
         if (c == new_c && t == new_t && e == new_e) {
             r = ite;
         }
@@ -223,9 +249,22 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
     return r;
 }
 
-expr_ref dom_simplify_tactic::simplify(expr * e0) {
+expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
+    expr_ref r(m);    
+    r = get_cached(e);
+    (*m_simplifier)(r);
+    TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";);
+    return r;
+}
+
+/**
+   \brief simplify e recursively.
+*/
+expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
     expr_ref r(m);
     expr* e = 0;
+
+    TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";);
     if (!m_result.find(e0, e)) {
         e = e0;
     }
@@ -245,12 +284,12 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
     }
     else {
         for (expr * child : tree(e)) {
-            simplify(child);
+            simplify_rec(child);
         }
         if (is_app(e)) {
             m_args.reset();
             for (expr* arg : *to_app(e)) {
-                m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms?
+                m_args.push_back(simplify_arg(arg)); 
             }
             r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr());
         }
@@ -281,18 +320,30 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
     };
 
     expr_ref_vector args(m);
-    for (expr * arg : *e) {
-        for (expr * child : tree(arg)) {
-            if (is_subexpr_arg(child, arg)) {
-                simplify(child);
-            }
-        }
-        r = simplify(arg);
-        args.push_back(r);
-        if (!assert_expr(simplify(arg), !is_and)) {
-            r = is_and ? m.mk_false() : m.mk_true();
-            return r;
+    if (m_forward) {
+        for (expr * arg : *e) {
+#define _SIMP_ARG(arg)                                          \
+            for (expr * child : tree(arg)) {                    \
+                if (is_subexpr_arg(child, arg)) {               \
+                    simplify_rec(child);                        \
+                }                                               \
+            }                                                   \
+            r = simplify_arg(arg);                              \
+            args.push_back(r);                                  \
+            if (!assert_expr(r, !is_and)) {                     \
+                r = is_and ? m.mk_false() : m.mk_true();        \
+                return r;                                       \
+            }                                                   
+            _SIMP_ARG(arg);
+        }                                                                  
+    }
+    else {        
+        for (unsigned i = e->get_num_args(); i > 0; ) {
+            --i;
+            expr* arg = e->get_arg(i);
+            _SIMP_ARG(arg);
         }
+        args.reverse();
     }
     pop(scope_level() - old_lvl);
     r = is_and ? mk_and(args) : mk_or(args);
@@ -319,13 +370,15 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         change = false;
 
         // go forwards
+        m_forward = true;
         if (!init(g)) return;
         unsigned sz = g.size();
         for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
-            expr_ref r = simplify(g.form(i));
+            expr_ref r = simplify_rec(g.form(i));
             if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
                 r = m.mk_false();
             }
+            CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
             change |= r != g.form(i);
             proof* new_pr = 0;
             if (g.proofs_enabled()) {
@@ -336,15 +389,17 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         pop(scope_level());
         
         // go backwards
+        m_forward = false;
         if (!init(g)) return;
         sz = g.size();
         for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
             --i;
-            expr_ref r = simplify(g.form(i));
+            expr_ref r = simplify_rec(g.form(i));
             if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
                 r = m.mk_false();
             }
             change |= r != g.form(i);
+            CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
             proof* new_pr = 0;
             if (g.proofs_enabled()) {
                 new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0)); 
@@ -356,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
     SASSERT(scope_level() == 0);
 }
 
+/**
+   \brief determine if a is dominated by b. 
+   Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b.
+   Save intermediary results in a cache to avoid recomputations.
+*/
+
 bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
     if (a == b)
         return true;
@@ -364,14 +425,13 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
     if (m_subexpr_cache.find(a, b, r))
         return r;
 
-    for (expr * e : tree(b)) {
-        if (is_subexpr(a, e)) {
-            m_subexpr_cache.insert(a, b, true);
-            return true;
-        }
+    if (get_depth(a) >= get_depth(b)) {
+        return false;
     }
-    m_subexpr_cache.insert(a, b, false);   
-    return false;
+    SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a));
+    r = is_subexpr(idom(a), b);
+    m_subexpr_cache.insert(a, b, r);   
+    return r;
 }
 
 ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 6e5833cdb..79bc9728c 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -48,6 +48,8 @@ private:
     bool compute_dominators();
     void extract_tree();
 
+    std::ostream& display(std::ostream& out, unsigned indent, expr* r);
+
 public:
     expr_dominators(ast_manager& m): m(m), m_root(m) {}
 
@@ -55,7 +57,9 @@ public:
     bool compile(unsigned sz, expr * const* es);
     tree_t const& get_tree() { return m_tree; }
     void reset();
-    
+    expr* idom(expr *e) const { return m_doms[e]; }
+
+    std::ostream& display(std::ostream& out);
 };
 
 class dom_simplifier {
@@ -83,8 +87,6 @@ class dom_simplifier {
 };
 
 class dom_simplify_tactic : public tactic {
-public:
-private:
     ast_manager&         m;
     dom_simplifier*      m_simplifier;
     params_ref           m_params;
@@ -96,8 +98,10 @@ private:
     unsigned             m_max_depth;
     ptr_vector<expr>     m_empty;
     obj_pair_map<expr, expr, bool> m_subexpr_cache;
+    bool                 m_forward;
 
-    expr_ref simplify(expr* t);
+    expr_ref simplify_rec(expr* t);
+    expr_ref simplify_arg(expr* t);
     expr_ref simplify_ite(app * ite);
     expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); }
     expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); }
@@ -110,6 +114,7 @@ private:
     void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
 
     ptr_vector<expr> const & tree(expr * e);
+    expr* idom(expr *e) const { return m_dominators.idom(e); }
 
     unsigned scope_level() { return m_scope_level; }
     void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }
@@ -122,10 +127,10 @@ public:
         m(m), m_simplifier(s), m_params(p), 
         m_trail(m), m_args(m), 
         m_dominators(m), 
-        m_scope_level(0), m_depth(0), m_max_depth(1024) {}
+        m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
 
 
-    virtual ~dom_simplify_tactic() {}
+    virtual ~dom_simplify_tactic();
 
     virtual tactic * translate(ast_manager & m);
     virtual void updt_params(params_ref const & p) {}
diff --git a/src/util/lp/indexed_vector_instances.cpp b/src/util/lp/indexed_vector_instances.cpp
index ee078f021..79c3ee1a1 100644
--- a/src/util/lp/indexed_vector_instances.cpp
+++ b/src/util/lp/indexed_vector_instances.cpp
@@ -33,6 +33,7 @@ template void indexed_vector<unsigned>::resize(unsigned int);
 template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
 template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
 #ifdef Z3DEBUG
+template bool indexed_vector<unsigned>::is_OK() const;
 template bool indexed_vector<double>::is_OK() const;
 template bool indexed_vector<mpq>::is_OK() const;
 template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 9569ac280..7cf87b24b 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -558,14 +558,13 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
 
 template<bool SYNCH>
 void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
-    if (is_small(a) && is_small(b)) {
+    COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
+    if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
         int _a = a.m_val;
         int _b = b.m_val;
         if (_a < 0) _a = -_a;
         if (_b < 0) _b = -_b;
         unsigned r = u_gcd(_a, _b);
-        // Remark: r is (INT_MAX + 1)
-        // If a == b == INT_MIN
         set(c, r);
     }
     else {