diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 3dbfbfd16ccfb3a21384371ad0801258278b0a90..78639540067dec38941768c711839f7aa662f1cc 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	math.h	1147	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc	math.h	1221	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
 tests/report	csv.c	11	main1	signed_overflow	Unknown	-2147483648 â‰¤ x * x
 tests/report	csv.c	11	main1	signed_overflow	Unknown	x * x â‰¤ 2147483647
 tests/report	csv.c	12	main1	index_bound	Unknown	0 â‰¤ x
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 2596ed249ede591884191af9e518229af9617054..0bfa1f9130fbc00df81f808ee1d5baf905f2578d 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2807,6 +2807,147 @@
             default behavior
             by Frama-C kernel.
 
+--------------------------------------------------------------------------------
+--- Properties of Function 'tan'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition for 'zero' 'zero_res'
+            ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'zero' 'no_error'
+            ensures no_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'result_not_nan'
+            ensures result_not_nan: Â¬\is_NaN(\result)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'maybe_error'
+            ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns (file share/libc/math.h, line 471)
+            assigns __fc_errno, \result;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'finite_non_zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 471)
+            assigns __fc_errno \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 471)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'finite_non_zero' (file share/libc/math.h, line 479)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'zero' (file share/libc/math.h, line 474)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+[  Valid  ] Behavior 'finite_non_zero'
+            behavior finite_non_zero
+            by Frama-C kernel.
+[  Valid  ] Behavior 'zero'
+            behavior zero
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'tanf'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition for 'zero' 'zero_res'
+            ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'zero' 'no_error'
+            ensures no_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'result_not_nan'
+            ensures result_not_nan: Â¬\is_NaN(\result)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'maybe_error'
+            ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns (file share/libc/math.h, line 497)
+            assigns __fc_errno, \result;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'finite_non_zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 497)
+            assigns __fc_errno \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 497)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'finite_non_zero' (file share/libc/math.h, line 505)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'zero' (file share/libc/math.h, line 500)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+[  Valid  ] Behavior 'finite_non_zero'
+            behavior finite_non_zero
+            by Frama-C kernel.
+[  Valid  ] Behavior 'zero'
+            behavior zero
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'tanl'
+--------------------------------------------------------------------------------
+
+[ Extern  ] Post-condition for 'zero' 'zero_res'
+            ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'zero' 'no_error'
+            ensures no_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'result_not_nan'
+            ensures result_not_nan: Â¬\is_NaN(\result)
+            Unverifiable but considered Valid.
+[ Extern  ] Post-condition for 'finite_non_zero' 'maybe_error'
+            ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno)
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns (file share/libc/math.h, line 523)
+            assigns __fc_errno, \result;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'finite_non_zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Assigns for 'zero' nothing
+            assigns \nothing;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 523)
+            assigns __fc_errno \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms (file share/libc/math.h, line 523)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'finite_non_zero' (file share/libc/math.h, line 531)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[ Extern  ] Froms for 'zero' (file share/libc/math.h, line 526)
+            assigns \result \from x;
+            Unverifiable but considered Valid.
+[  Valid  ] Default behavior
+            default behavior
+            by Frama-C kernel.
+[  Valid  ] Behavior 'finite_non_zero'
+            behavior finite_non_zero
+            by Frama-C kernel.
+[  Valid  ] Behavior 'zero'
+            behavior zero
+            by Frama-C kernel.
+
 --------------------------------------------------------------------------------
 --- Properties of Function 'acosh'
 --------------------------------------------------------------------------------
@@ -2820,7 +2961,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 478)
+[ Extern  ] Froms (file share/libc/math.h, line 552)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2840,7 +2981,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 504)
+[ Extern  ] Froms (file share/libc/math.h, line 578)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2860,7 +3001,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 530)
+[ Extern  ] Froms (file share/libc/math.h, line 604)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2892,7 +3033,7 @@
 [ Extern  ] Post-condition for 'minus_infinity' 'no_error'
             ensures no_error: __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 573)
+[ Extern  ] Assigns (file share/libc/math.h, line 647)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'minus_infinity' nothing
@@ -2901,16 +3042,16 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 573)
+[ Extern  ] Froms (file share/libc/math.h, line 647)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 573)
+[ Extern  ] Froms (file share/libc/math.h, line 647)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'minus_infinity' (file share/libc/math.h, line 596)
+[ Extern  ] Froms for 'minus_infinity' (file share/libc/math.h, line 670)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 577)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 651)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2951,7 +3092,7 @@
 [ Extern  ] Post-condition for 'minus_infinity' 'no_error'
             ensures no_error: __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 610)
