working on implementing fma, f16 rtz formal proof seems likely to work

[ieee754fpu.git] / fpmul_test.smt2

diff --git a/fpmul_test.smt2 b/fpmul_test.smt2
index e836f4df0d3cdc31ffda7824b56b489d03e6e31f..48c218dc56347ad0bf22539b147d35e9c0371497 100644 (file)
--- a/fpmul_test.smt2
+++ b/fpmul_test.smt2
@@ -259,11 +259,9 @@
                     ; subnormals:
                     (f32_round_product_rne
                         sign
-                        (bvadd
-                            (bv48_lshr_merging
-                                norm_product
-                                (f32_sexp_to_bv48 subnormal_shift)
-                            )
+                        (bv48_lshr_merging
+                            norm_product
+                            (f32_sexp_to_bv48 subnormal_shift)
                         )
                         f32_subnormal_exponent
                         #x00
@@ -287,11 +285,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)
+                    )
                 )
             )
         )