From 3365871b258ace119a3419e8d3492fb6b79c7dcb Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Fri, 13 May 2022 15:10:17 -0700 Subject: [PATCH] add missing inf * 0 -> NaN cases --- fpmul_test.smt2 | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) 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) + ) ) ) ) -- 2.30.2