diff --git a/README-CMake.md b/README-CMake.md
index 7550808fc..715cacad2 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -266,6 +266,8 @@ The following useful options can be passed to CMake whilst configuring.
     Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
 * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
 * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
+* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors.
+    If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
@@ -381,3 +383,13 @@ It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files m
 use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake.
 
 Long story short. Don't use file globbing.
+
+### Serious warning flags
+
+By default the `WARNINGS_AS_ERRORS` flag is set to `SERIOUS_ONLY` which means
+some warnings will be treated as errors. These warnings are controlled by the
+relevant `*_WARNINGS_AS_ERRORS` list defined in
+`cmake/compiler_warnings.cmake`.
+
+Additional warnings should only be added here if the warnings has no false
+positives.
diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index e02b28b2c..183f490dd 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -1,17 +1,61 @@
+################################################################################
+# Compiler warning flags
+################################################################################
+# These are passed to relevant compiler provided they are supported
 set(GCC_AND_CLANG_WARNINGS
-    "-Wall"
+  "-Wall"
 )
 set(GCC_ONLY_WARNINGS "")
 set(CLANG_ONLY_WARNINGS "")
 set(MSVC_WARNINGS "/W3")
 
+################################################################################
+# Serious warnings
+################################################################################
+# This declares the flags that are passed to the compiler when
+# `WARNINGS_AS_ERRORS` is set to `SERIOUS_ONLY`. Only flags that are supported
+# by the compiler are used.
+#
+# In effect this a "whitelist" approach where we explicitly tell the compiler
+# which warnings we want to be treated as errors. The alternative would be a
+# "blacklist" approach where we ask the compiler to treat all warnings are
+# treated as errors but then we explicitly list which warnings which should be
+# allowed.
+#
+# The "whitelist" approach seems simpiler because we can incrementally add
+# warnings we "think are serious".
+
+# TODO: Add more warnings that are considered serious enough that we should
+# treat them as errors.
+set(GCC_AND_CLANG_WARNINGS_AS_ERRORS
+  # https://clang.llvm.org/docs/DiagnosticsReference.html#wodr
+  "-Werror=odr"
+)
+set(GCC_WARNINGS_AS_ERRORS
+  ""
+)
+set(CLANG_WARNINGS_AS_ERRORS
+  # https://clang.llvm.org/docs/DiagnosticsReference.html#wdelete-non-virtual-dtor
+  "-Werror=delete-non-virtual-dtor"
+  # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual
+  "-Werror=overloaded-virtual"
+)
+
+################################################################################
+# Test warning/error flags
+################################################################################
 set(WARNING_FLAGS_TO_CHECK "")
+set(WARNING_AS_ERROR_FLAGS_TO_CHECK "")
 if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
+  list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
+  list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS})
 elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
   list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
+  list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
+  list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS})
   # FIXME: Remove "x.." when CMP0054 is set to NEW
 elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
   list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
@@ -31,8 +75,40 @@ foreach (flag ${WARNING_FLAGS_TO_CHECK})
   z3_add_cxx_flag("${flag}")
 endforeach()
 
-option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
-if (WARNINGS_AS_ERRORS)
+# TODO: Remove this eventually.
+# Detect legacy `WARNINGS_AS_ERRORS` boolean option and covert to new
+# to new option type.
+get_property(
+  WARNINGS_AS_ERRORS_CACHE_VAR_TYPE
+  CACHE
+  WARNINGS_AS_ERRORS
+  PROPERTY
+  TYPE
+)
+if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL")
+  message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading")
+  set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}")
+  # Delete old entry
+  unset(WARNINGS_AS_ERRORS CACHE)
+else()
+  set(WARNINGS_AS_ERRORS_DEFAULT "SERIOUS_ONLY")
+endif()
+
+set(WARNINGS_AS_ERRORS
+  ${WARNINGS_AS_ERRORS_DEFAULT}
+  CACHE STRING
+  "Treat warnings as errors. ON, OFF, or SERIOUS_ONLY"
+)
+ # Set GUI options
+set_property(
+  CACHE
+  WARNINGS_AS_ERRORS
+  PROPERTY STRINGS
+  "ON;OFF;SERIOUS_ONLY"
+)
+
+if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON")
+  message(STATUS "Treating compiler warnings as errors")
   if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
     list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
     # FIXME: Remove "x.." when CMP0054 is set to NEW
