diff --git a/share/libc/math.h b/share/libc/math.h
index ff2ef56a2db3aacb58d304f6e818caae62869885..750ce95085e5b7d9bd78df21e884213802f579eb 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -127,88 +127,41 @@ int __fc_fpclassify(double x);
 #define isnormal(x) \
   (sizeof(x) == sizeof(float) ? __fc_fpclassifyf(x) == FP_NORMAL : __fc_fpclassify(x) == FP_NORMAL)
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures positive_result: \is_finite(\result) && \result >= 0;
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern double acos(double x);
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures positive_result: \is_finite(\result) && \result >= 0;
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern float acosf(float x);
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures positive_result: \is_finite(\result) && \result >= 0;
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern long double acosl(long double x);
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures finite_result: \is_finite(\result);
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern double asin(double x);
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures finite_result: \is_finite(\result);
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern float asinf(float x);
 
-/*@
-  assigns __fc_errno, \result \from x;
-  behavior normal:
-    assumes in_domain: \is_finite(x) && \abs(x) <= 1;
+/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
     assigns \result \from x;
     ensures finite_result: \is_finite(\result);
-  behavior domain_error:
-    assumes out_of_domain: \is_infinite(x) || (\is_finite(x) && \abs(x) > 1);
-    assigns __fc_errno, \result \from x;
-    ensures errno_set: __fc_errno == 1;
-  disjoint behaviors;
- */
+*/
 extern long double asinl(long double x);
 
 /*@ requires finite_arg: \is_finite(x);
diff --git a/src/kernel_services/abstract_interp/fc_float.ml b/src/kernel_services/abstract_interp/fc_float.ml
index 766d977ded6352860c963a75d4cc0abdc7865700..3fd653052056c4e4aede01aaa7a01b37fc20652c 100644
--- a/src/kernel_services/abstract_interp/fc_float.ml
+++ b/src/kernel_services/abstract_interp/fc_float.ml
@@ -222,4 +222,7 @@ let pow round = generate Floating_point.powf ( ** ) round
 
 let cos round = generate Floating_point.cosf cos round
 let sin round = generate Floating_point.sinf sin round
+let acos round = generate Floating_point.acosf acos round
+let asin round = generate Floating_point.asinf asin round
+let atan round = generate Floating_point.atanf atan round
 let atan2 round = generate Floating_point.atan2f atan2 round
diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index c2a3520d261d9a2fa7200273d923fffaa6589bcc..fd063ecc15feda204b32f728b7d5d8c40ce53c11 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -80,6 +80,7 @@ module Make (F: Float_sig.S) = struct
     let pos_zero = Cst.pos_zero Float_sig.Single
     let neg_zero = Cst.neg_zero Float_sig.Single
     let one = F.of_float Near Float_sig.Single 1.
+    let minus_one = F.neg one
     let pos_infinity = Cst.pos_infinity Float_sig.Single
     let neg_infinity = Cst.neg_infinity Float_sig.Single
 
@@ -1005,6 +1006,31 @@ module Make (F: Float_sig.S) = struct
   let cos prec = cos_sin F.cos prec
   let sin prec = cos_sin F.sin prec
 
+  let acos_asin ~acos prec t =
+    t >>: fun ~nan b e ->
+    if Cmp.(lt e minus_one || gt b one)
+    then FRange.nan
+    else
+      let nan, b =
+        if Cmp.(lt b minus_one)
+        then true, F.of_float Near prec (-1.)
+        else nan, b
+      in
+      let nan, e =
+        if Cmp.(gt e one)
+        then true, F.of_float Near prec 1.
+        else nan, e
+      in
+      if acos
+      then approx F.acos prec ~nan e b
+      else approx F.asin prec ~nan b e
+
+  let acos = acos_asin ~acos:true
+  let asin = acos_asin ~acos:false
+
+  let atan prec t =
+    t >>: approx F.atan prec
+
   let atan2 prec x y =
     (x, y) >>% fun ~nan (b1, e1) (b2, e2) ->
     let op = F.atan2 Near prec in
diff --git a/src/kernel_services/abstract_interp/float_interval_sig.mli b/src/kernel_services/abstract_interp/float_interval_sig.mli
index c03606693c1e6518245bce4056ac536cb78b2866..93f2449edb27f4a93b5f5c2bc04628d00f3ef02d 100644
--- a/src/kernel_services/abstract_interp/float_interval_sig.mli
+++ b/src/kernel_services/abstract_interp/float_interval_sig.mli
@@ -140,6 +140,9 @@ module type S = sig
 
   val cos: prec -> t -> t
   val sin: prec -> t -> t
+  val acos: prec -> t -> t
+  val asin: prec -> t -> t
+  val atan: prec -> t -> t
   val atan2: prec -> t -> t -> t
 
   val backward_add:
diff --git a/src/kernel_services/abstract_interp/float_sig.mli b/src/kernel_services/abstract_interp/float_sig.mli
index b58635ea623351593b98b1309066a0635e02a658..b897cd89d1b64c80404513022e33f012ae39b31e 100644
--- a/src/kernel_services/abstract_interp/float_sig.mli
+++ b/src/kernel_services/abstract_interp/float_sig.mli
@@ -119,5 +119,8 @@ module type S = sig
 
   val cos: round -> prec -> t -> t
   val sin: round -> prec -> t -> t
+  val acos: round -> prec -> t -> t
+  val asin: round -> prec -> t -> t
+  val atan: round -> prec -> t -> t
   val atan2: round -> prec -> t -> t -> t
 end
diff --git a/src/libraries/utils/c_bindings.c b/src/libraries/utils/c_bindings.c
index 8ca903af5beb0a600e55d2ce00b285e561154172..8ddedd9fc6adc6aab20499944334f2606b3ec914 100644
--- a/src/libraries/utils/c_bindings.c
+++ b/src/libraries/utils/c_bindings.c
@@ -65,35 +65,24 @@ value c_trunc(value d)
   return caml_copy_double(trunc(Double_val(d)));
 }
 
-/* NOTE: The single-precision functions below (expf, logf, etc.) need the
-   'volatile' modifier due to odd behaviors detected in Ubuntu 12.04
-   (precise32), with gcc 4.6.3 and glibc 2.15.
-   In those machines, the absence of volatile leads gcc to optimize the
-   call to a double-precision result and, despite the use of 'float' and
-   casts (which should force the result to be truncated to 32 bits),
-   the 64-bit result is propagated back to OCaml, leading to non-zero bits
-   beyond the 32-bit range, which cause FRange.check_representability to fail,
-   leading to errors in tests/float/math_builtins.c.
-   This behavior has not been observed in more recent distributions. */
-
 value c_expf(value d)
 {
   float f = Double_val(d);
-  volatile float res = expf(f); // see remarks above
+  float res = expf(f);
   return caml_copy_double(res);
 }
 
 value c_logf(value d)
 {
   float f = Double_val(d);
-  volatile float res = logf(f); // see remarks above
+  float res = logf(f);
   return caml_copy_double(res);
 }
 
 value c_log10f(value d)
 {
   float f = Double_val(d);
-  volatile float res = log10f(f); // see remarks above
+  float res = log10f(f);
   return caml_copy_double(res);
 }
 
@@ -101,14 +90,14 @@ value c_powf(value x, value y)
 {
   float fx = Double_val(x);
   float fy = Double_val(y);
-  volatile float res = powf(fx, fy); // see remarks above
+  float res = powf(fx, fy);
   return caml_copy_double(res);
 }
 
 value c_sqrtf(value d)
 {
   float f = Double_val(d);
-  volatile float res = sqrtf(f); // see remarks above
+  float res = sqrtf(f);
   return caml_copy_double(res);
 }
 
@@ -116,21 +105,42 @@ value c_fmodf(value x, value y)
 {
   float fx = Double_val(x);
   float fy = Double_val(y);
-  volatile float res = fmodf(fx, fy); // see remarks above
+  float res = fmodf(fx, fy);
   return caml_copy_double(res);
 }
 
 value c_cosf(value x)
 {
   float f = Double_val(x);
-  volatile float res = cosf(f); // see remarks above
+  float res = cosf(f);
   return caml_copy_double(res);
 }
 
 value c_sinf(value x)
 {
   float f = Double_val(x);
-  volatile float res = sinf(f); // see remarks above
+  float res = sinf(f);
+  return caml_copy_double(res);
+}
+
+value c_acosf(value x)
+{
+  float f = Double_val(x);
+  float res = acosf(f);
+  return caml_copy_double(res);
+}
+
+value c_asinf(value x)
+{
+  float f = Double_val(x);
+  float res = asinf(f);
+  return caml_copy_double(res);
+}
+
+value c_atanf(value x)
+{
+  float f = Double_val(x);
+  float res = atanf(f);
   return caml_copy_double(res);
 }
 
@@ -138,7 +148,7 @@ value c_atan2f(value x, value y)
 {
   float fx = Double_val(x);
   float fy = Double_val(y);
-  volatile float res = atan2f(fx, fy); // see remarks above
+  float res = atan2f(fx, fy);
   return caml_copy_double(res);
 }
 
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 13227afdd5da5ff1abadabed250a4c13aff26dd2..63c67cd7a57612bf07140f07269a0442f07bf13f 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -426,6 +426,9 @@ external sqrtf: float -> float = "c_sqrtf"
 external fmodf: float -> float -> float = "c_fmodf"
 external cosf: float -> float = "c_cosf"
 external sinf: float -> float = "c_sinf"
+external acosf: float -> float = "c_acosf"
+external asinf: float -> float = "c_asinf"
+external atanf: float -> float = "c_atanf"
 external atan2f: float -> float -> float = "c_atan2f"
 
 
diff --git a/src/libraries/utils/floating_point.mli b/src/libraries/utils/floating_point.mli
index 11190c51425225feeae0faece5c12928f0090c90..10c0f35d64c858568cc718b469bdca9c647fc544 100644
--- a/src/libraries/utils/floating_point.mli
+++ b/src/libraries/utils/floating_point.mli
@@ -110,6 +110,9 @@ external sqrtf: float -> float = "c_sqrtf"
 external fmodf: float -> float -> float = "c_fmodf"
 external cosf: float -> float = "c_cosf"
 external sinf: float -> float = "c_sinf"
+external acosf: float -> float = "c_acosf"
+external asinf: float -> float = "c_asinf"
+external atanf: float -> float = "c_atanf"
 external atan2f: float -> float -> float = "c_atan2f"
 
 
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 4a8fc2e347b0524ed2dd3a46002026834a250e5d..445f2843ae3c712b2b47065c1d72f36a0c2d9ec8 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	525	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc	math.h	478	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/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index 7600ec19a6c18e34e703d9e9d0a08f72ae9bc3b9..3981a1f063c0076ad8cb69fa80ea45d0473fb675 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -121,6 +121,9 @@ let () =
   let open Fval in
   register_arity1 "cos" Cil_types.FDouble cos;
   register_arity1 "sin" Cil_types.FDouble sin;
+  register_arity1 "acos" Cil_types.FDouble acos;
+  register_arity1 "asin" Cil_types.FDouble asin;
+  register_arity1 "atan" Cil_types.FDouble atan;
   register_arity1 "log" Cil_types.FDouble log;
   register_arity1 "log10" Cil_types.FDouble log10;
   register_arity1 "exp" Cil_types.FDouble exp;
@@ -132,6 +135,9 @@ let () =
 
   register_arity1 "cosf" Cil_types.FFloat cos;
   register_arity1 "sinf" Cil_types.FFloat sin;
+  register_arity1 "acosf" Cil_types.FFloat acos;
+  register_arity1 "asinf" Cil_types.FFloat asin;
+  register_arity1 "atanf" Cil_types.FFloat atan;
   register_arity1 "logf" Cil_types.FFloat log;
   register_arity1 "log10f" Cil_types.FFloat log10;
   register_arity1 "expf" Cil_types.FFloat exp;
diff --git a/tests/float/math_builtins.c b/tests/float/math_builtins.c
index db8f6293442022436d2382973a30e836316f93dd..3ed738df40506625f643fc4684e02907b13ab368 100644
--- a/tests/float/math_builtins.c
+++ b/tests/float/math_builtins.c
@@ -6,6 +6,8 @@
 #include <math.h>
 
 static volatile int nondet;
