From: Jacob Lifshay <programmerjake@gmail.com>
Date: Fri, 13 May 2022 22:10:17 +0000 (-0700)
Subject: add missing inf * 0 -> NaN cases
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3365871b258ace119a3419e8d3492fb6b79c7dcb;p=ieee754fpu.git

add missing inf * 0 -> NaN cases
---

diff --git a/fpmul_test.smt2 b/fpmul_test.smt2
index e836f4df..3cb042cc 100644
--- a/fpmul_test.smt2
+++ b/fpmul_test.smt2
@@ -287,11 +287,18 @@
         (f32_into_qnan a)
         (ite (f32_is_nan b)
             (f32_into_qnan b)
-            (ite (or (f32_is_infinite a) (f32_is_infinite b))
-                (f32_infinity (bvxor (f32_sign_field a) (f32_sign_field b)))
-                (ite (or (f32_is_zero a) (f32_is_zero b))
-                    (f32_zero (bvxor (f32_sign_field a) (f32_sign_field b)))
-                    (f32_mul_nonzero_finite_rne a b)
+            (ite
+                (or
+                    (and (f32_is_zero a) (f32_is_infinite b))
+                    (and (f32_is_infinite a) (f32_is_zero b))
+                )
+                #x7FC00000
+                (ite (or (f32_is_infinite a) (f32_is_infinite b))
+                    (f32_infinity (bvxor (f32_sign_field a) (f32_sign_field b)))
+                    (ite (or (f32_is_zero a) (f32_is_zero b))
+                        (f32_zero (bvxor (f32_sign_field a) (f32_sign_field b)))
+                        (f32_mul_nonzero_finite_rne a b)
+                    )
                 )
             )
         )