@@ -41,8 +117,14 @@ if (WARNINGS_AS_ERRORS)
   else()
     message(AUTHOR_WARNING "Unknown compiler")
   endif()
-  message(STATUS "Treating compiler warnings as errors")
-else()
+elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY")
+  message(STATUS "Treating only serious compiler warnings as errors")
+  # Loop through the flags
+  foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK})
+    # Add globally because some flags need to be passed at link time.
+    z3_add_cxx_flag("${flag}" GLOBAL)
+  endforeach()
+elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF")
   message(STATUS "Not treating compiler warnings as errors")
   # FIXME: Remove "x.." when CMP0054 is set to NEW
   if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
@@ -51,4 +133,8 @@ else()
     # build system.
     list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-")
   endif()
+else()
+  message(FATAL_ERROR
+    "WARNINGS_AS_ERRORS set to unsupported value \"${WARNINGS_AS_ERRORS}\""
+  )
 endif()
diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake
index 6e756d3b9..d2624d890 100644
--- a/cmake/z3_add_cxx_flag.cmake
+++ b/cmake/z3_add_cxx_flag.cmake
@@ -2,7 +2,7 @@ include(CheckCXXCompilerFlag)
 include(CMakeParseArguments)
 
 function(z3_add_cxx_flag flag)
-  CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN})
+  CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED;GLOBAL" "" "" ${ARGN})
   string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
   string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
   string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
@@ -16,8 +16,13 @@ function(z3_add_cxx_flag flag)
   endif()
   if (HAS_${SANITIZED_FLAG_NAME})
     message(STATUS "C++ compiler supports ${flag}")
-    list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}")
-    set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE)
+    if (z3_add_flag_GLOBAL)
+      # Set globally
+      set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag} " PARENT_SCOPE)
+    else()
+      list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}")
+      set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE)
+    endif()
   else()
     message(STATUS "C++ compiler does not support ${flag}")
   endif()
diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile
index 8b922edff..2d16d5394 100644
--- a/contrib/ci/Dockerfiles/z3_build.Dockerfile
+++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile
@@ -28,6 +28,7 @@ ARG Z3_INSTALL_PREFIX=/usr
 ARG Z3_STATIC_BUILD=0
 # Blank default indicates use latest.
 ARG Z3_SYSTEM_TEST_GIT_REVISION
+ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY
 ARG Z3_VERBOSE_BUILD_OUTPUT=0
 
 ENV \
@@ -55,6 +56,7 @@ ENV \
   Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \
   Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \
   Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \
+  Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
   Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}
 
 # We add context across incrementally to maximal cache reuse
diff --git a/contrib/ci/README.md b/contrib/ci/README.md
index 31bb504b6..2e117c8b1 100644
--- a/contrib/ci/README.md
+++ b/contrib/ci/README.md
@@ -43,6 +43,7 @@ the future.
 * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
 * `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`)
 * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used.
+* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
 
 ### Linux
 
diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh
index 98a9724c7..76fd0fb84 100755
--- a/contrib/ci/scripts/build_z3_cmake.sh
+++ b/contrib/ci/scripts/build_z3_cmake.sh
@@ -20,7 +20,8 @@ set -o pipefail
 : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"}
 : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"}
 : ${USE_LTO?"USE_LTO must be specified"}
-: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX"}
+: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"}
+: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"}
 
 ADDITIONAL_Z3_OPTS=()
 
@@ -120,6 +121,7 @@ cmake \
   -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \
   -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \
   -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \
+  -DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \
   "${ADDITIONAL_Z3_OPTS[@]}" \
   "${Z3_SRC_DIR}"
 
diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
index 21b97788f..84b2dd400 100755
--- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh
+++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh
@@ -120,6 +120,13 @@ if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then
   )
 fi
 
