From 8cc3ba5a8b8ced685669d43ec315bd282a13269d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 4 Mar 2016 13:09:42 +0000
Subject: [PATCH 1/2] fixed FP Python doctest examples

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

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 3a4276dfd..088cd0d4d 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -8524,11 +8524,11 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
     >>> v = FPVal(-2.25, FPSort(8, 24))
     >>> v
     -1.125*(2**1)
-    >>> v = FPVal(-0.0, FPSort(8, 24))
+    >>> FPVal(-0.0, FPSort(8, 24))
     -0.0
-    >>> v = FPVal(0.0, FPSort(8, 24))
+    >>> FPVal(0.0, FPSort(8, 24))
     +0.0
-    >>> v = FPVal(+0.0, FPSort(8, 24))
+    >>> FPVal(+0.0, FPSort(8, 24))
     +0.0
     """
     ctx = _get_ctx(ctx)
@@ -8911,7 +8911,7 @@ def fpNEQ(a, b, ctx=None):
     >>> fpNEQ(x, y)
     Not(fpEQ(x, y))
     >>> (x != y).sexpr()
-    '(not (fp.eq x y))'
+    '(distinct x y)'
     """
     return Not(fpEQ(a, b, ctx))
 

From a51201298c2016fb4ed67372ccce84c26a797fd8 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 4 Mar 2016 14:42:38 +0000
Subject: [PATCH 2/2] Bugfix for assumptions in inc_sat_solver

---
 src/sat/sat_solver/inc_sat_solver.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 1c156d83e..7feed9fb1 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -151,6 +151,7 @@ public:
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(sz, assumptions, dep2asm);
+        SASSERT(sz == m_asms.size());
         if (r != l_true) return r;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@@ -300,6 +301,7 @@ private:
 
     lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
         if (sz == 0) {
+            m_asms.shrink(0);
             return l_true;
         }
         goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
@@ -331,6 +333,7 @@ private:
         sat::literal lit;
         for (unsigned i = 0; i < sz; ++i) {
             if (dep2asm.find(asms[i], lit)) {
+                SASSERT(lit.var() <= m_solver.num_vars());
                 m_asms.push_back(lit);
                 if (i != j && !m_weights.empty()) {
                     m_weights[j] = m_weights[i];