+static volatile double any_double;
+static volatile float any_float;
 #define assert_bottom(exp) if (nondet) { exp; Frama_C_show_each_unreachable(); }
 
 double double_interval(double min, double max) {
@@ -25,6 +27,74 @@ void test_sin_det() {
   double z = sin(-1.);
 }
 
+void test_acos () {
+  double half_pi = acos(0.);
+  double pi = acos(-1.);
+  double zero = acos(1.);
+  double acos_image = acos(any_double);
+  if (nondet) {
+    double bottom = acos(-1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom = acos(1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  double x = acos(0.5);
+  double y = acos(-0.5);
+  double xy = double_interval(-0.5, 0.5);
+  xy = acos(xy);
+  /* Test acosf. */
+  float f32_half_pi = acosf(0.f);
+  float f32_pi = acosf(-1.f);
+  float f32_zero = acosf(1.f);
+  float f32_acosf_image = acosf(any_float);
+  if (nondet) {
+    float bottom = acosf(2.f);
+    Frama_C_show_each_bottom(bottom);
+  }
+}
+
+void test_asin () {
+  double zero = asin(0.);
+  double minus_half_pi = asin(-1.);
+  double half_pi = asin(1.);
+  double asin_image = asin(any_double);
+  if (nondet) {
+    double bottom = asin(-1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom = asin(1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  double x = asin(-0.5);
+  double y = asin(0.5);
+  double xy = double_interval(-0.5, 0.5);
+  xy = asin(xy);
+  /* Test asinf. */
+  float f32_zero = asinf(0.f);
+  float f32_minus_half_pi = asinf(-1.f);
+  float f32_half_pi = asinf(1.f);
+  float f32_asinf_image = asinf(any_float);
+  if (nondet) {
+    float bottom = asinf(2.f);
+    Frama_C_show_each_bottom(bottom);
+  }
+}
+
+void test_atan () {
+  double zero = atan(0.);
+  double atan_image = atan(any_double);
+  double x = atan(-2.);
+  double y = atan(2.);
+  double xy = double_interval(-2., 2.);
+  xy = atan(xy);
+  /* Test atanf. */
+  float f32_zero = atanf(0.f);
+  float f32_atanf_image = atanf(any_float);
+}
+
 void test_atan2_det() {
   double a = atan2(1.,0.);
   double b = atan2(0.,1.);
@@ -655,6 +725,9 @@ void test_roundf() {
 int main() {
   test_cos_det();
   test_sin_det();
+  test_acos();
+  test_asin();
+  test_atan();
   test_atan2_det();
   test_atan2();
   test_pow_det();
diff --git a/tests/float/oracle/math_builtins.res.oracle b/tests/float/oracle/math_builtins.res.oracle
index a53099f800a4a3158bb767fb8a687b479f2a8d15..c1889dd4b24485b7e7df34fc9a077f6ff1eeaddc 100644
--- a/tests/float/oracle/math_builtins.res.oracle
+++ b/tests/float/oracle/math_builtins.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/math_builtins.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/math_builtins.c:248: Warning: 
+[kernel:parser:decimal-float] tests/float/math_builtins.c:318: Warning: 
   Floating-point constant 5.8 is not represented exactly. Will use 0x1.7333333333333p2.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -7,2292 +7,2423 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
+  any_double ∈ [--..--]
+  any_float ∈ [--..--]
 [eva] computing for function test_cos_det <- main.
-  Called from tests/float/math_builtins.c:656.
-[eva] tests/float/math_builtins.c:17: 
+  Called from tests/float/math_builtins.c:726.
+[eva] tests/float/math_builtins.c:19: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:17: 
+[eva] tests/float/math_builtins.c:19: 
   function cos: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:18: 
+[eva] tests/float/math_builtins.c:20: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:18: 
+[eva] tests/float/math_builtins.c:20: 
   function cos: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:19: 
+[eva] tests/float/math_builtins.c:21: 
   Call to builtin Frama_C_cos for function cos
-[eva] tests/float/math_builtins.c:19: 
+[eva] tests/float/math_builtins.c:21: 
   function cos: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_cos_det
 [eva] Done for function test_cos_det
 [eva] computing for function test_sin_det <- main.
-  Called from tests/float/math_builtins.c:657.
-[eva] tests/float/math_builtins.c:23: 
+  Called from tests/float/math_builtins.c:727.
+[eva] tests/float/math_builtins.c:25: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:23: 
+[eva] tests/float/math_builtins.c:25: 
   function sin: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:24: 
+[eva] tests/float/math_builtins.c:26: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:24: 
+[eva] tests/float/math_builtins.c:26: 
   function sin: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:25: 
+[eva] tests/float/math_builtins.c:27: 
   Call to builtin Frama_C_sin for function sin
-[eva] tests/float/math_builtins.c:25: 
+[eva] tests/float/math_builtins.c:27: 
   function sin: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_sin_det
 [eva] Done for function test_sin_det
+[eva] computing for function test_acos <- main.
+  Called from tests/float/math_builtins.c:728.
+[eva] tests/float/math_builtins.c:31: Call to builtin acos
+[eva] tests/float/math_builtins.c:31: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:32: Call to builtin acos
+[eva] tests/float/math_builtins.c:32: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:33: Call to builtin acos
+[eva] tests/float/math_builtins.c:33: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:34: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:34: Warning: 
+  function acos: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:36: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:36: Warning: 
+  function acos: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:40: Call to builtin acos
+[eva:alarm] tests/float/math_builtins.c:40: Warning: 
+  function acos: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:43: Call to builtin acos
+[eva] tests/float/math_builtins.c:43: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:44: Call to builtin acos
+[eva] tests/float/math_builtins.c:44: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] computing for function double_interval <- test_acos <- main.
+  Called from tests/float/math_builtins.c:45.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:46: Call to builtin acos
+[eva] tests/float/math_builtins.c:46: 
+  function acos: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:48: Call to builtin acosf
+[eva] tests/float/math_builtins.c:48: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:49: Call to builtin acosf
+[eva] tests/float/math_builtins.c:49: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:50: Call to builtin acosf
+[eva] tests/float/math_builtins.c:50: 
+  function acosf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:51: Call to builtin acosf
+[eva:alarm] tests/float/math_builtins.c:51: Warning: 
+  function acosf: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:53: Call to builtin acosf
+[eva:alarm] tests/float/math_builtins.c:53: Warning: 
+  function acosf: precondition 'in_domain' got status invalid.
+[eva] Recording results for test_acos
+[eva] Done for function test_acos
+[eva] computing for function test_asin <- main.
+  Called from tests/float/math_builtins.c:729.
+[eva] tests/float/math_builtins.c:59: Call to builtin asin
+[eva] tests/float/math_builtins.c:59: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:60: Call to builtin asin
+[eva] tests/float/math_builtins.c:60: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:61: Call to builtin asin
+[eva] tests/float/math_builtins.c:61: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:62: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:62: Warning: 
+  function asin: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:64: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:64: Warning: 
+  function asin: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:68: Call to builtin asin
+[eva:alarm] tests/float/math_builtins.c:68: Warning: 
+  function asin: precondition 'in_domain' got status invalid.
+[eva] tests/float/math_builtins.c:71: Call to builtin asin
+[eva] tests/float/math_builtins.c:71: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:72: Call to builtin asin
+[eva] tests/float/math_builtins.c:72: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] computing for function double_interval <- test_asin <- main.
+  Called from tests/float/math_builtins.c:73.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:74: Call to builtin asin
+[eva] tests/float/math_builtins.c:74: 
+  function asin: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:76: Call to builtin asinf
+[eva] tests/float/math_builtins.c:76: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:77: Call to builtin asinf
+[eva] tests/float/math_builtins.c:77: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:78: Call to builtin asinf
+[eva] tests/float/math_builtins.c:78: 
+  function asinf: precondition 'in_domain' got status valid.
+[eva] tests/float/math_builtins.c:79: Call to builtin asinf
+[eva:alarm] tests/float/math_builtins.c:79: Warning: 
+  function asinf: precondition 'in_domain' got status unknown.
+[eva] tests/float/math_builtins.c:81: Call to builtin asinf
+[eva:alarm] tests/float/math_builtins.c:81: Warning: 
+  function asinf: precondition 'in_domain' got status invalid.
+[eva] Recording results for test_asin
+[eva] Done for function test_asin
+[eva] computing for function test_atan <- main.
+  Called from tests/float/math_builtins.c:730.
+[eva] tests/float/math_builtins.c:87: Call to builtin atan
+[eva] tests/float/math_builtins.c:87: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:88: Call to builtin atan
+[eva:alarm] tests/float/math_builtins.c:88: Warning: 
+  function atan: precondition 'finite_arg' got status unknown.
+[eva] tests/float/math_builtins.c:89: Call to builtin atan
+[eva] tests/float/math_builtins.c:89: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:90: Call to builtin atan
+[eva] tests/float/math_builtins.c:90: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] computing for function double_interval <- test_atan <- main.
+  Called from tests/float/math_builtins.c:91.
+[eva] Recording results for double_interval
+[eva] Done for function double_interval
+[eva] tests/float/math_builtins.c:92: Call to builtin atan
+[eva] tests/float/math_builtins.c:92: 
+  function atan: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:94: Call to builtin atanf
+[eva] tests/float/math_builtins.c:94: 
+  function atanf: precondition 'finite_arg' got status valid.
+[eva] tests/float/math_builtins.c:95: Call to builtin atanf
+[eva:alarm] tests/float/math_builtins.c:95: Warning: 
+  function atanf: precondition 'finite_arg' got status unknown.
+[eva] Recording results for test_atan
+[eva] Done for function test_atan
 [eva] computing for function test_atan2_det <- main.
-  Called from tests/float/math_builtins.c:658.
-[eva] tests/float/math_builtins.c:29: 
+  Called from tests/float/math_builtins.c:731.
+[eva] tests/float/math_builtins.c:99: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:29: 
+[eva] tests/float/math_builtins.c:99: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:29: 
+[eva] tests/float/math_builtins.c:99: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:30: 
+[eva] tests/float/math_builtins.c:100: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:31: 
+[eva] tests/float/math_builtins.c:101: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:32: 
+[eva] tests/float/math_builtins.c:102: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:33: 
+[eva] tests/float/math_builtins.c:103: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:34: 
+[eva] tests/float/math_builtins.c:104: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:35: 
+[eva] tests/float/math_builtins.c:105: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:36: 
+[eva] tests/float/math_builtins.c:106: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:37: 
+[eva] tests/float/math_builtins.c:107: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:38: 
+[eva] tests/float/math_builtins.c:108: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:39: 
+[eva] tests/float/math_builtins.c:109: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:40: 
+[eva] tests/float/math_builtins.c:110: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:41: 
+[eva] tests/float/math_builtins.c:111: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] Recording results for test_atan2_det
 [eva] Done for function test_atan2_det
 [eva] computing for function test_atan2 <- main.
-  Called from tests/float/math_builtins.c:659.
+  Called from tests/float/math_builtins.c:732.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:46.
+  Called from tests/float/math_builtins.c:116.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:47.
+  Called from tests/float/math_builtins.c:117.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:48: 
+[eva] tests/float/math_builtins.c:118: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:49.
+  Called from tests/float/math_builtins.c:119.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:50: 
+[eva] tests/float/math_builtins.c:120: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:51.
+  Called from tests/float/math_builtins.c:121.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:52: 
+[eva] tests/float/math_builtins.c:122: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:53.
+  Called from tests/float/math_builtins.c:123.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:54: 
+[eva] tests/float/math_builtins.c:124: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:55.
+  Called from tests/float/math_builtins.c:125.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:56: 
+[eva] tests/float/math_builtins.c:126: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:57.
+  Called from tests/float/math_builtins.c:127.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:58.
+  Called from tests/float/math_builtins.c:128.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:59: 
+[eva] tests/float/math_builtins.c:129: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:60.
+  Called from tests/float/math_builtins.c:130.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:61: 
+[eva] tests/float/math_builtins.c:131: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:62.
+  Called from tests/float/math_builtins.c:132.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:63: 
+[eva] tests/float/math_builtins.c:133: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:64.
+  Called from tests/float/math_builtins.c:134.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:65: 
+[eva] tests/float/math_builtins.c:135: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] computing for function double_interval <- test_atan2 <- main.
-  Called from tests/float/math_builtins.c:66.
+  Called from tests/float/math_builtins.c:136.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:67: 
+[eva] tests/float/math_builtins.c:137: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:68: 
+[eva] tests/float/math_builtins.c:138: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:69: 
+[eva] tests/float/math_builtins.c:139: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:70: 
+[eva] tests/float/math_builtins.c:140: 
   function atan2: precondition 'finite_result' got status valid.
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   Call to builtin Frama_C_atan2 for function atan2
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   function atan2: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:71: 
+[eva] tests/float/math_builtins.c:141: 
   function atan2: precondition 'finite_result' got status valid.
 [eva] Recording results for test_atan2
 [eva] Done for function test_atan2
 [eva] computing for function test_pow_det <- main.
-  Called from tests/float/math_builtins.c:660.
-[eva] tests/float/math_builtins.c:75: 
+  Called from tests/float/math_builtins.c:733.
+[eva] tests/float/math_builtins.c:145: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:75: 
+[eva] tests/float/math_builtins.c:145: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:75: 
+[eva] tests/float/math_builtins.c:145: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:76: 
+[eva] tests/float/math_builtins.c:146: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:77: 
+[eva] tests/float/math_builtins.c:147: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:78: 
+[eva] tests/float/math_builtins.c:148: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:79: 
+[eva] tests/float/math_builtins.c:149: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:80: 
+[eva] tests/float/math_builtins.c:150: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:81: 
+[eva] tests/float/math_builtins.c:151: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:82: 
+[eva] tests/float/math_builtins.c:152: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow_det
 [eva] Done for function test_pow_det
 [eva] computing for function test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:661.
+  Called from tests/float/math_builtins.c:734.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:98.
+  Called from tests/float/math_builtins.c:168.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:100: 
+[eva] tests/float/math_builtins.c:170: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:100: 
+[eva] tests/float/math_builtins.c:170: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:100: Warning: 
+[eva:alarm] tests/float/math_builtins.c:170: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
-[eva] tests/float/math_builtins.c:102: 
+[eva] tests/float/math_builtins.c:172: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:102: 
+[eva] tests/float/math_builtins.c:172: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:102: Warning: 
+[eva:alarm] tests/float/math_builtins.c:172: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:105.
+  Called from tests/float/math_builtins.c:175.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:106: 
+[eva] tests/float/math_builtins.c:176: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:106: 
+[eva] tests/float/math_builtins.c:176: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:106: Warning: 
+[eva:alarm] tests/float/math_builtins.c:176: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:107: 
+[eva] tests/float/math_builtins.c:177: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:107: 
+[eva] tests/float/math_builtins.c:177: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:107: Warning: 
+[eva:alarm] tests/float/math_builtins.c:177: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:110: 
+[eva] tests/float/math_builtins.c:180: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:110: 
+[eva] tests/float/math_builtins.c:180: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:110: Warning: 
+[eva:alarm] tests/float/math_builtins.c:180: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:111: 
+[eva] tests/float/math_builtins.c:181: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:111: 
+[eva] tests/float/math_builtins.c:181: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:111: Warning: 
+[eva:alarm] tests/float/math_builtins.c:181: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:114.
+  Called from tests/float/math_builtins.c:184.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:115: 
+[eva] tests/float/math_builtins.c:185: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:115: 
+[eva] tests/float/math_builtins.c:185: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:115: Warning: 
+[eva:alarm] tests/float/math_builtins.c:185: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:116.
+  Called from tests/float/math_builtins.c:186.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:117: 
+[eva] tests/float/math_builtins.c:187: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:117: 
+[eva] tests/float/math_builtins.c:187: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:117: Warning: 
+[eva:alarm] tests/float/math_builtins.c:187: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:120.
+  Called from tests/float/math_builtins.c:190.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:121: 
+[eva] tests/float/math_builtins.c:191: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:122: 
+[eva] tests/float/math_builtins.c:192: 
   Frama_C_show_each_i: [0.0000000000000000 .. 1.0000000000000000*2^-1000]
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:123.
+  Called from tests/float/math_builtins.c:193.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:124: 
+[eva] tests/float/math_builtins.c:194: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:125: 
+[eva] tests/float/math_builtins.c:195: 
   Frama_C_show_each_j:
   [0.2500000000000000*2^-1022 .. 1.2707064924076672*2^-330]
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:129: 
+[eva] tests/float/math_builtins.c:199: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:130: 
+[eva] tests/float/math_builtins.c:200: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:132.
+  Called from tests/float/math_builtins.c:202.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:133: 
+[eva] tests/float/math_builtins.c:203: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:134: 
+[eva] tests/float/math_builtins.c:204: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:135: 
+[eva] tests/float/math_builtins.c:205: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:136: 
+[eva] tests/float/math_builtins.c:206: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:137: 
+[eva] tests/float/math_builtins.c:207: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:139.
+  Called from tests/float/math_builtins.c:209.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:140: 
+[eva] tests/float/math_builtins.c:210: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:141: 
+[eva] tests/float/math_builtins.c:211: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow_singleton_exp
 [eva] Done for function test_pow_singleton_exp
 [eva] computing for function test_pow <- main.
-  Called from tests/float/math_builtins.c:662.
+  Called from tests/float/math_builtins.c:735.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:147.
+  Called from tests/float/math_builtins.c:217.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:148: 
+[eva] tests/float/math_builtins.c:218: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:149.
+  Called from tests/float/math_builtins.c:219.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:150: 
+[eva] tests/float/math_builtins.c:220: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:151.
+  Called from tests/float/math_builtins.c:221.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:152: 
+[eva] tests/float/math_builtins.c:222: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:158.
+  Called from tests/float/math_builtins.c:228.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:159.
+  Called from tests/float/math_builtins.c:229.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:160: 
+[eva] tests/float/math_builtins.c:230: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:160: 
+[eva] tests/float/math_builtins.c:230: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:160: Warning: 
+[eva:alarm] tests/float/math_builtins.c:230: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:161.
+  Called from tests/float/math_builtins.c:231.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:162: 
+[eva] tests/float/math_builtins.c:232: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:162: 
+[eva] tests/float/math_builtins.c:232: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:162: Warning: 
+[eva:alarm] tests/float/math_builtins.c:232: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:163.
+  Called from tests/float/math_builtins.c:233.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:164: 
+[eva] tests/float/math_builtins.c:234: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:164: 
+[eva] tests/float/math_builtins.c:234: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:164: Warning: 
+[eva:alarm] tests/float/math_builtins.c:234: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:165.
+  Called from tests/float/math_builtins.c:235.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:166.
+  Called from tests/float/math_builtins.c:236.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:167: 
+[eva] tests/float/math_builtins.c:237: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:170.
+  Called from tests/float/math_builtins.c:240.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:171.
+  Called from tests/float/math_builtins.c:241.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:172: 
+[eva] tests/float/math_builtins.c:242: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:175.
+  Called from tests/float/math_builtins.c:245.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:176.
+  Called from tests/float/math_builtins.c:246.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:177: 
+[eva] tests/float/math_builtins.c:247: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:177: 
+[eva] tests/float/math_builtins.c:247: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:177: Warning: 
+[eva:alarm] tests/float/math_builtins.c:247: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:178.
+  Called from tests/float/math_builtins.c:248.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:179.
+  Called from tests/float/math_builtins.c:249.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:180: 
+[eva] tests/float/math_builtins.c:250: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:180: 
+[eva] tests/float/math_builtins.c:250: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:180: Warning: 
+[eva:alarm] tests/float/math_builtins.c:250: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:184.
+  Called from tests/float/math_builtins.c:254.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:185.
+  Called from tests/float/math_builtins.c:255.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:186: 
+[eva] tests/float/math_builtins.c:256: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:186: 
+[eva] tests/float/math_builtins.c:256: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:186: Warning: 
+[eva:alarm] tests/float/math_builtins.c:256: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:189.
+  Called from tests/float/math_builtins.c:259.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:190.
+  Called from tests/float/math_builtins.c:260.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:191: 
+[eva] tests/float/math_builtins.c:261: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:191: 
+[eva] tests/float/math_builtins.c:261: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:191: Warning: 
+[eva:alarm] tests/float/math_builtins.c:261: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:194.
+  Called from tests/float/math_builtins.c:264.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:195.
+  Called from tests/float/math_builtins.c:265.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:196: 
+[eva] tests/float/math_builtins.c:266: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:199.
+  Called from tests/float/math_builtins.c:269.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:200.
+  Called from tests/float/math_builtins.c:270.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:201: 
+[eva] tests/float/math_builtins.c:271: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:201: 
+[eva] tests/float/math_builtins.c:271: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:201: Warning: 
+[eva:alarm] tests/float/math_builtins.c:271: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:204.
+  Called from tests/float/math_builtins.c:274.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:205.
+  Called from tests/float/math_builtins.c:275.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:206: 
+[eva] tests/float/math_builtins.c:276: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:206: 
+[eva] tests/float/math_builtins.c:276: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:206: Warning: 
+[eva:alarm] tests/float/math_builtins.c:276: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:207.
+  Called from tests/float/math_builtins.c:277.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:208: 
+[eva] tests/float/math_builtins.c:278: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:208: 
+[eva] tests/float/math_builtins.c:278: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:208: Warning: 
+[eva:alarm] tests/float/math_builtins.c:278: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:209.
+  Called from tests/float/math_builtins.c:279.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:210: 
+[eva] tests/float/math_builtins.c:280: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:210: 
+[eva] tests/float/math_builtins.c:280: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:210: Warning: 
+[eva:alarm] tests/float/math_builtins.c:280: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:211.
+  Called from tests/float/math_builtins.c:281.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:212: 
+[eva] tests/float/math_builtins.c:282: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:212: 
+[eva] tests/float/math_builtins.c:282: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:212: Warning: 
+[eva:alarm] tests/float/math_builtins.c:282: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:215.
+  Called from tests/float/math_builtins.c:285.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:216.
+  Called from tests/float/math_builtins.c:286.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:217: 
+[eva] tests/float/math_builtins.c:287: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:217: 
+[eva] tests/float/math_builtins.c:287: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:217: Warning: 
+[eva:alarm] tests/float/math_builtins.c:287: Warning: 
   function pow: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:220.
+  Called from tests/float/math_builtins.c:290.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:221.
+  Called from tests/float/math_builtins.c:291.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:222: 
+[eva] tests/float/math_builtins.c:292: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:222: 
+[eva] tests/float/math_builtins.c:292: 
   function pow: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:222: Warning: 
+[eva:alarm] tests/float/math_builtins.c:292: Warning: 
   function pow: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:222: Frama_C_show_each_unreachable:
+[eva] tests/float/math_builtins.c:292: Frama_C_show_each_unreachable:
 [eva] computing for function double_interval <- test_pow <- main.
-  Called from tests/float/math_builtins.c:224.
+  Called from tests/float/math_builtins.c:294.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:225: 
+[eva] tests/float/math_builtins.c:295: 
   function pow: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_pow
 [eva] Done for function test_pow
 [eva] computing for function test_fmod_det <- main.
-  Called from tests/float/math_builtins.c:663.
-[eva] tests/float/math_builtins.c:335: 
+  Called from tests/float/math_builtins.c:736.
+[eva] tests/float/math_builtins.c:405: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:335: 
+[eva] tests/float/math_builtins.c:405: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:335: 
+[eva] tests/float/math_builtins.c:405: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:336: 
+[eva] tests/float/math_builtins.c:406: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:337: 
+[eva] tests/float/math_builtins.c:407: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:338: 
+[eva] tests/float/math_builtins.c:408: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:339: 
+[eva] tests/float/math_builtins.c:409: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:340: 
+[eva] tests/float/math_builtins.c:410: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:341: 
+[eva] tests/float/math_builtins.c:411: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:341: 
+[eva] tests/float/math_builtins.c:411: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:341: Warning: 
+[eva:alarm] tests/float/math_builtins.c:411: Warning: 
   function fmod: precondition 'finite_logic_result' got status invalid.
 [eva] Recording results for test_fmod_det
 [eva] Done for function test_fmod_det
 [eva] computing for function test_fmod <- main.
-  Called from tests/float/math_builtins.c:664.
+  Called from tests/float/math_builtins.c:737.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:346.
+  Called from tests/float/math_builtins.c:416.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:347: 
+[eva] tests/float/math_builtins.c:417: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:348: 
+[eva] tests/float/math_builtins.c:418: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:349: 
+[eva] tests/float/math_builtins.c:419: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:350: 
+[eva] tests/float/math_builtins.c:420: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:350: 
+[eva] tests/float/math_builtins.c:420: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:350: 
+[eva] tests/float/math_builtins.c:420: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:351.
+  Called from tests/float/math_builtins.c:421.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:352: 
+[eva] tests/float/math_builtins.c:422: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:353: 
+[eva] tests/float/math_builtins.c:423: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:353: 
+[eva] tests/float/math_builtins.c:423: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:353: 
+[eva] tests/float/math_builtins.c:423: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:354.
+  Called from tests/float/math_builtins.c:424.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:355.
+  Called from tests/float/math_builtins.c:425.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:356: 
+[eva] tests/float/math_builtins.c:426: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:356: 
+[eva] tests/float/math_builtins.c:426: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:356: 
+[eva] tests/float/math_builtins.c:426: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:357.
+  Called from tests/float/math_builtins.c:427.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:358.
+  Called from tests/float/math_builtins.c:428.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:359: 
+[eva] tests/float/math_builtins.c:429: 
   function fmod: precondition 'finite_logic_result' got status valid.
-[eva] tests/float/math_builtins.c:360: 
+[eva] tests/float/math_builtins.c:430: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:360: 
+[eva] tests/float/math_builtins.c:430: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:360: 
+[eva] tests/float/math_builtins.c:430: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:361.
+  Called from tests/float/math_builtins.c:431.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:362.
+  Called from tests/float/math_builtins.c:432.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:363: 
+[eva] tests/float/math_builtins.c:433: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:363: 
+[eva] tests/float/math_builtins.c:433: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:363: Warning: 
+[eva:alarm] tests/float/math_builtins.c:433: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:364.
+  Called from tests/float/math_builtins.c:434.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:365.
+  Called from tests/float/math_builtins.c:435.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:366: 
+[eva] tests/float/math_builtins.c:436: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:366: 
+[eva] tests/float/math_builtins.c:436: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:366: Warning: 
+[eva:alarm] tests/float/math_builtins.c:436: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:367.
+  Called from tests/float/math_builtins.c:437.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:368: 
+[eva] tests/float/math_builtins.c:438: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:368: 
+[eva] tests/float/math_builtins.c:438: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:368: Warning: 
+[eva:alarm] tests/float/math_builtins.c:438: Warning: 
   function fmod: precondition 'finite_logic_result' got status invalid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:369.
+  Called from tests/float/math_builtins.c:439.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:370: 
+[eva] tests/float/math_builtins.c:440: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:370: 
+[eva] tests/float/math_builtins.c:440: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:370: Warning: 
+[eva:alarm] tests/float/math_builtins.c:440: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:371.
+  Called from tests/float/math_builtins.c:441.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:372: 
+[eva] tests/float/math_builtins.c:442: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:372: 
+[eva] tests/float/math_builtins.c:442: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:372: Warning: 
+[eva:alarm] tests/float/math_builtins.c:442: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:373.
+  Called from tests/float/math_builtins.c:443.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:374: 
+[eva] tests/float/math_builtins.c:444: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:374: 
+[eva] tests/float/math_builtins.c:444: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:374: 
+[eva] tests/float/math_builtins.c:444: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:375.
+  Called from tests/float/math_builtins.c:445.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:376: 
+[eva] tests/float/math_builtins.c:446: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:376: 
+[eva] tests/float/math_builtins.c:446: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:376: 
+[eva] tests/float/math_builtins.c:446: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:377.
+  Called from tests/float/math_builtins.c:447.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:378: 
+[eva] tests/float/math_builtins.c:448: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:378: 
+[eva] tests/float/math_builtins.c:448: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:378: 
+[eva] tests/float/math_builtins.c:448: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:379.
+  Called from tests/float/math_builtins.c:449.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:380: 
+[eva] tests/float/math_builtins.c:450: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:380: 
+[eva] tests/float/math_builtins.c:450: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:380: 
+[eva] tests/float/math_builtins.c:450: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:381.
+  Called from tests/float/math_builtins.c:451.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:382: 
+[eva] tests/float/math_builtins.c:452: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:382: 
+[eva] tests/float/math_builtins.c:452: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:382: 
+[eva] tests/float/math_builtins.c:452: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:383.
+  Called from tests/float/math_builtins.c:453.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:384: 
+[eva] tests/float/math_builtins.c:454: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:384: 
+[eva] tests/float/math_builtins.c:454: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:384: 
+[eva] tests/float/math_builtins.c:454: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:385.
+  Called from tests/float/math_builtins.c:455.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:386: 
+[eva] tests/float/math_builtins.c:456: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:386: 
+[eva] tests/float/math_builtins.c:456: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:386: 
+[eva] tests/float/math_builtins.c:456: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:387.
+  Called from tests/float/math_builtins.c:457.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:388: 
+[eva] tests/float/math_builtins.c:458: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:388: 
+[eva] tests/float/math_builtins.c:458: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:388: 
+[eva] tests/float/math_builtins.c:458: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:389.
+  Called from tests/float/math_builtins.c:459.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:390.
+  Called from tests/float/math_builtins.c:460.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:391: 
+[eva] tests/float/math_builtins.c:461: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:391: 
+[eva] tests/float/math_builtins.c:461: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:391: 
+[eva] tests/float/math_builtins.c:461: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:392.
+  Called from tests/float/math_builtins.c:462.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:393: 
+[eva] tests/float/math_builtins.c:463: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:393: 
+[eva] tests/float/math_builtins.c:463: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:393: 
+[eva] tests/float/math_builtins.c:463: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:394.
+  Called from tests/float/math_builtins.c:464.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:395: 
+[eva] tests/float/math_builtins.c:465: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:395: 
+[eva] tests/float/math_builtins.c:465: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:395: 
+[eva] tests/float/math_builtins.c:465: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:396.
+  Called from tests/float/math_builtins.c:466.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:397: 
+[eva] tests/float/math_builtins.c:467: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:397: 
+[eva] tests/float/math_builtins.c:467: 
   function fmod: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:397: 
+[eva] tests/float/math_builtins.c:467: 
   function fmod: precondition 'finite_logic_result' got status valid.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:398.
+  Called from tests/float/math_builtins.c:468.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:399.
+  Called from tests/float/math_builtins.c:469.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:400: 
+[eva] tests/float/math_builtins.c:470: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:400: 
+[eva] tests/float/math_builtins.c:470: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:400: Warning: 
+[eva:alarm] tests/float/math_builtins.c:470: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:401.
+  Called from tests/float/math_builtins.c:471.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:402: 
+[eva] tests/float/math_builtins.c:472: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:402: 
+[eva] tests/float/math_builtins.c:472: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:402: Warning: 
+[eva:alarm] tests/float/math_builtins.c:472: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] computing for function double_interval <- test_fmod <- main.
-  Called from tests/float/math_builtins.c:403.
+  Called from tests/float/math_builtins.c:473.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:404: 
+[eva] tests/float/math_builtins.c:474: 
   Call to builtin Frama_C_fmod for function fmod
-[eva] tests/float/math_builtins.c:404: 
+[eva] tests/float/math_builtins.c:474: 
   function fmod: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:404: Warning: 
+[eva:alarm] tests/float/math_builtins.c:474: Warning: 
   function fmod: precondition 'finite_logic_result' got status unknown.
 [eva] Recording results for test_fmod
 [eva] Done for function test_fmod
 [eva] computing for function test_sqrt_det <- main.
-  Called from tests/float/math_builtins.c:665.
-[eva] tests/float/math_builtins.c:408: 
+  Called from tests/float/math_builtins.c:738.
+[eva] tests/float/math_builtins.c:478: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:408: 
+[eva] tests/float/math_builtins.c:478: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:408: 
+[eva] tests/float/math_builtins.c:478: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:409: 
+[eva] tests/float/math_builtins.c:479: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:410: 
+[eva] tests/float/math_builtins.c:480: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:410: 
+[eva] tests/float/math_builtins.c:480: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:410: Warning: 
+[eva:alarm] tests/float/math_builtins.c:480: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:411: 
+[eva] tests/float/math_builtins.c:481: 
   function sqrt: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:412: 
+[eva] tests/float/math_builtins.c:482: 
   function sqrt: precondition 'arg_positive' got status valid.
 [eva] Recording results for test_sqrt_det
 [eva] Done for function test_sqrt_det
 [eva] computing for function test_sqrt <- main.
-  Called from tests/float/math_builtins.c:666.
+  Called from tests/float/math_builtins.c:739.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:416.
+  Called from tests/float/math_builtins.c:486.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:417: 
+[eva] tests/float/math_builtins.c:487: 
   function sqrt: precondition 'arg_positive' got status valid.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:418.
+  Called from tests/float/math_builtins.c:488.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:419: 
+[eva] tests/float/math_builtins.c:489: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:419: 
+[eva] tests/float/math_builtins.c:489: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:419: Warning: 
+[eva:alarm] tests/float/math_builtins.c:489: Warning: 
   function sqrt: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:420.
+  Called from tests/float/math_builtins.c:490.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:421: 
+[eva] tests/float/math_builtins.c:491: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:421: 
+[eva] tests/float/math_builtins.c:491: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:421: Warning: 
+[eva:alarm] tests/float/math_builtins.c:491: Warning: 
   function sqrt: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrt <- main.
-  Called from tests/float/math_builtins.c:422.
+  Called from tests/float/math_builtins.c:492.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:423: 
+[eva] tests/float/math_builtins.c:493: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:423: 
+[eva] tests/float/math_builtins.c:493: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:423: Warning: 
+[eva:alarm] tests/float/math_builtins.c:493: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_sqrt
 [eva] Done for function test_sqrt
 [eva] computing for function test_exp_det <- main.
-  Called from tests/float/math_builtins.c:667.
-[eva] tests/float/math_builtins.c:446: 
+  Called from tests/float/math_builtins.c:740.
+[eva] tests/float/math_builtins.c:516: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:446: 
+[eva] tests/float/math_builtins.c:516: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:446: 
+[eva] tests/float/math_builtins.c:516: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:447: 
+[eva] tests/float/math_builtins.c:517: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:448: 
+[eva] tests/float/math_builtins.c:518: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:449: 
+[eva] tests/float/math_builtins.c:519: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   function exp: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:450: 
+[eva] tests/float/math_builtins.c:520: 
   function exp: precondition 'finite_domain' got status valid.
-[eva] tests/float/math_builtins.c:451: 
+[eva] tests/float/math_builtins.c:521: 
   Call to builtin Frama_C_exp for function exp
-[eva] tests/float/math_builtins.c:451: 
+[eva] tests/float/math_builtins.c:521: 
   function exp: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:451: Warning: 
+[eva:alarm] tests/float/math_builtins.c:521: Warning: 
   function exp: precondition 'finite_domain' got status invalid.
 [eva] Recording results for test_exp_det
 [eva] Done for function test_exp_det
 [eva] computing for function test_log_det <- main.
-  Called from tests/float/math_builtins.c:668.
-[eva] tests/float/math_builtins.c:463: 
+  Called from tests/float/math_builtins.c:741.
+[eva] tests/float/math_builtins.c:533: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:463: 
+[eva] tests/float/math_builtins.c:533: 
   function log: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:463: 
+[eva] tests/float/math_builtins.c:533: 
   function log: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   function log: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:464: 
+[eva] tests/float/math_builtins.c:534: 
   function log: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:465: 
+[eva] tests/float/math_builtins.c:535: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:465: 
+[eva] tests/float/math_builtins.c:535: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:465: Warning: 
+[eva:alarm] tests/float/math_builtins.c:535: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:466: 
+[eva] tests/float/math_builtins.c:536: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:466: 
+[eva] tests/float/math_builtins.c:536: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:466: Warning: 
+[eva:alarm] tests/float/math_builtins.c:536: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:467: 
+[eva] tests/float/math_builtins.c:537: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:467: 
+[eva] tests/float/math_builtins.c:537: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:467: Warning: 
+[eva:alarm] tests/float/math_builtins.c:537: Warning: 
   function log: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:468: 
+[eva] tests/float/math_builtins.c:538: 
   Call to builtin Frama_C_log for function log
-[eva] tests/float/math_builtins.c:468: 
+[eva] tests/float/math_builtins.c:538: 
   function log: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:468: Warning: 
+[eva:alarm] tests/float/math_builtins.c:538: Warning: 
   function log: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log_det
 [eva] Done for function test_log_det
 [eva] computing for function test_log10_det <- main.
-  Called from tests/float/math_builtins.c:669.
-[eva] tests/float/math_builtins.c:481: 
+  Called from tests/float/math_builtins.c:742.
+[eva] tests/float/math_builtins.c:551: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:481: 
+[eva] tests/float/math_builtins.c:551: 
   function log10: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:481: 
+[eva] tests/float/math_builtins.c:551: 
   function log10: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   function log10: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:482: 
+[eva] tests/float/math_builtins.c:552: 
   function log10: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:483: 
+[eva] tests/float/math_builtins.c:553: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:483: 
+[eva] tests/float/math_builtins.c:553: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:483: Warning: 
+[eva:alarm] tests/float/math_builtins.c:553: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:484: 
+[eva] tests/float/math_builtins.c:554: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:484: 
+[eva] tests/float/math_builtins.c:554: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:484: Warning: 
+[eva:alarm] tests/float/math_builtins.c:554: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:485: 
+[eva] tests/float/math_builtins.c:555: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:485: 
+[eva] tests/float/math_builtins.c:555: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:485: Warning: 
+[eva:alarm] tests/float/math_builtins.c:555: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:486: 
+[eva] tests/float/math_builtins.c:556: 
   Call to builtin Frama_C_log10 for function log10
-[eva] tests/float/math_builtins.c:486: 
+[eva] tests/float/math_builtins.c:556: 
   function log10: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:486: Warning: 
+[eva:alarm] tests/float/math_builtins.c:556: Warning: 
   function log10: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log10_det
 [eva] Done for function test_log10_det
 [eva] computing for function test_powf_det <- main.
-  Called from tests/float/math_builtins.c:671.
-[eva] tests/float/math_builtins.c:86: 
+  Called from tests/float/math_builtins.c:744.
+[eva] tests/float/math_builtins.c:156: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:86: 
+[eva] tests/float/math_builtins.c:156: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:86: 
+[eva] tests/float/math_builtins.c:156: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:87: 
+[eva] tests/float/math_builtins.c:157: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:88: 
+[eva] tests/float/math_builtins.c:158: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:89: 
+[eva] tests/float/math_builtins.c:159: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:90: 
+[eva] tests/float/math_builtins.c:160: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:91: 
+[eva] tests/float/math_builtins.c:161: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:92: 
+[eva] tests/float/math_builtins.c:162: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:93: 
+[eva] tests/float/math_builtins.c:163: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf_det
 [eva] Done for function test_powf_det
 [eva] computing for function test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:672.
+  Called from tests/float/math_builtins.c:745.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:231.
+  Called from tests/float/math_builtins.c:301.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:233: 
+[eva] tests/float/math_builtins.c:303: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:233: 
+[eva] tests/float/math_builtins.c:303: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:233: Warning: 
+[eva:alarm] tests/float/math_builtins.c:303: Warning: 
   function powf: precondition 'finite_logic_res' got status invalid.
-[eva] tests/float/math_builtins.c:235: 
+[eva] tests/float/math_builtins.c:305: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:235: 
+[eva] tests/float/math_builtins.c:305: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:235: Warning: 
+[eva:alarm] tests/float/math_builtins.c:305: Warning: 
   function powf: precondition 'finite_logic_res' got status invalid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:238.
+  Called from tests/float/math_builtins.c:308.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:239: 
+[eva] tests/float/math_builtins.c:309: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:239: 
+[eva] tests/float/math_builtins.c:309: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:239: Warning: 
+[eva:alarm] tests/float/math_builtins.c:309: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:240: 
+[eva] tests/float/math_builtins.c:310: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:240: 
+[eva] tests/float/math_builtins.c:310: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:240: Warning: 
+[eva:alarm] tests/float/math_builtins.c:310: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:243: 
+[eva] tests/float/math_builtins.c:313: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:243: 
+[eva] tests/float/math_builtins.c:313: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:243: Warning: 
+[eva:alarm] tests/float/math_builtins.c:313: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
-[eva] tests/float/math_builtins.c:244: 
+[eva] tests/float/math_builtins.c:314: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:244: 
+[eva] tests/float/math_builtins.c:314: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:244: Warning: 
+[eva:alarm] tests/float/math_builtins.c:314: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:247.
+  Called from tests/float/math_builtins.c:317.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:248: 
+[eva] tests/float/math_builtins.c:318: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:249.
+  Called from tests/float/math_builtins.c:319.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:250: 
+[eva] tests/float/math_builtins.c:320: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:250: 
+[eva] tests/float/math_builtins.c:320: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:250: Warning: 
+[eva:alarm] tests/float/math_builtins.c:320: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:253.
+  Called from tests/float/math_builtins.c:323.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:254: 
+[eva] tests/float/math_builtins.c:324: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:255: 
+[eva] tests/float/math_builtins.c:325: 
   Frama_C_show_each_i: [0.0000000000000000 .. 1.0000000000000000*2^-120]
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:256.
+  Called from tests/float/math_builtins.c:326.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:257: 
+[eva] tests/float/math_builtins.c:327: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:258: Frama_C_show_each_j: {0}
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:328: Frama_C_show_each_j: {0}
+[eva] tests/float/math_builtins.c:332: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:332: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:262: 
+[eva] tests/float/math_builtins.c:332: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:263: 
+[eva] tests/float/math_builtins.c:333: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:265.
+  Called from tests/float/math_builtins.c:335.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:266: 
+[eva] tests/float/math_builtins.c:336: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:267: 
+[eva] tests/float/math_builtins.c:337: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:268: 
+[eva] tests/float/math_builtins.c:338: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:269: 
+[eva] tests/float/math_builtins.c:339: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:270: 
+[eva] tests/float/math_builtins.c:340: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf_singleton_exp <- main.
-  Called from tests/float/math_builtins.c:272.
+  Called from tests/float/math_builtins.c:342.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:273: 
+[eva] tests/float/math_builtins.c:343: 
   function powf: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:274: 
+[eva] tests/float/math_builtins.c:344: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf_singleton_exp
 [eva] Done for function test_powf_singleton_exp
 [eva] computing for function test_powf <- main.
-  Called from tests/float/math_builtins.c:673.
+  Called from tests/float/math_builtins.c:746.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:280.
+  Called from tests/float/math_builtins.c:350.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:281: 
+[eva] tests/float/math_builtins.c:351: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:282.
+  Called from tests/float/math_builtins.c:352.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:283: 
+[eva] tests/float/math_builtins.c:353: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:284.
+  Called from tests/float/math_builtins.c:354.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:285: 
+[eva] tests/float/math_builtins.c:355: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:291.
+  Called from tests/float/math_builtins.c:361.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:292.
+  Called from tests/float/math_builtins.c:362.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:293: 
+[eva] tests/float/math_builtins.c:363: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:293: 
+[eva] tests/float/math_builtins.c:363: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:293: Warning: 
+[eva:alarm] tests/float/math_builtins.c:363: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:294.
+  Called from tests/float/math_builtins.c:364.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:295: 
+[eva] tests/float/math_builtins.c:365: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:295: 
+[eva] tests/float/math_builtins.c:365: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:295: Warning: 
+[eva:alarm] tests/float/math_builtins.c:365: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:296.
+  Called from tests/float/math_builtins.c:366.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:297: 
+[eva] tests/float/math_builtins.c:367: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:297: 
+[eva] tests/float/math_builtins.c:367: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:297: Warning: 
+[eva:alarm] tests/float/math_builtins.c:367: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:298.
+  Called from tests/float/math_builtins.c:368.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:299.
+  Called from tests/float/math_builtins.c:369.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:300: 
+[eva] tests/float/math_builtins.c:370: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:303.
+  Called from tests/float/math_builtins.c:373.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:304.
+  Called from tests/float/math_builtins.c:374.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:305: 
+[eva] tests/float/math_builtins.c:375: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:308.
+  Called from tests/float/math_builtins.c:378.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:309.
+  Called from tests/float/math_builtins.c:379.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:310: 
+[eva] tests/float/math_builtins.c:380: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:310: 
+[eva] tests/float/math_builtins.c:380: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:310: Warning: 
+[eva:alarm] tests/float/math_builtins.c:380: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:313.
+  Called from tests/float/math_builtins.c:383.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:314.
+  Called from tests/float/math_builtins.c:384.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:315: 
+[eva] tests/float/math_builtins.c:385: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:315: 
+[eva] tests/float/math_builtins.c:385: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:315: Warning: 
+[eva:alarm] tests/float/math_builtins.c:385: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:319.
+  Called from tests/float/math_builtins.c:389.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:320.
+  Called from tests/float/math_builtins.c:390.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:321: 
+[eva] tests/float/math_builtins.c:391: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:321: 
+[eva] tests/float/math_builtins.c:391: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:321: Warning: 
+[eva:alarm] tests/float/math_builtins.c:391: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:324.
+  Called from tests/float/math_builtins.c:394.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:325.
+  Called from tests/float/math_builtins.c:395.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:326: 
+[eva] tests/float/math_builtins.c:396: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:326: 
+[eva] tests/float/math_builtins.c:396: 
   function powf: precondition 'finite_args' got status valid.
-[eva:alarm] tests/float/math_builtins.c:326: Warning: 
+[eva:alarm] tests/float/math_builtins.c:396: Warning: 
   function powf: precondition 'finite_logic_res' got status unknown.
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:329.
+  Called from tests/float/math_builtins.c:399.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
 [eva] computing for function double_interval <- test_powf <- main.
-  Called from tests/float/math_builtins.c:330.
+  Called from tests/float/math_builtins.c:400.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:331: 
+[eva] tests/float/math_builtins.c:401: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_powf
 [eva] Done for function test_powf
 [eva] computing for function test_sqrtf_det <- main.
-  Called from tests/float/math_builtins.c:674.
-[eva] tests/float/math_builtins.c:427: 
+  Called from tests/float/math_builtins.c:747.
+[eva] tests/float/math_builtins.c:497: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:427: 
+[eva] tests/float/math_builtins.c:497: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:427: 
+[eva] tests/float/math_builtins.c:497: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:428: 
+[eva] tests/float/math_builtins.c:498: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:429: 
+[eva] tests/float/math_builtins.c:499: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:429: 
+[eva] tests/float/math_builtins.c:499: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:429: Warning: 
+[eva:alarm] tests/float/math_builtins.c:499: Warning: 
   function sqrtf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:430: 
+[eva] tests/float/math_builtins.c:500: 
   function sqrtf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:431: 
+[eva] tests/float/math_builtins.c:501: 
   function sqrtf: precondition 'arg_positive' got status valid.
 [eva] Recording results for test_sqrtf_det
 [eva] Done for function test_sqrtf_det
 [eva] computing for function test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:675.
+  Called from tests/float/math_builtins.c:748.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:435.
+  Called from tests/float/math_builtins.c:505.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:436: 
+[eva] tests/float/math_builtins.c:506: 
   function sqrtf: precondition 'arg_positive' got status valid.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:437.
+  Called from tests/float/math_builtins.c:507.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:438: 
+[eva] tests/float/math_builtins.c:508: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:438: 
+[eva] tests/float/math_builtins.c:508: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:438: Warning: 
+[eva:alarm] tests/float/math_builtins.c:508: Warning: 
   function sqrtf: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:439.
+  Called from tests/float/math_builtins.c:509.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:440: 
+[eva] tests/float/math_builtins.c:510: 
   Call to builtin Frama_C_sqrtf for function sqrtf
-[eva] tests/float/math_builtins.c:440: 
+[eva] tests/float/math_builtins.c:510: 
   function sqrtf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:440: Warning: 
+[eva:alarm] tests/float/math_builtins.c:510: Warning: 
   function sqrtf: precondition 'arg_positive' got status unknown.
 [eva] computing for function double_interval <- test_sqrtf <- main.
-  Called from tests/float/math_builtins.c:441.
+  Called from tests/float/math_builtins.c:511.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:442: 
+[eva] tests/float/math_builtins.c:512: 
   Call to builtin Frama_C_sqrt for function sqrt
-[eva] tests/float/math_builtins.c:442: 
+[eva] tests/float/math_builtins.c:512: 
   function sqrt: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:442: Warning: 
+[eva:alarm] tests/float/math_builtins.c:512: Warning: 
   function sqrt: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_sqrtf
 [eva] Done for function test_sqrtf
 [eva] computing for function test_expf_det <- main.
-  Called from tests/float/math_builtins.c:676.
-[eva] tests/float/math_builtins.c:455: 
+  Called from tests/float/math_builtins.c:749.
+[eva] tests/float/math_builtins.c:525: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:455: 
+[eva] tests/float/math_builtins.c:525: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:455: 
+[eva] tests/float/math_builtins.c:525: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:456: 
+[eva] tests/float/math_builtins.c:526: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:457: 
+[eva] tests/float/math_builtins.c:527: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:458: 
+[eva] tests/float/math_builtins.c:528: 
   function expf: precondition 'res_finite' got status valid.
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   Call to builtin Frama_C_expf for function expf
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   function expf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:459: 
+[eva] tests/float/math_builtins.c:529: 
   function expf: precondition 'res_finite' got status valid.
 [eva] Recording results for test_expf_det
 [eva] Done for function test_expf_det
 [eva] computing for function test_logf_det <- main.
-  Called from tests/float/math_builtins.c:677.
-[eva] tests/float/math_builtins.c:472: 
+  Called from tests/float/math_builtins.c:750.
+[eva] tests/float/math_builtins.c:542: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:472: 
+[eva] tests/float/math_builtins.c:542: 
   function logf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:472: 
+[eva] tests/float/math_builtins.c:542: 
   function logf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   function logf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:473: 
+[eva] tests/float/math_builtins.c:543: 
   function logf: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:474: 
+[eva] tests/float/math_builtins.c:544: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:474: 
+[eva] tests/float/math_builtins.c:544: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:474: Warning: 
+[eva:alarm] tests/float/math_builtins.c:544: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:475: 
+[eva] tests/float/math_builtins.c:545: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:475: 
+[eva] tests/float/math_builtins.c:545: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:475: Warning: 
+[eva:alarm] tests/float/math_builtins.c:545: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:476: 
+[eva] tests/float/math_builtins.c:546: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:476: 
+[eva] tests/float/math_builtins.c:546: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:476: Warning: 
+[eva:alarm] tests/float/math_builtins.c:546: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:477: 
+[eva] tests/float/math_builtins.c:547: 
   Call to builtin Frama_C_logf for function logf
-[eva] tests/float/math_builtins.c:477: 
+[eva] tests/float/math_builtins.c:547: 
   function logf: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:477: Warning: 
+[eva:alarm] tests/float/math_builtins.c:547: Warning: 
   function logf: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_logf_det
 [eva] Done for function test_logf_det
 [eva] computing for function test_log10f_det <- main.
-  Called from tests/float/math_builtins.c:678.
-[eva] tests/float/math_builtins.c:490: 
+  Called from tests/float/math_builtins.c:751.
+[eva] tests/float/math_builtins.c:560: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:490: 
+[eva] tests/float/math_builtins.c:560: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:490: 
+[eva] tests/float/math_builtins.c:560: 
   function log10f: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:491: 
+[eva] tests/float/math_builtins.c:561: 
   function log10f: precondition 'arg_positive' got status valid.
-[eva] tests/float/math_builtins.c:492: 
+[eva] tests/float/math_builtins.c:562: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:492: 
+[eva] tests/float/math_builtins.c:562: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:492: Warning: 
+[eva:alarm] tests/float/math_builtins.c:562: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:493: 
+[eva] tests/float/math_builtins.c:563: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:493: 
+[eva] tests/float/math_builtins.c:563: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:493: Warning: 
+[eva:alarm] tests/float/math_builtins.c:563: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:494: 
+[eva] tests/float/math_builtins.c:564: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:494: 
+[eva] tests/float/math_builtins.c:564: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:494: Warning: 
+[eva:alarm] tests/float/math_builtins.c:564: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
-[eva] tests/float/math_builtins.c:495: 
+[eva] tests/float/math_builtins.c:565: 
   Call to builtin Frama_C_log10f for function log10f
-[eva] tests/float/math_builtins.c:495: 
+[eva] tests/float/math_builtins.c:565: 
   function log10f: precondition 'finite_arg' got status valid.
-[eva:alarm] tests/float/math_builtins.c:495: Warning: 
+[eva:alarm] tests/float/math_builtins.c:565: Warning: 
   function log10f: precondition 'arg_positive' got status invalid.
 [eva] Recording results for test_log10f_det
 [eva] Done for function test_log10f_det
 [eva] computing for function test_diff_pow_powf <- main.
-  Called from tests/float/math_builtins.c:680.
-[eva] tests/float/math_builtins.c:499: 
+  Called from tests/float/math_builtins.c:753.
+[eva] tests/float/math_builtins.c:569: 
   Call to builtin Frama_C_pow for function pow
-[eva] tests/float/math_builtins.c:499: 
+[eva] tests/float/math_builtins.c:569: 
   function pow: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:499: 
+[eva] tests/float/math_builtins.c:569: 
   function pow: precondition 'finite_logic_res' got status valid.
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   Call to builtin Frama_C_powf for function powf
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   function powf: precondition 'finite_args' got status valid.
-[eva] tests/float/math_builtins.c:500: 
+[eva] tests/float/math_builtins.c:570: 
   function powf: precondition 'finite_logic_res' got status valid.
 [eva] Recording results for test_diff_pow_powf
 [eva] Done for function test_diff_pow_powf
 [eva] computing for function test_floor_det <- main.
-  Called from tests/float/math_builtins.c:682.
-[eva] tests/float/math_builtins.c:504: 
+  Called from tests/float/math_builtins.c:755.
+[eva] tests/float/math_builtins.c:574: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:504: 
+[eva] tests/float/math_builtins.c:574: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:505: 
+[eva] tests/float/math_builtins.c:575: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:505: 
+[eva] tests/float/math_builtins.c:575: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:506: 
+[eva] tests/float/math_builtins.c:576: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:506: 
+[eva] tests/float/math_builtins.c:576: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:507: 
+[eva] tests/float/math_builtins.c:577: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:507: 
+[eva] tests/float/math_builtins.c:577: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:508: 
+[eva] tests/float/math_builtins.c:578: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:508: 
+[eva] tests/float/math_builtins.c:578: 
   function floor: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:509: 
+[eva] tests/float/math_builtins.c:579: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:509: 
+[eva] tests/float/math_builtins.c:579: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floor_det
 [eva] Done for function test_floor_det
 [eva] computing for function test_ceil_det <- main.
-  Called from tests/float/math_builtins.c:683.
-[eva] tests/float/math_builtins.c:513: 
+  Called from tests/float/math_builtins.c:756.
+[eva] tests/float/math_builtins.c:583: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:513: 
+[eva] tests/float/math_builtins.c:583: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:514: 
+[eva] tests/float/math_builtins.c:584: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:514: 
+[eva] tests/float/math_builtins.c:584: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:515: 
+[eva] tests/float/math_builtins.c:585: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:515: 
+[eva] tests/float/math_builtins.c:585: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:516: 
+[eva] tests/float/math_builtins.c:586: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:516: 
+[eva] tests/float/math_builtins.c:586: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:517: 
+[eva] tests/float/math_builtins.c:587: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:517: 
+[eva] tests/float/math_builtins.c:587: 
   function ceil: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:518: 
+[eva] tests/float/math_builtins.c:588: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:518: 
+[eva] tests/float/math_builtins.c:588: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceil_det
 [eva] Done for function test_ceil_det
 [eva] computing for function test_trunc_det <- main.
-  Called from tests/float/math_builtins.c:684.
-[eva] tests/float/math_builtins.c:522: 
+  Called from tests/float/math_builtins.c:757.
+[eva] tests/float/math_builtins.c:592: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:522: 
+[eva] tests/float/math_builtins.c:592: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:523: 
+[eva] tests/float/math_builtins.c:593: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:523: 
+[eva] tests/float/math_builtins.c:593: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:524: 
+[eva] tests/float/math_builtins.c:594: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:524: 
+[eva] tests/float/math_builtins.c:594: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:525: 
+[eva] tests/float/math_builtins.c:595: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:525: 
+[eva] tests/float/math_builtins.c:595: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:526: 
+[eva] tests/float/math_builtins.c:596: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:526: 
+[eva] tests/float/math_builtins.c:596: 
   function trunc: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:527: 
+[eva] tests/float/math_builtins.c:597: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:527: 
+[eva] tests/float/math_builtins.c:597: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_trunc_det
 [eva] Done for function test_trunc_det
 [eva] computing for function test_round_det <- main.
-  Called from tests/float/math_builtins.c:685.
-[eva] tests/float/math_builtins.c:531: 
+  Called from tests/float/math_builtins.c:758.
+[eva] tests/float/math_builtins.c:601: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:531: 
+[eva] tests/float/math_builtins.c:601: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:532: 
+[eva] tests/float/math_builtins.c:602: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:532: 
+[eva] tests/float/math_builtins.c:602: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:533: 
+[eva] tests/float/math_builtins.c:603: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:533: 
+[eva] tests/float/math_builtins.c:603: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:534: 
+[eva] tests/float/math_builtins.c:604: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:534: 
+[eva] tests/float/math_builtins.c:604: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:535: 
+[eva] tests/float/math_builtins.c:605: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:535: 
+[eva] tests/float/math_builtins.c:605: 
   function round: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:536: 
+[eva] tests/float/math_builtins.c:606: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:536: 
+[eva] tests/float/math_builtins.c:606: 
   function round: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_round_det
 [eva] Done for function test_round_det
 [eva] computing for function test_floor <- main.
-  Called from tests/float/math_builtins.c:686.
+  Called from tests/float/math_builtins.c:759.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:541.
+  Called from tests/float/math_builtins.c:611.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:542: 
+[eva] tests/float/math_builtins.c:612: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:542: 
+[eva] tests/float/math_builtins.c:612: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:543.
+  Called from tests/float/math_builtins.c:613.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:544: 
+[eva] tests/float/math_builtins.c:614: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:544: 
+[eva] tests/float/math_builtins.c:614: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floor <- main.
-  Called from tests/float/math_builtins.c:545.
+  Called from tests/float/math_builtins.c:615.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:546: 
+[eva] tests/float/math_builtins.c:616: 
   Call to builtin Frama_C_floor for function floor
-[eva] tests/float/math_builtins.c:546: 
+[eva] tests/float/math_builtins.c:616: 
   function floor: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floor
 [eva] Done for function test_floor
 [eva] computing for function test_ceil <- main.
-  Called from tests/float/math_builtins.c:687.
+  Called from tests/float/math_builtins.c:760.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:551.
+  Called from tests/float/math_builtins.c:621.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:552: 
+[eva] tests/float/math_builtins.c:622: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:552: 
+[eva] tests/float/math_builtins.c:622: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:553.
+  Called from tests/float/math_builtins.c:623.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:554: 
+[eva] tests/float/math_builtins.c:624: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:554: 
+[eva] tests/float/math_builtins.c:624: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceil <- main.
-  Called from tests/float/math_builtins.c:555.
+  Called from tests/float/math_builtins.c:625.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:556: 
+[eva] tests/float/math_builtins.c:626: 
   Call to builtin Frama_C_ceil for function ceil
-[eva] tests/float/math_builtins.c:556: 
+[eva] tests/float/math_builtins.c:626: 
   function ceil: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceil
 [eva] Done for function test_ceil
 [eva] computing for function test_trunc <- main.
-  Called from tests/float/math_builtins.c:688.
+  Called from tests/float/math_builtins.c:761.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:561.
+  Called from tests/float/math_builtins.c:631.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:562: 
+[eva] tests/float/math_builtins.c:632: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:562: 
+[eva] tests/float/math_builtins.c:632: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:563.
+  Called from tests/float/math_builtins.c:633.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:564: 
+[eva] tests/float/math_builtins.c:634: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:564: 
+[eva] tests/float/math_builtins.c:634: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_trunc <- main.
-  Called from tests/float/math_builtins.c:565.
+  Called from tests/float/math_builtins.c:635.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:566: 
+[eva] tests/float/math_builtins.c:636: 
   Call to builtin Frama_C_trunc for function trunc
-[eva] tests/float/math_builtins.c:566: 
+[eva] tests/float/math_builtins.c:636: 
   function trunc: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_trunc
 [eva] Done for function test_trunc
 [eva] computing for function test_round <- main.
-  Called from tests/float/math_builtins.c:689.
+  Called from tests/float/math_builtins.c:762.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:571.
+  Called from tests/float/math_builtins.c:641.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:572: 
+[eva] tests/float/math_builtins.c:642: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:572: 
+[eva] tests/float/math_builtins.c:642: 
   function round: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:573.
+  Called from tests/float/math_builtins.c:643.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:574: 
+[eva] tests/float/math_builtins.c:644: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:574: 
+[eva] tests/float/math_builtins.c:644: 
   function round: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_round <- main.
-  Called from tests/float/math_builtins.c:575.
+  Called from tests/float/math_builtins.c:645.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:576: 
+[eva] tests/float/math_builtins.c:646: 
   Call to builtin Frama_C_round for function round
-[eva] tests/float/math_builtins.c:576: 
+[eva] tests/float/math_builtins.c:646: 
   function round: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_round
 [eva] Done for function test_round
 [eva] computing for function test_floorf_det <- main.
-  Called from tests/float/math_builtins.c:691.
-[eva] tests/float/math_builtins.c:580: 
+  Called from tests/float/math_builtins.c:764.
+[eva] tests/float/math_builtins.c:650: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:580: 
+[eva] tests/float/math_builtins.c:650: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:581: 
+[eva] tests/float/math_builtins.c:651: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:581: 
+[eva] tests/float/math_builtins.c:651: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:582: 
+[eva] tests/float/math_builtins.c:652: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:582: 
+[eva] tests/float/math_builtins.c:652: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:583: 
+[eva] tests/float/math_builtins.c:653: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:583: 
+[eva] tests/float/math_builtins.c:653: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:584: 
+[eva] tests/float/math_builtins.c:654: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:584: 
+[eva] tests/float/math_builtins.c:654: 
   function floorf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:585: 
+[eva] tests/float/math_builtins.c:655: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:585: 
+[eva] tests/float/math_builtins.c:655: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floorf_det
 [eva] Done for function test_floorf_det
 [eva] computing for function test_ceilf_det <- main.
-  Called from tests/float/math_builtins.c:692.
-[eva] tests/float/math_builtins.c:589: 
+  Called from tests/float/math_builtins.c:765.
+[eva] tests/float/math_builtins.c:659: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:589: 
+[eva] tests/float/math_builtins.c:659: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:590: 
+[eva] tests/float/math_builtins.c:660: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:590: 
+[eva] tests/float/math_builtins.c:660: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:591: 
+[eva] tests/float/math_builtins.c:661: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:591: 
+[eva] tests/float/math_builtins.c:661: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:592: 
+[eva] tests/float/math_builtins.c:662: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:592: 
+[eva] tests/float/math_builtins.c:662: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:593: 
+[eva] tests/float/math_builtins.c:663: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:593: 
+[eva] tests/float/math_builtins.c:663: 
   function ceilf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:594: 
+[eva] tests/float/math_builtins.c:664: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:594: 
+[eva] tests/float/math_builtins.c:664: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceilf_det
 [eva] Done for function test_ceilf_det
 [eva] computing for function test_truncf_det <- main.
-  Called from tests/float/math_builtins.c:693.
-[eva] tests/float/math_builtins.c:598: 
+  Called from tests/float/math_builtins.c:766.
+[eva] tests/float/math_builtins.c:668: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:598: 
+[eva] tests/float/math_builtins.c:668: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:599: 
+[eva] tests/float/math_builtins.c:669: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:599: 
+[eva] tests/float/math_builtins.c:669: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:600: 
+[eva] tests/float/math_builtins.c:670: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:600: 
+[eva] tests/float/math_builtins.c:670: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:601: 
+[eva] tests/float/math_builtins.c:671: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:601: 
+[eva] tests/float/math_builtins.c:671: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:602: 
+[eva] tests/float/math_builtins.c:672: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:602: 
+[eva] tests/float/math_builtins.c:672: 
   function truncf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:603: 
+[eva] tests/float/math_builtins.c:673: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:603: 
+[eva] tests/float/math_builtins.c:673: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_truncf_det
 [eva] Done for function test_truncf_det
 [eva] computing for function test_roundf_det <- main.
-  Called from tests/float/math_builtins.c:694.
-[eva] tests/float/math_builtins.c:607: 
+  Called from tests/float/math_builtins.c:767.
+[eva] tests/float/math_builtins.c:677: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:607: 
+[eva] tests/float/math_builtins.c:677: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:608: 
+[eva] tests/float/math_builtins.c:678: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:608: 
+[eva] tests/float/math_builtins.c:678: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:609: 
+[eva] tests/float/math_builtins.c:679: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:609: 
+[eva] tests/float/math_builtins.c:679: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:610: 
+[eva] tests/float/math_builtins.c:680: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:610: 
+[eva] tests/float/math_builtins.c:680: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:611: 
+[eva] tests/float/math_builtins.c:681: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:611: 
+[eva] tests/float/math_builtins.c:681: 
   function roundf: precondition 'finite_arg' got status valid.
-[eva] tests/float/math_builtins.c:612: 
+[eva] tests/float/math_builtins.c:682: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:612: 
+[eva] tests/float/math_builtins.c:682: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_roundf_det
 [eva] Done for function test_roundf_det
 [eva] computing for function test_floorf <- main.
-  Called from tests/float/math_builtins.c:695.
+  Called from tests/float/math_builtins.c:768.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:617.
+  Called from tests/float/math_builtins.c:687.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:618: 
+[eva] tests/float/math_builtins.c:688: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:618: 
+[eva] tests/float/math_builtins.c:688: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:619.
+  Called from tests/float/math_builtins.c:689.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:620: 
+[eva] tests/float/math_builtins.c:690: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:620: 
+[eva] tests/float/math_builtins.c:690: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_floorf <- main.
-  Called from tests/float/math_builtins.c:621.
+  Called from tests/float/math_builtins.c:691.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:622: 
+[eva] tests/float/math_builtins.c:692: 
   Call to builtin Frama_C_floorf for function floorf
-[eva] tests/float/math_builtins.c:622: 
+[eva] tests/float/math_builtins.c:692: 
   function floorf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_floorf
 [eva] Done for function test_floorf
 [eva] computing for function test_ceilf <- main.
-  Called from tests/float/math_builtins.c:696.
+  Called from tests/float/math_builtins.c:769.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:627.
+  Called from tests/float/math_builtins.c:697.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:628: 
+[eva] tests/float/math_builtins.c:698: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:628: 
+[eva] tests/float/math_builtins.c:698: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:629.
+  Called from tests/float/math_builtins.c:699.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:630: 
+[eva] tests/float/math_builtins.c:700: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:630: 
+[eva] tests/float/math_builtins.c:700: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_ceilf <- main.
-  Called from tests/float/math_builtins.c:631.
+  Called from tests/float/math_builtins.c:701.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:632: 
+[eva] tests/float/math_builtins.c:702: 
   Call to builtin Frama_C_ceilf for function ceilf
-[eva] tests/float/math_builtins.c:632: 
+[eva] tests/float/math_builtins.c:702: 
   function ceilf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_ceilf
 [eva] Done for function test_ceilf
 [eva] computing for function test_truncf <- main.
-  Called from tests/float/math_builtins.c:697.
+  Called from tests/float/math_builtins.c:770.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:637.
+  Called from tests/float/math_builtins.c:707.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:638: 
+[eva] tests/float/math_builtins.c:708: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:638: 
+[eva] tests/float/math_builtins.c:708: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:639.
+  Called from tests/float/math_builtins.c:709.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:640: 
+[eva] tests/float/math_builtins.c:710: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:640: 
+[eva] tests/float/math_builtins.c:710: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_truncf <- main.
-  Called from tests/float/math_builtins.c:641.
+  Called from tests/float/math_builtins.c:711.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:642: 
+[eva] tests/float/math_builtins.c:712: 
   Call to builtin Frama_C_truncf for function truncf
-[eva] tests/float/math_builtins.c:642: 
+[eva] tests/float/math_builtins.c:712: 
   function truncf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_truncf
 [eva] Done for function test_truncf
 [eva] computing for function test_roundf <- main.
-  Called from tests/float/math_builtins.c:698.
+  Called from tests/float/math_builtins.c:771.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:647.
+  Called from tests/float/math_builtins.c:717.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:648: 
+[eva] tests/float/math_builtins.c:718: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:648: 
+[eva] tests/float/math_builtins.c:718: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:649.
+  Called from tests/float/math_builtins.c:719.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:650: 
+[eva] tests/float/math_builtins.c:720: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:650: 
+[eva] tests/float/math_builtins.c:720: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] computing for function double_interval <- test_roundf <- main.
-  Called from tests/float/math_builtins.c:651.
+  Called from tests/float/math_builtins.c:721.
 [eva] Recording results for double_interval
 [eva] Done for function double_interval
-[eva] tests/float/math_builtins.c:652: 
+[eva] tests/float/math_builtins.c:722: 
   Call to builtin Frama_C_roundf for function roundf
-[eva] tests/float/math_builtins.c:652: 
+[eva] tests/float/math_builtins.c:722: 
   function roundf: precondition 'finite_arg' got status valid.
 [eva] Recording results for test_roundf
 [eva] Done for function test_roundf
@@ -2301,6 +2432,38 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function double_interval:
   __retres ∈ [-1.2237906221789607*2^1023 .. 1.2237906221789607*2^1023]
+[eva:final-states] Values at end of function test_acos:
+  half_pi ∈ {1.5707963267948965}
+  pi ∈ {3.1415926535897931}
+  zero ∈ {0}
+  acos_image ∈ [0.0000000000000000 .. 3.1415926535897931]
+  x ∈ {1.0471975511965978}
+  y ∈ {2.0943951023931957}
+  xy ∈ [1.0471975511965978 .. 2.0943951023931957]
+  f32_half_pi ∈ {1.5707963705062866}
+  f32_pi ∈ {3.1415927410125732}
+  f32_zero ∈ {0}
+  f32_acosf_image ∈ [0.0000000000000000 .. 3.1415927410125732]
+[eva:final-states] Values at end of function test_asin:
+  zero ∈ {0}
+  minus_half_pi ∈ {-1.5707963267948965}
+  half_pi ∈ {1.5707963267948965}
+  asin_image ∈ [-1.5707963267948965 .. 1.5707963267948965]
+  x ∈ {-1.0471975511965978*2^-1}
+  y ∈ {1.0471975511965978*2^-1}
+  xy ∈ [-1.0471975511965978*2^-1 .. 1.0471975511965978*2^-1]
+  f32_zero ∈ {0}
+  f32_minus_half_pi ∈ {-1.5707963705062866}
+  f32_half_pi ∈ {1.5707963705062866}
+  f32_asinf_image ∈ [-1.5707963705062866 .. 1.5707963705062866]
+[eva:final-states] Values at end of function test_atan:
+  zero ∈ {0}
+  atan_image ∈ [-1.5707963267948965 .. 1.5707963267948965]
+  x ∈ {-1.1071487177940904}
+  y ∈ {1.1071487177940904}
+  xy ∈ [-1.1071487177940904 .. 1.1071487177940904]
+  f32_zero ∈ {0}
+  f32_atanf_image ∈ [-1.5707963705062866 .. 1.5707963705062866]
 [eva:final-states] Values at end of function test_atan2:
   x ∈ [1.0000000000000000 .. 5.0000000000000000]
   y ∈ [-0.0000000000000000 .. 0.0000000000000000]
@@ -2618,6 +2781,24 @@
   __retres ∈ {0}
 [from] Computing for function double_interval
 [from] Done for function double_interval
+[from] Computing for function test_acos
+[from] Computing for function acos <-test_acos
+[from] Done for function acos
+[from] Computing for function acosf <-test_acos
+[from] Done for function acosf
+[from] Done for function test_acos
+[from] Computing for function test_asin
+[from] Computing for function asin <-test_asin
+[from] Done for function asin
+[from] Computing for function asinf <-test_asin
+[from] Done for function asinf
+[from] Done for function test_asin
+[from] Computing for function test_atan
+[from] Computing for function atan <-test_atan
+[from] Done for function atan
+[from] Computing for function atanf <-test_atan
+[from] Done for function atanf
+[from] Done for function test_atan
 [from] Computing for function test_atan2
 [from] Computing for function atan2 <-test_atan2
 [from] Done for function atan2
@@ -2744,8 +2925,20 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function acos:
+  \result FROM x
+[from] Function acosf:
+  \result FROM x
+[from] Function asin:
+  \result FROM x
+[from] Function asinf:
+  \result FROM x
+[from] Function atan:
+  \result FROM x
 [from] Function atan2:
   \result FROM y; x
+[from] Function atanf:
+  \result FROM x
 [from] Function ceil:
   \result FROM x
 [from] Function ceilf:
@@ -2786,6 +2979,12 @@
   \result FROM x
 [from] Function sqrtf:
   \result FROM x
+[from] Function test_acos:
+  NO EFFECTS
+[from] Function test_asin:
+  NO EFFECTS
+[from] Function test_atan:
+  NO EFFECTS
 [from] Function test_atan2:
   NO EFFECTS
 [from] Function test_atan2_det:
@@ -2875,6 +3074,20 @@
     __retres
 [inout] Inputs for function double_interval:
     nondet
+[inout] Out (internal) for function test_acos:
+    half_pi; pi; zero; acos_image; bottom; bottom_0; x; y; xy; f32_half_pi;
+    f32_pi; f32_zero; f32_acosf_image; bottom_1
+[inout] Inputs for function test_acos:
+    nondet; any_double; any_float
+[inout] Out (internal) for function test_asin:
+    zero; minus_half_pi; half_pi; asin_image; bottom; bottom_0; x; y; xy;
+    f32_zero; f32_minus_half_pi; f32_half_pi; f32_asinf_image; bottom_1
+[inout] Inputs for function test_asin:
+    nondet; any_double; any_float
+[inout] Out (internal) for function test_atan:
+    zero; atan_image; x; y; xy; f32_zero; f32_atanf_image
+[inout] Inputs for function test_atan:
+    nondet; any_double; any_float
 [inout] Out (internal) for function test_atan2:
     x; y; a; b; c; d; e; f; g; h; i; j; k; l; m; n
 [inout] Inputs for function test_atan2:
@@ -3040,11 +3253,13 @@
 [inout] Out (internal) for function main:
     __retres
 [inout] Inputs for function main:
-    nondet
+    nondet; any_double; any_float
 /* Generated by Frama-C */
 #include "errno.h"
 #include "math.h"
 static int volatile nondet;
+static double volatile any_double;
+static float volatile any_float;
 double double_interval(double min, double max)
 {
   double __retres;
@@ -3075,6 +3290,79 @@ void test_sin_det(void)
   return;
 }
 
+extern int ( /* missing proto */ Frama_C_show_each_bottom)();
+
+void test_acos(void)
+{
+  double half_pi = acos(0.);
+  double pi = acos(- 1.);
+  double zero = acos(1.);
+  double acos_image = acos(any_double);
+  if (nondet) {
+    double bottom = acos(- 1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom_0 = acos(1.5);
+    Frama_C_show_each_bottom(bottom_0);
+  }
+  double x = acos(0.5);
+  double y = acos(- 0.5);
+  double xy = double_interval(- 0.5,0.5);
+  xy = acos(xy);
+  float f32_half_pi = acosf(0.f);
+  float f32_pi = acosf(- 1.f);
+  float f32_zero = acosf(1.f);
+  float f32_acosf_image = acosf(any_float);
+  if (nondet) {
+    float bottom_1 = acosf(2.f);
+    Frama_C_show_each_bottom(bottom_1);
+  }
+  return;
+}
+
+void test_asin(void)
+{
+  double zero = asin(0.);
+  double minus_half_pi = asin(- 1.);
+  double half_pi = asin(1.);
+  double asin_image = asin(any_double);
+  if (nondet) {
+    double bottom = asin(- 1.5);
+    Frama_C_show_each_bottom(bottom);
+  }
+  if (nondet) {
+    double bottom_0 = asin(1.5);
+    Frama_C_show_each_bottom(bottom_0);
+  }
+  double x = asin(- 0.5);
+  double y = asin(0.5);
+  double xy = double_interval(- 0.5,0.5);
+  xy = asin(xy);
+  float f32_zero = asinf(0.f);
+  float f32_minus_half_pi = asinf(- 1.f);
+  float f32_half_pi = asinf(1.f);
+  float f32_asinf_image = asinf(any_float);
+  if (nondet) {
+    float bottom_1 = asinf(2.f);
+    Frama_C_show_each_bottom(bottom_1);
+  }
+  return;
+}
+
+void test_atan(void)
+{
+  double zero = atan(0.);
+  double atan_image = atan(any_double);
+  double x = atan(- 2.);
+  double y = atan(2.);
+  double xy = double_interval(- 2.,2.);
+  xy = atan(xy);
+  float f32_zero = atanf(0.f);
+  float f32_atanf_image = atanf(any_float);
+  return;
+}
+
 void test_atan2_det(void)
 {
   double a = atan2(1.,0.);
@@ -3903,6 +4191,9 @@ int main(void)
   int __retres;
   test_cos_det();
   test_sin_det();
+  test_acos();
+  test_asin();
+  test_atan();
   test_atan2_det();
   test_atan2();
   test_pow_det();
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 6019d52b6974e590ed64929f0443da77b325f790..c3f8b8d2b91ee064a2084b5a3c0cfa2241763c11 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2409,265 +2409,103 @@
 --- Properties of Function 'acos'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'positive_result'
+[ Extern  ] Post-condition 'positive_result'
             ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 131)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 138)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 131)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 131)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 138)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 138)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 134)
