From eee076b9f8b5d2f3347dfa4f83b64851cb2372a0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 21 May 2015 18:16:02 +0100
Subject: [PATCH] Bugfixes for fp.min, fp.max.

Fixes the fix for #68
---
 src/ast/fpa/fpa2bv_converter.cpp  | 4 ++--
 src/ast/rewriter/fpa_rewriter.cpp | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index f69f27214..1d794c898 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1072,7 +1072,7 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
     
     result = y;
     mk_ite(lt, x, result, result);
-    mk_ite(both_zero, pzero, result, result);
+    mk_ite(both_zero, y, result, result);
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
@@ -1102,7 +1102,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
 
     result = y;
     mk_ite(gt, x, result, result);
-    mk_ite(both_zero, pzero, result, result);
+    mk_ite(both_zero, y, result, result);
     mk_ite(y_is_nan, x, result, result);
     mk_ite(x_is_nan, y, result, result);
 
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index 40021e330..37c42b494 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -412,7 +412,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-        result = m_util.mk_pzero(m().get_sort(arg1));
+        result = arg2;
         return BR_DONE;
     }
 
@@ -421,7 +421,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
                         m().mk_ite(mk_eq_nan(arg2),
                         arg1,
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                        m_util.mk_pzero(m().get_sort(arg1)),
+                        arg2,
                         m().mk_ite(m_util.mk_lt(arg1, arg2),
                         arg1,
                         arg2))));
@@ -438,7 +438,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_DONE;
     }
     if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
-        result = m_util.mk_pzero(m().get_sort(arg1));
+        result = arg2;
         return BR_DONE;
     }
 
@@ -447,7 +447,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
                         m().mk_ite(mk_eq_nan(arg2),
                         arg1,
                         m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
-                        m_util.mk_pzero(m().get_sort(arg1)),
+                        arg2,
                         m().mk_ite(m_util.mk_gt(arg1, arg2),
                         arg1,
                         arg2))));