+[ Extern  ] Assigns (file share/libc/math.h, line 684)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'minus_infinity' nothing
@@ -2960,16 +3101,16 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 610)
+[ Extern  ] Froms (file share/libc/math.h, line 684)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 610)
+[ Extern  ] Froms (file share/libc/math.h, line 684)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'minus_infinity' (file share/libc/math.h, line 633)
+[ Extern  ] Froms for 'minus_infinity' (file share/libc/math.h, line 707)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 614)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 688)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3010,13 +3151,13 @@
 [ Extern  ] Post-condition for 'zero' 'zero_exp'
             ensures zero_exp: *\old(exp) â‰¡ 0
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 658)
+[ Extern  ] Assigns (file share/libc/math.h, line 732)
             assigns \result, *exp;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 658)
+[ Extern  ] Froms (file share/libc/math.h, line 732)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 658)
+[ Extern  ] Froms (file share/libc/math.h, line 732)
             assigns *exp \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3054,13 +3195,13 @@
 [ Extern  ] Post-condition for 'zero' 'zero_exp'
             ensures zero_exp: *\old(exp) â‰¡ 0
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 685)
+[ Extern  ] Assigns (file share/libc/math.h, line 759)
             assigns \result, *exp;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 685)
+[ Extern  ] Froms (file share/libc/math.h, line 759)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 685)
+[ Extern  ] Froms (file share/libc/math.h, line 759)
             assigns *exp \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3098,13 +3239,13 @@
 [ Extern  ] Post-condition for 'zero' 'zero_exp'
             ensures zero_exp: *\old(exp) â‰¡ 0
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 712)
+[ Extern  ] Assigns (file share/libc/math.h, line 786)
             assigns \result, *exp;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 712)
+[ Extern  ] Froms (file share/libc/math.h, line 786)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 712)
+[ Extern  ] Froms (file share/libc/math.h, line 786)
             assigns *exp \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3128,13 +3269,13 @@
             ensures
             __fc_errno: __fc_errno â‰¡ 34 âˆ¨ __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 742)
+[ Extern  ] Assigns (file share/libc/math.h, line 816)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 742)
+[ Extern  ] Froms (file share/libc/math.h, line 816)
             assigns __fc_errno \from x, exp;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 742)
+[ Extern  ] Froms (file share/libc/math.h, line 816)
             assigns \result \from x, exp;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3152,13 +3293,13 @@
             ensures
             __fc_errno: __fc_errno â‰¡ 34 âˆ¨ __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 762)
+[ Extern  ] Assigns (file share/libc/math.h, line 836)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 762)
+[ Extern  ] Froms (file share/libc/math.h, line 836)
             assigns __fc_errno \from x, exp;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 762)
+[ Extern  ] Froms (file share/libc/math.h, line 836)
             assigns \result \from x, exp;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3178,7 +3319,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 788)
+[ Extern  ] Froms (file share/libc/math.h, line 862)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3198,7 +3339,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 819)
+[ Extern  ] Froms (file share/libc/math.h, line 893)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3218,7 +3359,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 850)
+[ Extern  ] Froms (file share/libc/math.h, line 924)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3238,7 +3379,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 881)
+[ Extern  ] Froms (file share/libc/math.h, line 955)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3258,7 +3399,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 912)
+[ Extern  ] Froms (file share/libc/math.h, line 986)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3278,7 +3419,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 943)
+[ Extern  ] Froms (file share/libc/math.h, line 1017)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3298,7 +3439,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 978)
+[ Extern  ] Froms (file share/libc/math.h, line 1052)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3318,7 +3459,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1009)
+[ Extern  ] Froms (file share/libc/math.h, line 1083)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3338,7 +3479,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1040)
+[ Extern  ] Froms (file share/libc/math.h, line 1114)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3363,7 +3504,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1087)
+[ Extern  ] Froms (file share/libc/math.h, line 1161)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3388,7 +3529,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1105)
+[ Extern  ] Froms (file share/libc/math.h, line 1179)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3413,7 +3554,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1123)
+[ Extern  ] Froms (file share/libc/math.h, line 1197)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3431,13 +3572,13 @@
             ensures
             __fc_errno: __fc_errno â‰¡ 34 âˆ¨ __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 1145)
+[ Extern  ] Assigns (file share/libc/math.h, line 1219)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1145)
+[ Extern  ] Froms (file share/libc/math.h, line 1219)
             assigns __fc_errno \from x, y;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1145)