+[ Extern  ] Froms (file share/libc/math.h, line 132)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'acosf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'positive_result'
+[ Extern  ] Post-condition 'positive_result'
             ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 145)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 152)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 145)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 145)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 152)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 152)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 148)
+[ Extern  ] Froms (file share/libc/math.h, line 138)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'acosl'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'positive_result'
+[ Extern  ] Post-condition 'positive_result'
             ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 159)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 166)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 159)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 159)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 166)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 166)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 162)
+[ Extern  ] Froms (file share/libc/math.h, line 144)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'asin'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'finite_result'
+[ Extern  ] Post-condition 'finite_result'
             ensures finite_result: \is_finite(\result)
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 173)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 180)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 173)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 173)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 180)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 180)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 176)
+[ Extern  ] Froms (file share/libc/math.h, line 150)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'asinf'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'finite_result'
+[ Extern  ] Post-condition 'finite_result'
             ensures finite_result: \is_finite(\result)
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 187)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 194)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 187)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 187)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 194)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 194)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 190)
+[ Extern  ] Froms (file share/libc/math.h, line 156)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'asinl'
 --------------------------------------------------------------------------------
 
-[ Extern  ] Post-condition for 'normal' 'finite_result'
+[ Extern  ] Post-condition 'finite_result'
             ensures finite_result: \is_finite(\result)
             Unverifiable but considered Valid.