+if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then
+  BUILD_OPTS+=( \
+    "--build-arg" \
+    "Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \
+  )
+fi
+
 case ${LINUX_BASE} in
   ubuntu_14.04)
     BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile"
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 9a1ebccf6..a16c1b92b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6054,6 +6054,24 @@ class Solver(Z3PPObject):
         """
         Z3_solver_pop(self.ctx.ref(), self.solver, num)
 
+    def num_scopes(self):
+        """Return the current number of backtracking points.
+
+        >>> s = Solver()
+        >>> s.num_scopes()
+        0L
+        >>> s.push()
+        >>> s.num_scopes()
+        1L
+        >>> s.push()
+        >>> s.num_scopes()
+        2L
+        >>> s.pop()
+        >>> s.num_scopes()
+        1L
+        """
+        return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
+
     def reset(self):
         """Remove all asserted constraints and backtracking points created using `push()`.
 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 505302dc1..8d53c9255 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -421,7 +421,7 @@ typedef enum
      It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero.
 
    - Z3_OP_BSMOD_I: Binary signed modulus.
-     It has the same semantics as Z3_OP_BSMOND, but created in a context where the second operand can be assumed to be non-zero.
+     It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero.
 
    - Z3_OP_PR_UNDEF: Undef/Null proof object.
 
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 03b4fe637..321943c72 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
         op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I));
         op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I));
         op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I));
-        op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I));
+        op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I));
 
         op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
         op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 2c0ba1ce1..99b8c5ac8 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1632,8 +1632,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
 
     res_exp = e_exp;
 
-    // Result could overflow into 4.xxx ...
-
     family_id bvfid = m_bv_util.get_fid();
     expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
     expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
@@ -1646,11 +1644,34 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
     expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
     res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
 
+    // Result could have overflown into 4.xxx.
+    SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2);
+    expr_ref ovfl_into_4(m);
+    ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs),
+                          m_bv_util.mk_numeral(1, 2));
+    dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4);
     if (sbits > 5) {
-        sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs);
-        sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
-        expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky };
-        res_sig = m_bv_util.mk_bv_or(2, res_or_args);
+        expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m);
+        sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
+        sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
+        SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4);
+        sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get());
+        sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd);
+        expr * res_or_args[2] = { sig_upper, sticky };
+        res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args);
+
+        expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m);
+        sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs);
+        sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs);
+        SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4);
+        sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get());
+        sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl);
+        expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl };
+        res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl);
+
+        res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm);
+        res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)),
+                                        res_exp);
     }
     else {
         unsigned too_short = 6 - sbits;
@@ -1658,6 +1679,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
         res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs);
     }
     dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