+[ Extern  ] Froms (file share/libc/math.h, line 1219)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3455,13 +3596,13 @@
             ensures
             __fc_errno: __fc_errno â‰¡ 34 âˆ¨ __fc_errno â‰¡ \old(__fc_errno)
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 1160)
+[ Extern  ] Assigns (file share/libc/math.h, line 1234)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1160)
+[ Extern  ] Froms (file share/libc/math.h, line 1234)
             assigns __fc_errno \from x, y;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1160)
+[ Extern  ] Froms (file share/libc/math.h, line 1234)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3493,7 +3634,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1181)
+[ Extern  ] Froms (file share/libc/math.h, line 1255)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3519,7 +3660,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1210)
+[ Extern  ] Froms (file share/libc/math.h, line 1284)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3542,7 +3683,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1239)
+[ Extern  ] Froms (file share/libc/math.h, line 1313)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3559,7 +3700,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1279)
+[ Extern  ] Froms (file share/libc/math.h, line 1353)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3576,7 +3717,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1296)
+[ Extern  ] Froms (file share/libc/math.h, line 1370)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3593,7 +3734,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1313)
+[ Extern  ] Froms (file share/libc/math.h, line 1387)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3610,7 +3751,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1330)
+[ Extern  ] Froms (file share/libc/math.h, line 1404)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3627,7 +3768,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1347)
+[ Extern  ] Froms (file share/libc/math.h, line 1421)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3644,7 +3785,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1364)
+[ Extern  ] Froms (file share/libc/math.h, line 1438)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3661,7 +3802,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1397)
+[ Extern  ] Froms (file share/libc/math.h, line 1471)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3678,7 +3819,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1414)
+[ Extern  ] Froms (file share/libc/math.h, line 1488)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3695,7 +3836,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1431)
+[ Extern  ] Froms (file share/libc/math.h, line 1505)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3712,7 +3853,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1456)
+[ Extern  ] Froms (file share/libc/math.h, line 1530)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3729,7 +3870,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1473)
+[ Extern  ] Froms (file share/libc/math.h, line 1547)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3746,7 +3887,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1490)
+[ Extern  ] Froms (file share/libc/math.h, line 1564)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3766,7 +3907,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1510)
+[ Extern  ] Froms (file share/libc/math.h, line 1584)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3786,7 +3927,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1531)
+[ Extern  ] Froms (file share/libc/math.h, line 1605)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3803,7 +3944,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1564)
+[ Extern  ] Froms (file share/libc/math.h, line 1638)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3820,7 +3961,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1571)
+[ Extern  ] Froms (file share/libc/math.h, line 1645)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3837,7 +3978,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1578)
+[ Extern  ] Froms (file share/libc/math.h, line 1652)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3857,7 +3998,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1608)
+[ Extern  ] Froms (file share/libc/math.h, line 1682)
             assigns \result \from f;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3883,7 +4024,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1621)
+[ Extern  ] Froms (file share/libc/math.h, line 1695)
             assigns \result \from d;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3906,7 +4047,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1648)
+[ Extern  ] Froms (file share/libc/math.h, line 1722)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3923,7 +4064,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 1654)
+[ Extern  ] Froms (file share/libc/math.h, line 1728)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -4285,9 +4426,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   184 Completely validated
+   193 Completely validated
     16 Locally validated
-   534 Considered valid
+   567 Considered valid
     56 To be validated
-   790 Total
+   832 Total
 --------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e78d1082652406952488171029bc8f3bcd957daf..52ea02c4ae31933fef4f719db82c1493a10b18a3 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -46,7 +46,7 @@
    wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
    wmemset (0 call); 
   
-  Specified-only functions (423)
+  Specified-only functions (426)
   ==============================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -163,17 +163,18 @@
    strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
    strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
    sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
