Return second arg for float min/max on x86.

If both arguments are zero the second argument is returned independ from
their sign.
Bug 32640

1 files changed, 4 insertions, 4 deletions

diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index e5233ff5..7c77a488 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.v
@@ -42,14 +42,14 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
   | BI_fmin =>
       mkbuiltin_n2t Tfloat Tfloat Tfloat
         (fun f1 f2 => match Float.compare f1 f2 with
-                      | Some Eq | Some Lt => f1
-                      | Some Gt | None => f2
+                      | Some Lt => f1
+                      | Some Eq | Some Gt | None => f2
                       end)
   | BI_fmax =>
       mkbuiltin_n2t Tfloat Tfloat Tfloat
         (fun f1 f2 => match Float.compare f1 f2 with
-                      | Some Eq | Some Gt => f1
-                      | Some Lt | None => f2
+                      | Some Gt => f1
+                      | Some Eq | Some Lt | None => f2
                       end)
   end.