+    dbg_decouple("fpa2bv_fma_sig_abs", sig_abs);
+    dbg_decouple("fpa2bv_fma_res_sig", res_sig);
     SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
 
     expr_ref is_zero_sig(m), nil_sbits4(m);
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 8901c276f..525d084dc 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -32,7 +32,7 @@ namespace sat {
     void model_converter::reset() {
         m_entries.finalize();
     }
-    
+
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
         vector<entry>::const_iterator it    = m_entries.end();
@@ -46,7 +46,7 @@ namespace sat {
             literal_vector::const_iterator it2  = it->m_clauses.begin();
             literal_vector::const_iterator end2 = it->m_clauses.end();
             for (; it2 != end2; ++it2) {
-                literal l  = *it2;
+                literal l = *it2;
                 if (l == null_literal) {
                     // end of clause
                     if (!sat) {
@@ -56,6 +56,7 @@ namespace sat {
                     sat = false;
                     continue;
                 }
+
                 if (sat)
                     continue;
                 bool sign  = l.sign();
@@ -125,7 +126,7 @@ namespace sat {
         }
         return ok;
     }
-    
+
     model_converter::entry & model_converter::mk(kind k, bool_var v) {
         m_entries.push_back(entry(k, v));
         entry & e = m_entries.back();
@@ -218,7 +219,7 @@ namespace sat {
                 out << *it2;
             }
             out << ")";
-        }    
+        }
         out << ")\n";
     }
 
@@ -237,4 +238,22 @@ namespace sat {
         }
     }
 
+    unsigned model_converter::max_var(unsigned min) const {
+        unsigned result = min;
+        vector<entry>::const_iterator it = m_entries.begin();
+        vector<entry>::const_iterator end = m_entries.end();
+        for (; it != end; ++it) {
+            literal_vector::const_iterator lvit = it->m_clauses.begin();
+            literal_vector::const_iterator lvend = it->m_clauses.end();
+            for (; lvit != lvend; ++lvit) {
+                literal l = *lvit;
+                if (l != null_literal) {
+                    if (l.var() > result)
+                        result = l.var();
+                }
+            }
+        }
+        return result;
+    }
+
 };
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index b89e6e784..eb2237707 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -26,7 +26,7 @@ namespace sat {
        \brief Stores eliminated variables and Blocked clauses.
        It uses these clauses to extend/patch the model produced for the
        simplified CNF formula.
-       
+
        This information may also be used to support incremental solving.
        If new clauses are asserted into the SAT engine, then we can
        restore the state by re-asserting all clauses in the model
@@ -50,7 +50,7 @@ namespace sat {
                 m_kind(src.m_kind),
                 m_clauses(src.m_clauses) {
             }
-            bool_var var() const { return m_var; } 
+            bool_var var() const { return m_var; }
             kind get_kind() const { return static_cast<kind>(m_kind); }
         };
     private:
@@ -74,8 +74,9 @@ namespace sat {
 
         void copy(model_converter const & src);
         void collect_vars(bool_var_set & s) const;
+        unsigned max_var(unsigned min) const;
     };
-    
+
 };
 
 #endif
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 7f2b75830..fbfa0ec6b 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2628,7 +2628,7 @@ namespace sat {
         unsigned j = 0;
         for (unsigned i = 0; i < clauses.size(); ++i) {
             clause & c = *(clauses[i]);
-            if (c.contains(lit)) {
+            if (c.contains(lit) || c.contains(~lit)) {
                 detach_clause(c);
                 del_clause(c);
             }
@@ -2684,6 +2684,7 @@ namespace sat {
             w = max_var(m_clauses, w);
             w = max_var(true, w);
             w = max_var(false, w);
+            v = m_mc.max_var(w);
             for (unsigned i = 0; i < m_trail.size(); ++i) {
                 if (m_trail[i].var() > w) w = m_trail[i].var();
             }
@@ -3150,9 +3151,9 @@ namespace sat {
             }
         }
     }
-    
+
     // Algorithm 7: Corebased Algorithm with Chunking
-    
+
     static void back_remove(sat::literal_vector& lits, sat::literal l) {
         for (unsigned i = lits.size(); i > 0; ) {
             --i;
@@ -3176,7 +3177,7 @@ namespace sat {
             }
         }
     }
-    
+
     static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
         sat::literal_vector lambda;
         for (unsigned i = 0; i < vars.size(); i++) {
@@ -3375,7 +3376,7 @@ namespace sat {
         if (check_inconsistent()) return l_false;
 
         unsigned num_iterations = 0;
-        extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); 
+        extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
         update_unfixed_literals(unfixed_lits, unfixed_vars);
         while (!unfixed_lits.empty()) {
             if (scope_lvl() > 1) {
@@ -3390,7 +3391,7 @@ namespace sat {
             unsigned num_assigned = 0;
             lbool is_sat = l_true;
             for (; it != end; ++it) {
-                literal lit = *it;                
+                literal lit = *it;
                 if (value(lit) != l_undef) {
                     ++num_fixed;
                     if (lvl(lit) <= 1 && value(lit) == l_true) {
@@ -3445,8 +3446,8 @@ namespace sat {
                        << " iterations: " << num_iterations
                        << " variables: " << unfixed_lits.size()
                        << " fixed: " << conseq.size()
-                       << " status: " << is_sat 
-                       << " pre-assigned: " << num_fixed                        
+                       << " status: " << is_sat
+                       << " pre-assigned: " << num_fixed
                        << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
                        << ")\n";);
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index b6904ef02..baac9f37b 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -131,7 +131,7 @@ public:
     }
 
     bool is_literal(expr* e) const {
-        return 
+        return
             is_uninterp_const(e) ||
             (m.is_not(e, e) && is_uninterp_const(e));
     }
@@ -153,7 +153,7 @@ public:
                 asm2fml.insert(assumptions[i], assumptions[i]);
             }
         }
-        
+
         TRACE("sat", tout << _assumptions << "\n";);
         dep2asm_t dep2asm;
         m_model = 0;
@@ -163,7 +163,7 @@ public:
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
-        
+
         switch (r) {
         case l_true:
             if (sz > 0) {
@@ -280,14 +280,14 @@ public:
             return r;
         }
 
-        // build map from bound variables to 
+        // build map from bound variables to
         // the consequences that cover them.
         u_map<unsigned> bool_var2conseq;
         for (unsigned i = 0; i < lconseq.size(); ++i) {
             TRACE("sat", tout << lconseq[i] << "\n";);
             bool_var2conseq.insert(lconseq[i][0].var(), i);
         }
-        
+
         // extract original fixed variables
         u_map<expr*> asm2dep;
         extract_asm2dep(dep2asm, asm2dep);
@@ -441,7 +441,7 @@ private:
 
     lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
         for (unsigned i = 0; i < vars.size(); ++i) {
-            internalize_var(vars[i], bvars);            
+            internalize_var(vars[i], bvars);
         }
         return l_true;
     }
@@ -453,7 +453,7 @@ private:
         bool internalized = false;
         if (is_uninterp_const(v) && m.is_bool(v)) {
             sat::bool_var b = m_map.to_bool_var(v);
-            
+
             if (b != sat::null_bool_var) {
                 bvars.push_back(b);
                 internalized = true;
@@ -479,7 +479,7 @@ private:
         else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
             // variable does not occur in assertions, so is unconstrained.
         }
-        CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);        
+        CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
         return internalized;
     }
 
@@ -506,7 +506,7 @@ private:
         }
         expr_ref val(m);
         expr_ref_vector conj(m);
-        internalize_value(value, v, val);        
+        internalize_value(value, v, val);
         while (!premises.empty()) {
             expr* e = 0;
             VERIFY(asm2dep.find(premises.pop().index(), e));
diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp
index 1db3aa0a6..c36eb6dd2 100644
--- a/src/smt/cached_var_subst.cpp
+++ b/src/smt/cached_var_subst.cpp
@@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache
         return false;
     if (k1->m_num_bindings != k2->m_num_bindings)
         return false;
-    for (unsigned i = 0; i < k1->m_num_bindings; i++) 
+    for (unsigned i = 0; i < k1->m_num_bindings; i++)
         if (k1->m_bindings[i] != k2->m_bindings[i])
             return false;
     return true;
@@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
 
     new_key->m_qa           = qa;
     new_key->m_num_bindings = num_bindings;
-    for (unsigned i = 0; i < num_bindings; i++) 
+    for (unsigned i = 0; i < num_bindings; i++)
         new_key->m_bindings[i] = bindings[i]->get_owner();
-    
+
     instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0);
     if (entry->get_data().m_key != new_key) {
         SASSERT(entry->get_data().m_value != 0);
@@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
         result = entry->get_data().m_value;
         return;
     }
-    
-    m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
+
+    SASSERT(entry->get_data().m_value == 0);
+    try {
+        m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
+    }
+    catch (...) {
+        // CMW: The var_subst reducer was interrupted and m_instances is
+        // in an inconsistent state; we need to remove (new_key, 0).
+        m_instances.remove(new_key);
+        throw; // Throw on to smt::qi_queue/smt::solver.
+    }
+
     // cache result
     entry->get_data().m_value = result;
 
     // remove key from cache
     m_new_keys[num_bindings] = 0;
-    
+
     // increment reference counters
     m_refs.push_back(qa);
     for (unsigned i = 0; i < new_key->m_num_bindings; i++)
         m_refs.push_back(new_key->m_bindings[i]);
     m_refs.push_back(result);
 }
-
-
- 
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 530d0ec88..70a3041d2 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -41,7 +41,7 @@ namespace smt {
         init_parser_vars();
         m_vals.resize(15, 0.0f);
     }
-    
+
     qi_queue::~qi_queue() {
     }
 
@@ -50,7 +50,7 @@ namespace smt {
         if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
             // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
             // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
-            
+
             // using warning message instead
             warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
             // Trying again with default function
@@ -107,7 +107,7 @@ namespace smt {
         m_vals[SIZE]               = static_cast<float>(stat->get_size());
         m_vals[DEPTH]              = static_cast<float>(stat->get_depth());
         m_vals[GENERATION]         = static_cast<float>(generation);
-        m_vals[QUANT_GENERATION]   = static_cast<float>(stat->get_generation()); 
+        m_vals[QUANT_GENERATION]   = static_cast<float>(stat->get_generation());
         m_vals[WEIGHT]             = static_cast<float>(q->get_weight());
         m_vals[VARS]               = static_cast<float>(q->get_num_decls());
         m_vals[PATTERN_WIDTH]      = pat ? static_cast<float>(pat->get_num_args()) : 1.0f;
@@ -118,7 +118,7 @@ namespace smt {
         TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";);
         return stat;
     }
-    
+
     float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
         quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0);
         float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr());
@@ -132,11 +132,11 @@ namespace smt {
         float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr());
         return static_cast<unsigned>(r);
     }
-    
+
     void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
         quantifier * q         = static_cast<quantifier*>(f->get_data());
         float cost             = get_cost(q, pat, generation, min_top_generation, max_top_generation);
-        TRACE("qi_queue_detail", 
+        TRACE("qi_queue_detail",
               tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight()
               << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n";
               for (unsigned i = 0; i < f->get_num_args(); i++) {
@@ -157,7 +157,7 @@ namespace smt {
             quantifier * qa    = static_cast<quantifier*>(f->get_data());
 
             if (curr.m_cost <= m_eager_cost_threshold) {
-                instantiate(curr);    
+                instantiate(curr);
             }
             else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) {
                 // do not delay instances that produce a conflict.
@@ -193,7 +193,7 @@ namespace smt {
                 // This nasty side-effect may change the behavior of Z3.
                 m_manager.trace_stream() << " #" << bindings[i]->get_owner_id();
             }
-            
+
 #endif
             if (m_manager.proofs_enabled())
                 m_manager.trace_stream() << " #" << proof_id;
@@ -233,7 +233,7 @@ namespace smt {
         if (m_manager.is_true(s_instance)) {
             TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
 
-            if (m_manager.has_trace_stream()) 
+            if (m_manager.has_trace_stream())
                 m_manager.trace_stream() << "[end-of-instance]\n";
 
             return;
@@ -278,7 +278,7 @@ namespace smt {
                 pr1             = m_manager.mk_modus_ponens(qi_pr, rw);
             }
             else {
-                app * bare_s_lemma  = m_manager.mk_or(m_manager.mk_not(q), s_instance); 
+                app * bare_s_lemma  = m_manager.mk_or(m_manager.mk_not(q), s_instance);
                 proof * prs[1]      = { pr.get() };
                 proof * cg          = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs);
                 proof * rw          = m_manager.mk_rewrite(bare_s_lemma, lemma);
@@ -331,13 +331,13 @@ namespace smt {
         s.m_instances_lim          = m_instances.size();
         s.m_instantiated_trail_lim = m_instantiated_trail.size();
     }
-     
+
     void qi_queue::pop_scope(unsigned num_scopes) {
         unsigned new_lvl    = m_scopes.size() - num_scopes;
         scope & s           = m_scopes[new_lvl];
         unsigned old_sz     = s.m_instantiated_trail_lim;
         unsigned sz         = m_instantiated_trail.size();
-        for (unsigned i = old_sz; i < sz; i++) 
+        for (unsigned i = old_sz; i < sz; i++)
             m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false;
         m_instantiated_trail.shrink(old_sz);
         m_delayed_entries.shrink(s.m_delayed_entries_lim);
@@ -359,7 +359,7 @@ namespace smt {
     }
 
     bool qi_queue::final_check_eh() {
-        TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold 
+        TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
               << ", scope_level: " << m_context.get_scope_level() << "\n";);
         if (m_params.m_qi_conservative_final_check) {
             bool  init = false;
@@ -379,7 +379,7 @@ namespace smt {
                 entry & e       = m_delayed_entries[i];
                 TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
                 if (!e.m_instantiated && e.m_cost <= min_cost) {
-                    TRACE("qi_queue", 
+                    TRACE("qi_queue",
                           tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
                     result             = false;
                     m_instantiated_trail.push_back(i);
@@ -389,13 +389,13 @@ namespace smt {
             }
             return result;
         }
-       
+
         bool result = true;
         for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
             entry & e       = m_delayed_entries[i];
             TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
             if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold)  {
-                TRACE("qi_queue", 
+                TRACE("qi_queue",
                       tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
                 result             = false;
                 m_instantiated_trail.push_back(i);
@@ -443,7 +443,7 @@ namespace smt {
             quantifier * qa = *it2;
             delayed_qa_info info;
             qa2info.find(qa, info);
-            out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; 
+            out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";
         }
     }
 
@@ -482,6 +482,6 @@ namespace smt {
         }
 #endif
     }
-    
+
 };
 
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 10e2df988..1c8f94edf 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -135,7 +135,7 @@ namespace smt {
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
                 m_num_instances++;
             }
-            TRACE("quantifier", 
+            TRACE("quantifier",
                   tout << mk_pp(q, m()) << " ";
                   for (unsigned i = 0; i < num_bindings; ++i) {
                       tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
@@ -372,7 +372,7 @@ namespace smt {
         quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
         m_imp->~imp();
         m_imp = new (m_imp) imp(*this, ctx, p, plugin);
-        plugin->set_manager(*this);        
+        plugin->set_manager(*this);
     }
 
     void quantifier_manager::display(std::ostream & out) const {
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index 6dcf20583..96af9909a 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -75,7 +75,7 @@ namespace smt {
         };
 
         bool model_based() const;
-	bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
+        bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
         void adjust_model(proto_model * m);
         check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
 
@@ -167,7 +167,7 @@ namespace smt {
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;
 
-        
+
 
     };
 };
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index 8e8879fef..3b820de7a 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -47,10 +47,10 @@ class collect_statistics_tactic : public tactic {
 
 public:
     collect_statistics_tactic(ast_manager & m, params_ref const & p) :
-        m(m), 
+        m(m),
         m_params(p) {
-    }    
-        
+    }
+
     virtual ~collect_statistics_tactic() {}
 
     virtual tactic * translate(ast_manager & m_) {
@@ -60,21 +60,21 @@ public:
     virtual void updt_params(params_ref const & p) {
         m_params = p;
     }
-    
+
     virtual void collect_param_descrs(param_descrs & r) {}
 
     virtual void operator()(goal_ref const & g, goal_ref_buffer & result,
-                            model_converter_ref & mc, proof_converter_ref & pc, 
+                            model_converter_ref & mc, proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         mc = 0;
-        tactic_report report("collect-statistics", *g);        
-        
+        tactic_report report("collect-statistics", *g);
+
         collect_proc cp(m, m_stats);
-        expr_mark visited;                            
+        expr_mark visited;
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++)
             for_each_expr(cp, visited, g->form(i));
-        
+
         std::cout << "(" << std::endl;
         stats_type::iterator it = m_stats.begin();
         stats_type::iterator end = m_stats.end();
@@ -84,7 +84,7 @@ public:
 
         g->inc_depth();
         result.push_back(g.get());
-    }    
+    }
 
     virtual void cleanup() {}
 
@@ -98,11 +98,12 @@ protected:
     class collect_proc {
     public:
         ast_manager &            m;
-        stats_type &             m_stats;        
+        stats_type &             m_stats;
         obj_hashtable<sort>      m_seen_sorts;
         obj_hashtable<func_decl> m_seen_func_decls;
+        unsigned                 m_qdepth;
 
-        collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {}
+        collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s), m_qdepth(0) {}
 
         void operator()(var * v) {
             m_stats["bound-variables"]++;
@@ -113,7 +114,18 @@ protected:
             m_stats["quantifiers"]++;
             SASSERT(is_app(q->get_expr()));
             app * body = to_app(q->get_expr());
+            if (q->is_forall())
+                m_stats["forall-variables"] += q->get_num_decls();
+            else
+                m_stats["exists-variables"] += q->get_num_decls();
+            m_stats["patterns"] += q->get_num_patterns();
+            m_stats["no-patterns"] += q->get_num_no_patterns();
+            m_qdepth++;
+            if (m_stats.find("max-quantification-depth") == m_stats.end() ||
+                m_stats["max-quantification-depth"] < m_qdepth)
+                m_stats["max-quantification-depth"] = m_qdepth;
             this->operator()(body);
+            m_qdepth--;
         }
 
         void operator()(app * n) {
@@ -121,7 +133,7 @@ protected:
             this->operator()(n->get_decl());
         }
 
-        void operator()(sort * s) {            
+        void operator()(sort * s) {
             if (m.is_uninterp(s)) {
                 if (!m_seen_sorts.contains(s)) {
                     m_stats["uninterpreted-sorts"]++;
@@ -135,7 +147,7 @@ protected:
                 std::stringstream ss;
                 ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")";
                 m_stats[ss.str()]++;
-                
+
                 if (s->get_info()->get_num_parameters() > 0) {
                     std::stringstream ssname;
                     ssname << "(declare-sort (_ " << s->get_name() << " *))";