fix #995: broken fmin/fmax semantics for -0.0/+0.0

AliveToolkit · Dec 25, 2023 · d1dfabb · d1dfabb
1 parent 3dbff83
commit d1dfabb
Showing 1 changed file with 2 additions and 5 deletions.
diff --git 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;