Test nan equality for reals as well

formalsec · Jul 28, 2024 · 2b1d34d · 2b1d34d
1 parent b47258e
commit 2b1d34d
Showing 1 changed file with 15 additions and 2 deletions.
diff --git a/test/regression/test_pr_77.ml b/test/regression/test_pr_77.ml
@@ -4,12 +4,25 @@ let () =
   let open Num in
   let nan0 = F32 (Int32.bits_of_float Float.nan) in
   let nan1 = F32 (Int32.bits_of_float Float.nan) in
+  (* Library functions ensure total order of floats. *)
   assert (Num.equal nan0 nan1)
 
 let () =
   let open Expr.Fpa in
   let nan0 = F32.v Float.nan in
   let nan1 = F32.v Float.nan in
+  (* Library functions ensure total order of floats. *)
   assert (Expr.equal nan0 nan1);
-  let eq = Expr.relop (Ty_fp 32) Eq nan0 nan1 in
-  assert (Expr.equal (Expr.simplify eq) (Expr.value False))
+  let assert_ = Expr.relop (Ty_fp 32) Eq nan0 nan1 in
+  (* Evaluation functions do not. *)
+  assert (Expr.equal (Expr.simplify assert_) (Expr.value False))
+
+let () =
+  let open Expr in
+  let nan0 = value (Real Float.nan) in
+  let nan1 = value (Real Float.nan) in
+  (* Library functions ensure total order of floats. *)
+  assert (Expr.equal nan0 nan1);
+  let assert_ = Expr.relop Ty_real Eq nan0 nan1 in
+  (* Evaluation functions do not. *)
+  assert (Expr.equal (Expr.simplify assert_) (Expr.value False))