From 2b1d34dac14c9e80ef851584c8348b1a4cdc4e12 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Sun, 28 Jul 2024 19:10:11 +0200 Subject: [PATCH] Test nan equality for reals as well --- test/regression/test_pr_77.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/test/regression/test_pr_77.ml b/test/regression/test_pr_77.ml index 3cc7e0ea..048ead89 100644 --- 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))