-   tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
-   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
-   truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
-   umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
-   usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
-   vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
-   vsyslog (0 call); wait (0 call); waitpid (0 call); wcscasecmp (0 call);
-   wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
-   wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
-   wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
-   wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call); 
+   tan (0 call); tanf (0 call); tanl (0 call); tcflush (0 call);
+   tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
+   tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
+   truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
+   uname (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
+   utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
+   vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
+   wait (0 call); waitpid (0 call); wcscasecmp (0 call); wcschr (0 call);
+   wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+   wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+   wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+   wmemcmp (0 call); wmemmove (0 call); write (0 call); 
   
   Undefined and unspecified functions (1)
   =======================================
@@ -202,7 +203,7 @@
   Goto = 112
   Assignment = 618
   Exit point = 99
-  Function = 523
+  Function = 526
   Function call = 141
   Pointer dereferencing = 249
   Cyclomatic complexity = 369
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6bc8c7e7ed63a16dde73c5e20be6b47b952ab5ce..abbb75a19d6c1d2882b1f32247232afd0bd23edb 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3758,6 +3758,81 @@ extern float sinf(float x);
  */
 extern long double sinl(long double x);
 
+/*@ requires Â¬(infinite_arg: \is_infinite(x));
+    requires Â¬(nan_arg: \is_NaN(x));
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+    
+    behavior zero:
+      assumes zero_arg: \is_finite(x) âˆ§ x â‰¡ 0.;
+      ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x);
+      ensures no_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    behavior finite_non_zero:
+      assumes finite_arg: \is_finite(x) âˆ§ x â‰¢ 0.;
+      ensures result_not_nan: Â¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern double tan(double x);
+
+/*@ requires Â¬(infinite_arg: \is_infinite(x));
+    requires Â¬(nan_arg: \is_NaN(x));
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+    
+    behavior zero:
+      assumes zero_arg: \is_finite(x) âˆ§ x â‰¡ 0.;
+      ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x);
+      ensures no_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    behavior finite_non_zero:
+      assumes finite_arg: \is_finite(x) âˆ§ x â‰¢ 0.;
+      ensures result_not_nan: Â¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern float tanf(float x);
+
+/*@ requires Â¬(infinite_arg: \is_infinite(x));
+    requires Â¬(nan_arg: \is_NaN(x));
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from x;
+    assigns \result \from x;
+    
+    behavior zero:
+      assumes zero_arg: \is_finite(x) âˆ§ x â‰¡ 0.;
+      ensures zero_res: \is_finite(\result) âˆ§ \result â‰¡ \old(x);
+      ensures no_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    behavior finite_non_zero:
+      assumes finite_arg: \is_finite(x) âˆ§ x â‰¢ 0.;
+      ensures result_not_nan: Â¬\is_NaN(\result);
+      ensures maybe_error: __fc_errno â‰¡ \old(__fc_errno);
+      assigns \result;
+      assigns \result \from x;
+    
+    complete behaviors finite_non_zero, zero;
+    disjoint behaviors finite_non_zero, zero;
+ */
+extern long double tanl(long double x);
+
 /*@ requires in_domain: \is_finite(x) âˆ§ x â‰¥ 1;
     ensures positive_result: \is_finite(\result) âˆ§ \result â‰¥ 0;
     ensures no_error: __fc_errno â‰¡ \old(__fc_errno);
diff --git a/tests/libc/oracle/math_h.0.res.oracle b/tests/libc/oracle/math_h.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6270a1a96a98be26db438a332ddd1f738ebc5a9c
--- /dev/null
+++ b/tests/libc/oracle/math_h.0.res.oracle
@@ -0,0 +1,719 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning: 
+  Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  pi âˆˆ {3.14159265359}
+  half_pi âˆˆ {1.57079632679}
+  e âˆˆ {2.71828182846}
+  top âˆˆ [--..--]
+  f_pi âˆˆ {3.14159274101}
+  f_half_pi âˆˆ {1.57079637051}
+  f_e âˆˆ {2.71828174591}
+  f_top âˆˆ [--..--]
+  ld_pi âˆˆ [3.14159265359 .. 3.14159265359]
+  ld_half_pi âˆˆ [1.57079632679 .. 1.57079632679]
+  ld_e âˆˆ {2.71828182846}
+  ld_top âˆˆ [--..--]
+  zero âˆˆ {0}
+  minus_zero âˆˆ {-0.}
+  one âˆˆ {1.}
+  minus_one âˆˆ {-1.}
+  large âˆˆ {1e+38}
+  f_pos_inf âˆˆ {inf}
+  pos_inf âˆˆ {inf}
+  ld_pos_inf âˆˆ {inf}
+  f_neg_inf âˆˆ {-inf}
+  neg_inf âˆˆ {-inf}
+  ld_neg_inf âˆˆ {-inf}
+  infinity âˆˆ {inf}
+  fp_ilogb0 âˆˆ {-2147483648.}
+  fp_ilogbnan âˆˆ {-2147483648.}
+  int_top âˆˆ [--..--]
+  nondet âˆˆ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] using specification for function ldexp
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:108.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:109: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:111: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:112.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:112.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:113: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:115: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:116.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:117: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:119.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:121: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_errno âˆˆ [--..--]
+  exponent âˆˆ [--..--] or UNINITIALIZED
+  r âˆˆ {0}
+  __retres âˆˆ {0}
diff --git a/tests/libc/oracle/math_h.1.res.oracle b/tests/libc/oracle/math_h.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7b044ea68c6299473004aae7f4040ab276e96016
--- /dev/null
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -0,0 +1,1110 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning: 
+  Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  pi âˆˆ {3.14159265359}
+  half_pi âˆˆ {1.57079632679}
+  e âˆˆ {2.71828182846}
+  top âˆˆ [--..--]
+  f_pi âˆˆ {3.14159274101}
+  f_half_pi âˆˆ {1.57079637051}
+  f_e âˆˆ {2.71828174591}
+  f_top âˆˆ [--..--]
+  ld_pi âˆˆ [3.14159265359 .. 3.14159265359]
+  ld_half_pi âˆˆ [1.57079632679 .. 1.57079632679]
+  ld_e âˆˆ {2.71828182846}
+  ld_top âˆˆ [--..--]
+  zero âˆˆ {0}
+  minus_zero âˆˆ {-0.}
+  one âˆˆ {1.}
+  minus_one âˆˆ {-1.}
+  large âˆˆ {1e+38}
+  f_pos_inf âˆˆ {inf}
+  pos_inf âˆˆ {inf}
+  ld_pos_inf âˆˆ {inf}
+  f_neg_inf âˆˆ {-inf}
+  neg_inf âˆˆ {-inf}
+  ld_neg_inf âˆˆ {-inf}
+  infinity âˆˆ {inf}
+  fp_ilogb0 âˆˆ {-2147483648.}
+  fp_ilogbnan âˆˆ {-2147483648.}
+  int_top âˆˆ [--..--]
+  nondet âˆˆ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  function atan: precondition 'number_arg' got status unknown.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  function atanf: precondition 'number_arg' got status unknown.
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  NaN long double value. assert Â¬\is_NaN(ld_top);
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  NaN long double value. assert Â¬\is_NaN(ld_top);
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabs: precondition got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsf: precondition got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: function fabsl: precondition got status valid.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  NaN long double value. assert Â¬\is_NaN(ld_top);
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: no state left, precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva:alarm] tests/libc/math_h.c:90: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva:alarm] tests/libc/math_h.c:91: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva:alarm] tests/libc/math_h.c:92: Warning: 
+  NaN long double value. assert Â¬\is_NaN(ld_top);
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] using specification for function ldexp
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:93: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:94: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:96: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:97: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:99: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:100: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  NaN double value. assert Â¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102: function ldexp: precondition got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  NaN float value. assert Â¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103: function ldexpf: precondition got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:108.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:109: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:111: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:112.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:112.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:113: assertion got status valid.
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+  Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:115: assertion got status valid.
+[eva] computing for function __finitef <- main.
+  Called from tests/libc/math_h.c:116.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:117: assertion got status valid.
+[eva] tests/libc/math_h.c:121: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[scope:rm_asserts] removing 1 assertion(s)
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_errno âˆˆ [--..--]
+  exponent âˆˆ [--..--] or UNINITIALIZED
+  r âˆˆ {0}
+  __retres âˆˆ {0}
diff --git a/tests/libc/oracle/math_h.2.res.oracle b/tests/libc/oracle/math_h.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2c5443e6086f72eadb95e0f251ae0cb3be6906b3
--- /dev/null
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -0,0 +1,1188 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning: 
+  Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  pi âˆˆ {3.14159265359}
+  half_pi âˆˆ {1.57079632679}
+  e âˆˆ {2.71828182846}
+  top âˆˆ [--..--]
+  f_pi âˆˆ {3.14159274101}
+  f_half_pi âˆˆ {1.57079637051}
+  f_e âˆˆ {2.71828174591}
+  f_top âˆˆ [--..--]
+  ld_pi âˆˆ [3.14159265359 .. 3.14159265359]
+  ld_half_pi âˆˆ [1.57079632679 .. 1.57079632679]
+  ld_e âˆˆ {2.71828182846}
+  ld_top âˆˆ [--..--]
+  zero âˆˆ {0}
+  minus_zero âˆˆ {-0.}
+  one âˆˆ {1.}
+  minus_one âˆˆ {-1.}
+  large âˆˆ {1e+38}
+  fp_ilogb0 âˆˆ {-2147483648.}
+  fp_ilogbnan âˆˆ {-2147483648.}
+  int_top âˆˆ [--..--]
+  nondet âˆˆ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: 
+  function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  function atan: precondition 'number_arg' got status unknown.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: 
+  function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  function atanf: precondition 'number_arg' got status unknown.
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva:alarm] tests/libc/math_h.c:86: Warning: 
+  non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function atanl <- main.
+  Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86: 
+  function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function fabs <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function fabsf <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87: 
+  function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function fabsl <- main.
+  Called from tests/libc/math_h.c:87.
+[eva:alarm] tests/libc/math_h.c:87: Warning: 
+  function fabsl: precondition 'finite_arg' got status unknown.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function tan <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tan: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function tanf <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function tanl <- main.
+  Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning: 
+  function tanl: precondition Â¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88: 
+  function tanl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva:alarm] tests/libc/math_h.c:90: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(infinite_arg:
+                                    \is_plus_infinity(x) âˆ¨
+                                    \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90: 
+  function frexp: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+  Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva:alarm] tests/libc/math_h.c:91: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function frexpf <- main.
+  Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91: 
+  function frexpf: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva:alarm] tests/libc/math_h.c:92: Warning: 
+  non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function frexpl <- main.
+  Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition 'valid_exp' got status valid.
+[eva:alarm] tests/libc/math_h.c:92: Warning: 
+  function frexpl: precondition Â¬(infinite_arg:
+                                     \is_plus_infinity(x) âˆ¨
+                                     \is_minus_infinity(x)) got status unknown.
+[eva] tests/libc/math_h.c:92: 
+  function frexpl: precondition Â¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] using specification for function ldexp
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:93: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:93.
+[eva:alarm] tests/libc/math_h.c:93: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva:alarm] tests/libc/math_h.c:94: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:94: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:94.
+[eva:alarm] tests/libc/math_h.c:94: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:96: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:97: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:99: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99: 
+  function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:100: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100: 
+  function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+  Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning: 
+  function ldexp: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+  Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning: 
+  function ldexpf: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexpf
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_errno âˆˆ [--..--]
+  exponent âˆˆ [--..--] or UNINITIALIZED
+  __retres âˆˆ {0}
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
deleted file mode 100644
index 098f41b2d50485bb9e2598d9aba1d05d10190ce3..0000000000000000000000000000000000000000
--- a/tests/libc/oracle/math_h.res.oracle
+++ /dev/null
@@ -1,903 +0,0 @@
-[kernel] Parsing tests/libc/math_h.c (with preprocessing)
-[kernel:parser:decimal-float] tests/libc/math_h.c:6: Warning: 
-  Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
-  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  pi âˆˆ {3.14159265359}
-  half_pi âˆˆ {1.57079632679}
-  e âˆˆ {2.71828182846}
-  top âˆˆ [--..--]
-  f_pi âˆˆ {3.14159274101}
-  f_half_pi âˆˆ {1.57079637051}
-  f_e âˆˆ {2.71828174591}
-  f_top âˆˆ [--..--]
-  ld_pi âˆˆ [3.14159265359 .. 3.14159265359]
-  ld_half_pi âˆˆ [1.57079632679 .. 1.57079632679]
-  ld_e âˆˆ {2.71828182846}
-  ld_top âˆˆ [--..--]
-  zero âˆˆ {0}
-  minus_zero âˆˆ {-0.}
-  one âˆˆ {1.}
-  minus_one âˆˆ {-1.}
-  large âˆˆ {1e+38}
-  huge_val âˆˆ {inf}
-  huge_valf âˆˆ {inf}
-  huge_vall âˆˆ {inf}
-  infinity âˆˆ {inf}
-  fp_ilogb0 âˆˆ {-2147483648.}
-  fp_ilogbnan âˆˆ {-2147483648.}
-  int_top âˆˆ [--..--]
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:61: Call to builtin atan
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] tests/libc/math_h.c:62: Call to builtin atanf
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] using specification for function atanl
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:63.
-[eva] Done for function atanl
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] using specification for function fabs
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:64.
-[eva] Done for function fabs
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] using specification for function fabsf
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] using specification for function fabsl
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:66.
-[eva] Done for function fabsl
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] using specification for function frexp
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexp <- main.
-  Called from tests/libc/math_h.c:68.
-[eva] tests/libc/math_h.c:68: 
-  function frexp: precondition 'valid_exp' got status valid.
-[eva] Done for function frexp
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] using specification for function frexpf
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpf <- main.
-  Called from tests/libc/math_h.c:69.
-[eva] tests/libc/math_h.c:69: 
-  function frexpf: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpf
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] using specification for function frexpl
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function frexpl <- main.
-  Called from tests/libc/math_h.c:70.
-[eva] tests/libc/math_h.c:70: 
-  function frexpl: precondition 'valid_exp' got status valid.
-[eva] Done for function frexpl
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] using specification for function ldexp
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:71.
-[eva] Done for function ldexp
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] using specification for function ldexpf
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:72.
-[eva] Done for function ldexpf
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:74.
-[eva] Done for function ldexp
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:75.
-[eva] Done for function ldexpf
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:77.
-[eva] Done for function ldexp
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:78.
-[eva] Done for function ldexpf
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexp <- main.
-  Called from tests/libc/math_h.c:80.
-[eva] Done for function ldexp
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function ldexpf <- main.
-  Called from tests/libc/math_h.c:81.
-[eva] Done for function ldexpf
-[eva] computing for function __finite <- main.
-  Called from tests/libc/math_h.c:86.
-[eva] using specification for function __finite
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:87: assertion got status valid.
-[eva] computing for function __finite <- main.
-  Called from tests/libc/math_h.c:88.
-[eva] Done for function __finite
-[eva] computing for function __finite <- main.
-  Called from tests/libc/math_h.c:88.
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:89: assertion got status valid.
-[eva] computing for function __finitef <- main.
-  Called from tests/libc/math_h.c:90.
-[eva] using specification for function __finitef
-[eva] Done for function __finitef
-[eva] computing for function __finitef <- main.
-  Called from tests/libc/math_h.c:90.
-[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:91: assertion got status valid.
-[eva] computing for function __finite <- main.
-  Called from tests/libc/math_h.c:92.
-[eva] Done for function __finite
-[eva] computing for function __finite <- main.
-  Called from tests/libc/math_h.c:92.
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:93: assertion got status valid.
-[eva] computing for function __finitef <- main.
-  Called from tests/libc/math_h.c:94.
-[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:95: assertion got status valid.
-[eva] computing for function __finitef <- main.
-  Called from tests/libc/math_h.c:96.
-[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:97: assertion got status valid.
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
-  __fc_errno âˆˆ [--..--]
-  atan_pi âˆˆ {1.26262725568}
-  atan_half_pi âˆˆ {1.00388482185}
-  atan_e âˆˆ {1.21828290502}
-  atan_zero âˆˆ {0}
-  atan_minus_zero âˆˆ {-0.}
-  atan_one âˆˆ {0.785398163397}
-  atan_minus_one âˆˆ {-0.785398163397}
-  atan_large âˆˆ {1.57079632679}
-  atan_top âˆˆ [-1.57079632679 .. 1.57079632679] âˆª {NaN}
-  atanf_f_pi âˆˆ {1.262627}
-  atanf_f_half_pi âˆˆ {1.003884}
-  atanf_f_e âˆˆ {1.218282}
-  atanf_zero âˆˆ {0}
-  atanf_minus_zero âˆˆ {-0.}
-  atanf_one âˆˆ {0.785398}
-  atanf_minus_one âˆˆ {-0.785398}
-  atanf_large âˆˆ {1.570796}
-  atanf_f_top âˆˆ [-1.570796 .. 1.570796] âˆª {NaN}
-  atanl_ld_pi âˆˆ [-inf .. inf]
-  atanl_ld_half_pi âˆˆ [-inf .. inf]
-  atanl_ld_e âˆˆ [-inf .. inf]
-  atanl_zero âˆˆ [-inf .. inf]
-  atanl_minus_zero âˆˆ [-inf .. inf]
-  atanl_one âˆˆ [-inf .. inf]
-  atanl_minus_one âˆˆ [-inf .. inf]
-  atanl_large âˆˆ [-inf .. inf]
-  atanl_ld_top âˆˆ [-inf .. inf] âˆª {NaN}
-  fabs_pi âˆˆ {3.14159265359}
-  fabs_half_pi âˆˆ {1.57079632679}
-  fabs_e âˆˆ {2.71828182846}
-  fabs_zero âˆˆ [-0. .. 0.]
-  fabs_minus_zero âˆˆ [-0. .. 0.]
-  fabs_one âˆˆ {1.}
-  fabs_minus_one âˆˆ {1.}
-  fabs_large âˆˆ {1e+38}
-  fabs_top âˆˆ [-0. .. inf] âˆª {NaN}
-  fabsf_f_pi âˆˆ {3.14159274101}
-  fabsf_f_half_pi âˆˆ {1.57079637051}
-  fabsf_f_e âˆˆ {2.71828174591}
-  fabsf_zero âˆˆ [-0. .. 0.]
-  fabsf_minus_zero âˆˆ [-0. .. 0.]
-  fabsf_one âˆˆ {1.}
-  fabsf_minus_one âˆˆ {1.}
-  fabsf_large âˆˆ {9.99999968029e+37}
-  fabsf_f_top âˆˆ [-0. .. inf] âˆª {NaN}
-  fabsl_ld_pi âˆˆ [-inf .. inf]
-  fabsl_ld_half_pi âˆˆ [-inf .. inf]
-  fabsl_ld_e âˆˆ [-inf .. inf]
-  fabsl_zero âˆˆ [-inf .. inf]
-  fabsl_minus_zero âˆˆ [-inf .. inf]
-  fabsl_one âˆˆ [-inf .. inf]
-  fabsl_minus_one âˆˆ [-inf .. inf]
-  fabsl_large âˆˆ [-inf .. inf]
-  fabsl_ld_top âˆˆ [-inf .. inf] âˆª {NaN}
-  exponent âˆˆ [--..--]
-  frexp_pi âˆˆ [0.5 .. 1.]
-  frexp_half_pi âˆˆ [0.5 .. 1.]
-  frexp_e âˆˆ [0.5 .. 1.]
-  frexp_zero âˆˆ [-0. .. 0.]
-  frexp_minus_zero âˆˆ [-0. .. 0.]
-  frexp_one âˆˆ [0.5 .. 1.]
-  frexp_minus_one âˆˆ [0.5 .. 1.]
-  frexp_large âˆˆ [0.5 .. 1.]
-  frexp_top âˆˆ [-inf .. inf] âˆª {NaN}
-  frexpf_f_pi âˆˆ [0.5 .. 0.999999940395]
-  frexpf_f_half_pi âˆˆ [0.5 .. 0.999999940395]
-  frexpf_f_e âˆˆ [0.5 .. 0.999999940395]
-  frexpf_zero âˆˆ [-0. .. 0.]
-  frexpf_minus_zero âˆˆ [-0. .. 0.]
-  frexpf_one âˆˆ [0.5 .. 0.999999940395]
-  frexpf_minus_one âˆˆ [0.5 .. 0.999999940395]
-  frexpf_large âˆˆ [0.5 .. 0.999999940395]
-  frexpf_f_top âˆˆ [-inf .. inf] âˆª {NaN}
-  frexpl_ld_pi âˆˆ [-inf .. inf]
-  frexpl_ld_half_pi âˆˆ [-inf .. inf]
-  frexpl_ld_e âˆˆ [-inf .. inf]
-  frexpl_zero âˆˆ [-inf .. inf]
-  frexpl_minus_zero âˆˆ [-inf .. inf]
-  frexpl_one âˆˆ [-inf .. inf]
-  frexpl_minus_one âˆˆ [-inf .. inf]
-  frexpl_large âˆˆ [-inf .. inf]
-  frexpl_ld_top âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexp_pi âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_half_pi âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_e âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_one âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_one âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_large âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_top âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexpf_f_pi âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_half_pi âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_e âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_one âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_one âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_large âˆˆ [-inf .. inf]
-  ldexpf_f_top âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexp_pi_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_half_pi_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_e_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_zero_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_zero_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_one_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_one_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_large_zero âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_top_zero âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexpf_f_pi_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_half_pi_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_e_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_zero_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_zero_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_one_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_one_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_large_zero âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_top_zero âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexp_pi_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_half_pi_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_e_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_zero_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_zero_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_one_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_minus_one_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_large_minus5 âˆˆ [-1.79769313486e+308 .. 1.79769313486e+308]
-  ldexp_top_minus5 âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexpf_f_pi_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_half_pi_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_e_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_zero_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_zero_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_one_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_minus_one_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_large_minus5 âˆˆ [-3.40282346639e+38 .. 3.40282346639e+38]
-  ldexpf_f_top_minus5 âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexp_pi_huge âˆˆ [-inf .. inf]
-  ldexp_half_pi_huge âˆˆ [-inf .. inf]
-  ldexp_e_huge âˆˆ [-inf .. inf]
-  ldexp_zero_huge âˆˆ [-inf .. inf]
-  ldexp_minus_zero_huge âˆˆ [-inf .. inf]
-  ldexp_one_huge âˆˆ [-inf .. inf]
-  ldexp_minus_one_huge âˆˆ [-inf .. inf]
-  ldexp_large_huge âˆˆ [-inf .. inf]
-  ldexp_top_huge âˆˆ [-inf .. inf] âˆª {NaN}
-  ldexpf_f_pi_huge âˆˆ [-inf .. inf]
-  ldexpf_f_half_pi_huge âˆˆ [-inf .. inf]
-  ldexpf_f_e_huge âˆˆ [-inf .. inf]
-  ldexpf_zero_huge âˆˆ [-inf .. inf]
-  ldexpf_minus_zero_huge âˆˆ [-inf .. inf]
-  ldexpf_one_huge âˆˆ [-inf .. inf]
-  ldexpf_minus_one_huge âˆˆ [-inf .. inf]
-  ldexpf_large_huge âˆˆ [-inf .. inf]
-  ldexpf_f_top_huge âˆˆ [-inf .. inf] âˆª {NaN}
-  r âˆˆ {0}
-  __retres âˆˆ {0}