-[ Extern  ] Post-condition for 'domain_error' 'errno_set'
-            ensures errno_set: __fc_errno ≡ 1
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 201)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 208)
-            assigns __fc_errno, \result;
-            Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'normal' nothing
+[ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 201)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 201)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 208)
-            assigns __fc_errno \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 208)
-            assigns \result \from x;
-            Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 204)
+[ Extern  ] Froms (file share/libc/math.h, line 162)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
             default behavior
             by Frama-C kernel.
-[  Valid  ] Behavior 'domain_error'
-            behavior domain_error
-            by Frama-C kernel.
-[  Valid  ] Behavior 'normal'
-            behavior normal
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'atanf'
@@ -2682,7 +2520,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 215)
+[ Extern  ] Froms (file share/libc/math.h, line 168)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2702,7 +2540,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 222)
+[ Extern  ] Froms (file share/libc/math.h, line 175)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2722,7 +2560,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 229)
+[ Extern  ] Froms (file share/libc/math.h, line 182)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2739,7 +2577,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 237)
+[ Extern  ] Froms (file share/libc/math.h, line 190)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2756,7 +2594,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 244)
+[ Extern  ] Froms (file share/libc/math.h, line 197)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2779,7 +2617,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 252)
+[ Extern  ] Froms (file share/libc/math.h, line 205)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2799,7 +2637,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 259)
+[ Extern  ] Froms (file share/libc/math.h, line 212)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2819,7 +2657,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 266)
+[ Extern  ] Froms (file share/libc/math.h, line 219)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2839,7 +2677,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 273)
+[ Extern  ] Froms (file share/libc/math.h, line 226)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2859,7 +2697,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 280)
+[ Extern  ] Froms (file share/libc/math.h, line 233)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2879,7 +2717,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 287)
+[ Extern  ] Froms (file share/libc/math.h, line 240)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2899,10 +2737,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 298)
+[ Extern  ] Assigns (file share/libc/math.h, line 251)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 309)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 262)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -2911,22 +2749,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 298)
+[ Extern  ] Froms (file share/libc/math.h, line 251)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 298)
+[ Extern  ] Froms (file share/libc/math.h, line 251)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 309)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 262)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 309)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 262)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 305)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 258)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 301)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 254)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2955,10 +2793,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 316)
+[ Extern  ] Assigns (file share/libc/math.h, line 269)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 327)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 280)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -2967,22 +2805,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 316)
+[ Extern  ] Froms (file share/libc/math.h, line 269)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 316)
+[ Extern  ] Froms (file share/libc/math.h, line 269)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 327)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 280)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 327)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 280)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 323)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 276)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 319)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 272)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3011,10 +2849,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 334)
+[ Extern  ] Assigns (file share/libc/math.h, line 287)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 345)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 298)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -3023,22 +2861,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 334)
+[ Extern  ] Froms (file share/libc/math.h, line 287)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 334)
+[ Extern  ] Froms (file share/libc/math.h, line 287)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 345)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 298)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 345)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 298)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 341)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 294)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 337)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 290)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3067,7 +2905,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 373)
+[ Extern  ] Froms (file share/libc/math.h, line 326)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3087,7 +2925,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 381)
+[ Extern  ] Froms (file share/libc/math.h, line 334)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3104,7 +2942,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 411)
+[ Extern  ] Froms (file share/libc/math.h, line 364)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3121,7 +2959,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 418)
+[ Extern  ] Froms (file share/libc/math.h, line 371)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3138,7 +2976,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 425)
+[ Extern  ] Froms (file share/libc/math.h, line 378)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3155,7 +2993,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 432)
+[ Extern  ] Froms (file share/libc/math.h, line 385)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3172,7 +3010,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 439)
+[ Extern  ] Froms (file share/libc/math.h, line 392)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3189,7 +3027,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 446)
+[ Extern  ] Froms (file share/libc/math.h, line 399)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3206,7 +3044,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 457)
+[ Extern  ] Froms (file share/libc/math.h, line 410)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3223,7 +3061,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 464)
+[ Extern  ] Froms (file share/libc/math.h, line 417)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3240,7 +3078,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 471)
+[ Extern  ] Froms (file share/libc/math.h, line 424)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3265,7 +3103,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 497)
+[ Extern  ] Froms (file share/libc/math.h, line 450)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3290,7 +3128,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 505)
+[ Extern  ] Froms (file share/libc/math.h, line 458)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3315,7 +3153,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 513)
+[ Extern  ] Froms (file share/libc/math.h, line 466)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3332,7 +3170,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 526)
+[ Extern  ] Froms (file share/libc/math.h, line 479)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3349,7 +3187,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 533)
+[ Extern  ] Froms (file share/libc/math.h, line 486)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3378,7 +3216,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 542)
+[ Extern  ] Froms (file share/libc/math.h, line 495)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3401,7 +3239,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 551)
+[ Extern  ] Froms (file share/libc/math.h, line 504)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3421,7 +3259,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 560)
+[ Extern  ] Froms (file share/libc/math.h, line 513)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3438,7 +3276,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 583)
+[ Extern  ] Froms (file share/libc/math.h, line 536)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3455,7 +3293,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 589)
+[ Extern  ] Froms (file share/libc/math.h, line 542)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3472,7 +3310,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 596)
+[ Extern  ] Froms (file share/libc/math.h, line 549)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3489,7 +3327,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 602)
+[ Extern  ] Froms (file share/libc/math.h, line 555)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3506,7 +3344,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 608)
+[ Extern  ] Froms (file share/libc/math.h, line 561)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3523,7 +3361,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 614)
+[ Extern  ] Froms (file share/libc/math.h, line 567)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3540,7 +3378,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 636)
+[ Extern  ] Froms (file share/libc/math.h, line 589)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3557,7 +3395,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 642)
+[ Extern  ] Froms (file share/libc/math.h, line 595)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3574,7 +3412,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 648)
+[ Extern  ] Froms (file share/libc/math.h, line 601)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3591,7 +3429,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 662)
+[ Extern  ] Froms (file share/libc/math.h, line 615)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3608,7 +3446,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 668)
+[ Extern  ] Froms (file share/libc/math.h, line 621)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3625,7 +3463,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 674)
+[ Extern  ] Froms (file share/libc/math.h, line 627)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3642,7 +3480,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 681)
+[ Extern  ] Froms (file share/libc/math.h, line 634)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3659,7 +3497,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 688)
+[ Extern  ] Froms (file share/libc/math.h, line 641)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3676,7 +3514,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 709)
+[ Extern  ] Froms (file share/libc/math.h, line 662)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3693,7 +3531,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 716)
+[ Extern  ] Froms (file share/libc/math.h, line 669)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3710,7 +3548,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 723)
+[ Extern  ] Froms (file share/libc/math.h, line 676)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3727,7 +3565,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 771)
+[ Extern  ] Froms (file share/libc/math.h, line 724)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3744,7 +3582,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 777)
+[ Extern  ] Froms (file share/libc/math.h, line 730)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -4106,9 +3944,9 @@
 --------------------------------------------------------------------------------
 --- Status Report Summary
 --------------------------------------------------------------------------------
