From 6e2ca69654efae9fcddcad755aa5826448f1a8d2 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 9 Jul 2017 14:21:27 +0100
Subject: [PATCH 1/9] [CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL
 to STRING to allow a new mode `SERIOUS_ONLY`.

Modes:

`ON` - All warnings are treated as errors (same as before)
`OFF` - Warnings are not treated as errors (same as before)
`SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors.

Upgrade code is included to upgrade old CMake cache's to use the new
type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The
user's previous setting is preserved when doing this.

Very few warnings are treated as errors for now. Developers can
add more later as they see fit.
---
 README-CMake.md               | 12 +++++
 cmake/compiler_warnings.cmake | 96 +++++++++++++++++++++++++++++++++--
 cmake/z3_add_cxx_flag.cmake   | 11 ++--
 3 files changed, 111 insertions(+), 8 deletions(-)

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()

From 630863619b926e1741f195a8ad0b2dd91a4fa4ee Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 9 Jul 2017 14:41:59 +0100
Subject: [PATCH 2/9] [TravisCI] Add `Z3_WARNINGS_AS_ERRORS` environment
 variable to control the `WARNINGS_AS_ERRORS` CMake option.

---
 contrib/ci/Dockerfiles/z3_build.Dockerfile        | 2 ++
 contrib/ci/README.md                              | 1 +
 contrib/ci/scripts/build_z3_cmake.sh              | 4 +++-
 contrib/ci/scripts/travis_ci_linux_entry_point.sh | 7 +++++++
 4 files changed, 13 insertions(+), 1 deletion(-)

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"

From 0e45777104e6da51ca717d1950bd8cbb72657857 Mon Sep 17 00:00:00 2001
From: Jack Feser <feser@csail.mit.edu>
Date: Tue, 11 Jul 2017 14:41:54 -0400
Subject: [PATCH 3/9] add get_num_scopes to python solver api

---
 src/api/python/z3/z3.py | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

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()`.
 

From 89c8f1722f33556def93aa54c92c3f2e3141014e Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 12 Jul 2017 12:53:10 +0100
Subject: [PATCH 4/9] Fix typo that prevented uses of `bvsmod_i` being parsed.

---
 src/ast/bv_decl_plugin.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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));

From 5b511f12b3465fa1e2757cee3b500f524f50856a Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 12 Jul 2017 13:07:19 +0100
Subject: [PATCH 5/9] Fix minor typo in C API documentation

---
 src/api/z3_api.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
 

From da34de340d582784e0068eb6f287faa56b74a243 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 15 Jul 2017 20:25:13 +0100
Subject: [PATCH 6/9] Fixed bug in sat model converter. Fixes #1148.

---
 src/sat/sat_model_converter.cpp       | 27 +++++++++++++++++++++++----
 src/sat/sat_model_converter.h         |  7 ++++---
 src/sat/sat_solver.cpp                | 17 +++++++++--------
 src/sat/sat_solver/inc_sat_solver.cpp | 18 +++++++++---------
 4 files changed, 45 insertions(+), 24 deletions(-)

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));

From 943dc8118a3df069fb0674ca1c0b739d7f307ce7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 20 Jul 2017 13:44:47 +0100
Subject: [PATCH 7/9] Improved collect-statistics tactic

---
 src/tactic/core/collect_statistics_tactic.cpp | 40 ++++++++++++-------
 1 file changed, 26 insertions(+), 14 deletions(-)

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() << " *))";

From faa19117e40fa6850318fa777f884e65a68aae1a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 21 Jul 2017 17:42:48 +0100
Subject: [PATCH 8/9] Fixed inconsistent state upon solver interruption.
 Partially fixes #951.

---
 src/smt/cached_var_subst.cpp | 25 ++++++++++++++++---------
 src/smt/qi_queue.cpp         | 36 ++++++++++++++++++------------------
 src/smt/smt_quantifier.cpp   |  4 ++--
 src/smt/smt_quantifier.h     |  4 ++--
 4 files changed, 38 insertions(+), 31 deletions(-)

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;
 
-        
+
 
     };
 };

From 0f1583309d0813e87d6003fe46cf8bb32899d773 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 21 Jul 2017 21:12:45 +0100
Subject: [PATCH 9/9] Bugfix for fp.fma. One piece of puzzle #872.

---
 src/ast/fpa/fpa2bv_converter.cpp | 35 ++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

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);