diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 76a1baafa01abf2cb3cc44f03e3769be62ef1409..926e4c6571ea7138238380b0d5b41920fc592b92 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,10 +1,10 @@
 /* run.config*
    OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
    OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
-   OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+   OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
    OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
    OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
-   OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+   OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
 */
 
 #include "__fc_builtin.h"
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 702ae9ed8649aed621c855c09d3d9b6614778aab..116cdb8b400156c488caf18419e3e10a02c053af 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -204,8 +204,6 @@
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
   Called from tests/float/nonlin.c:109.
-[eva:alarm] tests/float/nonlin.c:76: Warning: 
-  non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:77: 
   non-linear '(double)ff * (double)ff', lv 'ff'
 [eva:nonlin] tests/float/nonlin.c:77: subdividing on ff
@@ -213,10 +211,6 @@
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
   Called from tests/float/nonlin.c:110.
-[eva:alarm] tests/float/nonlin.c:81: Warning: 
-  non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:82: Warning: 
-  non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v1 * (double)v1', lv 'v1'
 [eva:nonlin] tests/float/nonlin.c:83: 
@@ -227,16 +221,9 @@
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
   Called from tests/float/nonlin.c:111.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
-  non-finite float value.
-  assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
 [eva] tests/float/nonlin.c:89: 
   Assigning imprecise value to a_0.
   The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
-  non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
-  non-finite float value. assert \is_finite((float)(a_0 + a_0));
 [eva] tests/float/nonlin.c:90: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
@@ -255,9 +242,6 @@
 [eva:nonlin] tests/float/nonlin.c:103: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
 [eva:nonlin] tests/float/nonlin.c:103: subdividing on f
-[eva:alarm] tests/float/nonlin.c:103: Warning: 
-  non-finite float value.
-  assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
 [eva] Recording results for around_zeros
 [eva] Done for function around_zeros
 [eva] Recording results for main
@@ -270,8 +254,8 @@
 [eva:final-states] Values at end of function around_zeros:
   Frama_C_entropy_source ∈ [--..--]
   f1 ∈ {0x1.0000000000000p-149}
-  f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
-  res ∈ {-0x1.0000000000000p0}
+  f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
+  res ∈ [-0x1.0000000000000p0 .. inf]
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
@@ -286,9 +270,9 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  v1 ∈ [-inf .. inf] ∪ {NaN}
+  v2 ∈ [-inf .. inf] ∪ {NaN}
+  square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
@@ -304,8 +288,8 @@
   rbits1 ∈ {0; 1; 2}
   rbits2 ∈ {0; 1}
 [eva:final-states] Values at end of function split_alarm:
-  ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+  ff ∈ [-inf .. inf] ∪ {NaN}
+  d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 3f173370a07378228f7f65b238c616648d520f24..e041a4b9edf6c2ba43533323437c505765adea95 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -204,8 +204,6 @@
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
   Called from tests/float/nonlin.c:109.
-[eva:alarm] tests/float/nonlin.c:76: Warning: 
-  non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:77: 
   non-linear '(double)ff * (double)ff', lv 'ff'
 [eva:nonlin] tests/float/nonlin.c:77: subdividing on ff
@@ -213,10 +211,6 @@
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
   Called from tests/float/nonlin.c:110.
-[eva:alarm] tests/float/nonlin.c:81: Warning: 
-  non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:82: Warning: 
-  non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v1 * (double)v1', lv 'v1'
 [eva:nonlin] tests/float/nonlin.c:83: 
@@ -227,16 +221,9 @@
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
   Called from tests/float/nonlin.c:111.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
-  non-finite float value.
-  assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
 [eva] tests/float/nonlin.c:89: 
   Assigning imprecise value to a_0.
   The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
-  non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
-  non-finite float value. assert \is_finite((float)(a_0 + a_0));
 [eva] tests/float/nonlin.c:90: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
@@ -255,9 +242,6 @@
 [eva:nonlin] tests/float/nonlin.c:103: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
 [eva:nonlin] tests/float/nonlin.c:103: subdividing on f
-[eva:alarm] tests/float/nonlin.c:103: Warning: 
-  non-finite float value.
-  assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
 [eva] Recording results for around_zeros
 [eva] Done for function around_zeros
 [eva] Recording results for main
@@ -270,8 +254,8 @@
 [eva:final-states] Values at end of function around_zeros:
   Frama_C_entropy_source ∈ [--..--]
   f1 ∈ {0x1.0000000000000p-149}
-  f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
-  res ∈ {-0x1.0000000000000p0}
+  f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
+  res ∈ [-0x1.0000000000000p0 .. inf]
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
@@ -286,9 +270,9 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  v1 ∈ [-inf .. inf] ∪ {NaN}
+  v2 ∈ [-inf .. inf] ∪ {NaN}
+  square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
@@ -304,8 +288,8 @@
   rbits1 ∈ {0; 1; 2}
   rbits2 ∈ {0; 1}
 [eva:final-states] Values at end of function split_alarm:
-  ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+  ff ∈ [-inf .. inf] ∪ {NaN}
+  d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]