-   181 Completely validated
+   169 Completely validated
     16 Locally validated
-   494 Considered valid
+   452 Considered valid
     56 To be validated
-   747 Total
+   693 Total
 --------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6e164aa81579b0f8146b9ca5e60b583632cce8f7..70a3baea5cd3d9cb5d0a3884f8a27b5b2437c965 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2835,135 +2835,45 @@ int __fc_fpclassifyf(float x);
  */
 int __fc_fpclassify(double x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern double acos(double x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern float acosf(float x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern long double acosl(long double x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures finite_result: \is_finite(\result);
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures finite_result: \is_finite(\result);
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern double asin(double x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures finite_result: \is_finite(\result);
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures finite_result: \is_finite(\result);
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern float asinf(float x);
 
-/*@ assigns __fc_errno, \result;
-    assigns __fc_errno \from x;
+/*@ requires in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
+    ensures finite_result: \is_finite(\result);
+    assigns \result;
     assigns \result \from x;
-    
-    behavior normal:
-      assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1;
-      ensures finite_result: \is_finite(\result);
-      assigns \result;
-      assigns \result \from x;
-    
-    behavior domain_error:
-      assumes
-        out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1);
-      ensures errno_set: __fc_errno ≡ 1;
-      assigns __fc_errno, \result;
-      assigns __fc_errno \from x;
-      assigns \result \from x;
-    
-    disjoint behaviors domain_error, normal;
  */
 extern long double asinl(long double x);
 
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index cf2aaaa418c7a222f1075e5c20d0b5d874d4c60a..9f997874c0f244b3e9afeb9b62afb588a606109d 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -29,98 +29,60 @@
   infinity ∈ {inf}
   fp_ilogb0 ∈ {-2147483648.}
   fp_ilogbnan ∈ {-2147483648.}
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
-[eva] using specification for function atan
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
-[eva] Done for function atan
-[eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: Call to builtin atan
 [eva:alarm] tests/libc/math_h.c:45: Warning: 
   function atan: precondition 'finite_arg' got status unknown.
-[eva] Done for function atan
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
-[eva] using specification for function atanf
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
-[eva] Done for function atanf
-[eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: Call to builtin atanf
 [eva:alarm] tests/libc/math_h.c:46: Warning: 
   function atanf: precondition 'finite_arg' got status unknown.
-[eva] Done for function atanf
 [eva] computing for function atanl <- main.
   Called from tests/libc/math_h.c:47.
 [eva] using specification for function atanl
@@ -309,24 +271,24 @@
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  atan_pi ∈ [-1.571 .. 1.571]
-  atan_half_pi ∈ [-1.571 .. 1.571]
-  atan_e ∈ [-1.571 .. 1.571]
-  atan_zero ∈ [-1.571 .. 1.571]
-  atan_minus_zero ∈ [-1.571 .. 1.571]
-  atan_one ∈ [-1.571 .. 1.571]
-  atan_minus_one ∈ [-1.571 .. 1.571]
-  atan_large ∈ [-1.571 .. 1.571]
-  atan_top ∈ [-1.571 .. 1.571]
-  atanf_f_pi ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_half_pi ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_e ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_zero ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_minus_zero ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_one ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_minus_one ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_large ∈ [-1.57099997997 .. 1.57099997997]
-  atanf_f_top ∈ [-1.57099997997 .. 1.57099997997]
+  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.262627244}
+  atanf_f_half_pi ∈ {1.00388479233}
+  atanf_f_e ∈ {1.218282938}
+  atanf_zero ∈ {0}
+  atanf_minus_zero ∈ {-0.}
+  atanf_one ∈ {0.785398185253}
+  atanf_minus_one ∈ {-0.785398185253}
+  atanf_large ∈ {1.57079637051}
+  atanf_f_top ∈ [-1.57079637051 .. 1.57079637051] ∪ {NaN}
   atanl_ld_pi ∈ [-inf .. inf]
   atanl_ld_half_pi ∈ [-inf .. inf]
   atanl_ld_e ∈ [-inf .. inf]