From d1dfabbc5117734fd84c93cec7bb533109abb7ca Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Mon, 25 Dec 2023 14:31:06 +0000
Subject: [PATCH] fix #995: broken fmin/fmax semantics for -0.0/+0.0

---
 ir/instr.cpp | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/ir/instr.cpp b/ir/instr.cpp
index abbf2c9b5..10214f91f 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -848,14 +848,11 @@ StateValue FpBinOp::toSMT(State &s) const {
   case FMax:
     fn = [&](const expr &a, const expr &b, const expr &rm) {
       expr ndet = s.getFreshNondetVar("maxminnondet", true);
-      auto ndz = expr::mkIf(ndet, expr::mkNumber("0", a),
-                            expr::mkNumber("-0", a));
-
-      expr z = a.isFPZero() && b.isFPZero();
       expr cmp = op == FMin ? a.fole(b) : a.foge(b);
       return expr::mkIf(a.isNaN(), b,
                         expr::mkIf(b.isNaN(), a,
-                                   expr::mkIf(z, ndz,
+                                   expr::mkIf(a.foeq(b),
+                                              expr::mkIf(ndet, a, b),
                                               expr::mkIf(cmp, a, b))));
     };
     break;