MPF min/max -+0.0 special cases changed to +0.0 instead of second arg…

…ument. Another piece of fix #68
Z3Prover · May 28, 2015 · 49a4df0 · 49a4df0
1 parent ee79b1c
commit 49a4df0
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
@@ -1229,7 +1229,11 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
 }
 
 void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
-    if (is_nan(x) || (is_zero(x) && is_zero(y)))
+    if (is_nan(x))
+        set(o, y);
+    else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
+        mk_pzero(x.ebits, x.sbits, o);
+    else if (is_zero(x) && is_zero(y))
         set(o, y);
     else if (is_nan(y))
         set(o, x);
@@ -1240,7 +1244,11 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
 }
 
 void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
-    if (is_nan(x) || (is_zero(x) && is_zero(y)))
+    if (is_nan(x))
+        set(o, y);
+    else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
+        mk_pzero(x.ebits, x.sbits, o);
+    else if (is_zero(x) && is_zero(y))
         set(o, y);
     else if (is_nan(y))
         set(o, x);