diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 35fa2d83ce93c43e8e4c11aa05621578ab18b3a3..4d258f382ae1e2e040e0e55988c3b6a782ca1b64 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -81,6 +81,15 @@ void norm() {
   float v1 = v;
   float v2 = v;
   double square = (double)v1*v1+(double)v2*v2;
+  v1 = Frama_C_float_interval(-1e22, 1e18);
+  v2 = Frama_C_float_interval(-1e22, 1e18);
+  /* Without subdivision, v1*v1 = v2*v2 = [-∞..∞]. Thus the subdivision of [v1]
+     only (or [v2] only) cannot improve the precision of the final expression,
+     while the subdivision of both variables leads to a positive interval.
+     To be precise here, the subdivision should not be stopped when it does not
+     improve the final interval but other subdivisions might. Note that a single
+     split of each variable at 0 is enough to achieve maximal precision here. */
+  float square2 = v1*v1 + v2*v2;
 }
 
 // a bug resulted in an invalid interval due to the presence of garbled mix
@@ -104,6 +113,33 @@ void around_zeros() {
   float res = f1 / (f+f-f - f1);
 }
 
+volatile FLOAT nondet;
+
+/* This function is carefully designed to illustrate the difference between
+   several strategies to subdivide a floating-point interval. In particular,
+   float_interval provides two implementations to cut in half an interval:
+   1. cut the interval at the mathematical average between its two bounds.
+   2. balance the number of representable floating-point values in both
+      resulting intervals. */
+void subdivide_strategy () {
+  FLOAT x, d;
+  x = Frama_C_float_interval(-0.1, 100);
+  /* Square of an interval not centered at 0: starting the subdivisions by
+     splitting the interval between negative and positive values greatly
+     improves the precision on such code. */
+  FLOAT square1 = x * x;
+  x = nondet;
+  d = 0.125;
+  /* Here the optimal subdivision is to cut the interval at [d]. As [d] is close
+     to 0, the "balance" split is better as it splits intervals closer to 0. */
+  FLOAT square2 = (x - d) * (x - d);
+  x = Frama_C_float_interval(-4e4, 4e4);
+  d = 1e4;
+  /* Here the optimal subdivision is to cut the interval at [d]. As [d] is close
+     to the average between 0 and max(x), the "average" split is better. */
+  FLOAT square3 = (x - d) * (x - d);
+}
+
 void main() {
   nonlin_f();
   other ();
@@ -111,4 +147,5 @@ void main() {
   norm();
   garbled();
   around_zeros();
+  subdivide_strategy();
 }
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 051d2eeaf89092b9813bc11e31ad87959a6e2865..648a1ae9af5f33b985dcd3411249ebe3e07a77c4 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -153,7 +154,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -188,7 +189,7 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [eva:alarm] tests/float/nonlin.c:76: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:alarm] tests/float/nonlin.c:77: Warning: 
@@ -199,44 +200,88 @@
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [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] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v1 * v1));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v2 * v2));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
+  Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning: 
   non-finite float value.
   assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
-[eva] tests/float/nonlin.c:89: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite((float)(a_0 + a_0));
-[eva] tests/float/nonlin.c:90: 
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:alarm] tests/float/nonlin.c:104: Warning: 
+[eva:alarm] tests/float/nonlin.c:113: 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] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:alarm] tests/float/nonlin.c:131: Warning: 
+  non-finite double value. assert \is_finite(nondet);
+[eva:alarm] tests/float/nonlin.c:135: Warning: 
+  non-finite double value.
+  assert \is_finite((double)((double)(x_0 - d_0) * (double)(x_0 - d_0)));
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -252,7 +297,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -263,9 +308,11 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
   square ∈ [-0x1.fffffc0000020p256 .. 0x1.fffffc0000020p256]
+  square2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
@@ -283,6 +330,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
   d_0 ∈ [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.4000005000000p3 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
+  square3 ∈ [-0x1.65a0bc0000000p30 .. 0x1.2a05f20000000p31]
 [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.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 9811f59ffe15cdfca96a0da91b9da3175f63166f..3605d95496f4a537cef62c1739a71cf0018cf255 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -157,7 +158,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -203,7 +204,7 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [eva:alarm] tests/float/nonlin.c:76: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:77: 
@@ -212,7 +213,7 @@
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [eva:alarm] tests/float/nonlin.c:81: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:alarm] tests/float/nonlin.c:82: Warning: 
@@ -223,43 +224,97 @@
   non-linear '(double)v2 * (double)v2', lv 'v2'
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v1
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v2
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v1 * v1', lv 'v1'
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v2 * v2', lv 'v2'
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v1 * v1));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v2 * v2));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
+  Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning: 
   non-finite float value.
   assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
-[eva] tests/float/nonlin.c:89: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite((float)(a_0 + a_0));
-[eva] tests/float/nonlin.c:90: 
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:104: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:104: 
+[eva:nonlin] tests/float/nonlin.c:113: non-linear '(f + f) - f', lv 'f'
+[eva:nonlin] tests/float/nonlin.c:113: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
-[eva:nonlin] tests/float/nonlin.c:104: subdividing on f
-[eva:alarm] tests/float/nonlin.c:104: Warning: 
+[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
+[eva:alarm] tests/float/nonlin.c:113: 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] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:130: non-linear 'x_0 * x_0', lv 'x_0'
+[eva:nonlin] tests/float/nonlin.c:130: subdividing on x_0
+[eva:alarm] tests/float/nonlin.c:131: Warning: 
+  non-finite double value. assert \is_finite(nondet);
+[eva:nonlin] tests/float/nonlin.c:135: 
+  non-linear '(x_0 - d_0) * (x_0 - d_0)', lv 'd_0, x_0'
+[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
+[eva:alarm] tests/float/nonlin.c:135: Warning: 
+  non-finite double value.
+  assert \is_finite((double)((double)(x_0 - d_0) * (double)(x_0 - d_0)));
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:140: subdividing on x_0
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -275,7 +330,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -286,9 +341,11 @@
   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]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
   square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  square2 ∈ [-0x1.a618a60000000p123 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
@@ -306,6 +363,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
   d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.c1e15ac305198p-13 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffffffffffp1001 .. 0x1.fffffffffffffp1023]
+  square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
 [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.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 1ee6463ceac50b1170fa0a4df98880e7dc5478d1..3e52ec0cee57fd0518732d725a540b65e8ba015b 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -157,7 +158,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -203,47 +204,89 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [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
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v1 * (double)v1', lv 'v1'
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v2 * (double)v2', lv 'v2'
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v1
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v2
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v1 * v1', lv 'v1'
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v2 * v2', lv 'v2'
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva] tests/float/nonlin.c:89: 
+  Called from tests/float/nonlin.c:148.
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva] tests/float/nonlin.c:90: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:104: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:104: 
+[eva:nonlin] tests/float/nonlin.c:113: non-linear '(f + f) - f', lv 'f'
+[eva:nonlin] tests/float/nonlin.c:113: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
-[eva:nonlin] tests/float/nonlin.c:104: subdividing on f
+[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
 [eva] Recording results for around_zeros
 [eva] Done for function around_zeros
+[eva] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:130: non-linear 'x_0 * x_0', lv 'x_0'
+[eva:nonlin] tests/float/nonlin.c:130: subdividing on x_0
+[eva:nonlin] tests/float/nonlin.c:135: 
+  non-linear '(x_0 - d_0) * (x_0 - d_0)', lv 'd_0, x_0'
+[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:140: subdividing on x_0
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -259,7 +302,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -270,9 +313,11 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-inf .. inf] ∪ {NaN}
-  v2 ∈ [-inf .. inf] ∪ {NaN}
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
   square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
+  square2 ∈ [-inf .. inf] ∪ {NaN}
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
@@ -290,6 +335,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-inf .. inf] ∪ {NaN}
   d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.c1e15ac305198p-13 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffffffffffp1014 .. inf] ∪ {NaN}
+  square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
 [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.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index ca363536807906bb21daed0dd032f8c3f974b9a8..c3e1e9cdb8b72a6f1a433932db7cf78cbfcc82bc 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -153,7 +154,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -188,7 +189,7 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [eva:alarm] tests/float/nonlin.c:76: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:alarm] tests/float/nonlin.c:77: Warning: 
@@ -199,44 +200,88 @@
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [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] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v1 * v1));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v2 * v2));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
+  Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning: 
   non-finite float value.
   assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
-[eva] tests/float/nonlin.c:89: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite((float)(a_0 + a_0));
-[eva] tests/float/nonlin.c:90: 
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:alarm] tests/float/nonlin.c:104: Warning: 
+[eva:alarm] tests/float/nonlin.c:113: 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] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:alarm] tests/float/nonlin.c:131: Warning: 
+  non-finite float value. assert \is_finite(nondet);
+[eva:alarm] tests/float/nonlin.c:135: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(x_0 - d_0) * (float)(x_0 - d_0)));
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -252,7 +297,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -263,9 +308,11 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
-  v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
   square ∈ [-0x1.fffffc0000020p256 .. 0x1.fffffc0000020p256]
+  square2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
@@ -283,6 +330,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
   d_0 ∈ [-0x1.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.4000000000000p3 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
+  square3 ∈ [-0x1.65a0bc0000000p30 .. 0x1.2a05f20000000p31]
 [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.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index 45139110f67ea6ef7f5ed1ea11435db694f741e4..37f4cb97df6d0d60043fa37bacce7135e9289bb8 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -157,7 +158,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -203,7 +204,7 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [eva:alarm] tests/float/nonlin.c:76: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:nonlin] tests/float/nonlin.c:77: 
@@ -212,7 +213,7 @@
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [eva:alarm] tests/float/nonlin.c:81: Warning: 
   non-finite float value. assert \is_finite(v);
 [eva:alarm] tests/float/nonlin.c:82: Warning: 
@@ -223,43 +224,97 @@
   non-linear '(double)v2 * (double)v2', lv 'v2'
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v1
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v2
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v1 * v1', lv 'v1'
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v2 * v2', lv 'v2'
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v1 * v1));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value. assert \is_finite((float)(v2 * v2));
+[eva:alarm] tests/float/nonlin.c:92: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva:alarm] tests/float/nonlin.c:89: Warning: 
+  Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning: 
   non-finite float value.
   assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
-[eva] tests/float/nonlin.c:89: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning: 
+[eva:alarm] tests/float/nonlin.c:99: Warning: 
   non-finite float value. assert \is_finite((float)(a_0 + a_0));
-[eva] tests/float/nonlin.c:90: 
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:104: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:104: 
+[eva:nonlin] tests/float/nonlin.c:113: non-linear '(f + f) - f', lv 'f'
+[eva:nonlin] tests/float/nonlin.c:113: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
-[eva:nonlin] tests/float/nonlin.c:104: subdividing on f
-[eva:alarm] tests/float/nonlin.c:104: Warning: 
+[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
+[eva:alarm] tests/float/nonlin.c:113: 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] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:130: non-linear 'x_0 * x_0', lv 'x_0'
+[eva:nonlin] tests/float/nonlin.c:130: subdividing on x_0
+[eva:alarm] tests/float/nonlin.c:131: Warning: 
+  non-finite float value. assert \is_finite(nondet);
+[eva:nonlin] tests/float/nonlin.c:135: 
+  non-linear '(x_0 - d_0) * (x_0 - d_0)', lv 'd_0, x_0'
+[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
+[eva:alarm] tests/float/nonlin.c:135: Warning: 
+  non-finite float value.
+  assert \is_finite((float)((float)(x_0 - d_0) * (float)(x_0 - d_0)));
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:140: subdividing on x_0
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -275,7 +330,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -286,9 +341,11 @@
   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]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0133220000000p64 .. 0x1.bc16d60000000p59]
   square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  square2 ∈ [-0x1.a618a60000000p123 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
@@ -306,6 +363,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
   d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.c1e2e00000000p-13 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffe0000000p105 .. 0x1.fffffe0000000p127]
+  square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
 [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 9da885a3918b348ea4ce28d3aa3f6c7d272d46db..531c482e3f6ceec95bed03dbeb7402fd3b8d6576 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -35,8 +35,9 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:108.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
   Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
@@ -157,7 +158,7 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:109.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
   Called from tests/float/nonlin.c:61.
 [eva] tests/float/nonlin.c:61: 
@@ -203,47 +204,89 @@
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:110.
+  Called from tests/float/nonlin.c:146.
 [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
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:111.
+  Called from tests/float/nonlin.c:147.
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v1 * (double)v1', lv 'v1'
 [eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v2 * (double)v2', lv 'v2'
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v1
 [eva:nonlin] tests/float/nonlin.c:83: subdividing on v2
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:84.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:84: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] computing for function Frama_C_float_interval <- norm <- main.
+  Called from tests/float/nonlin.c:85.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:85: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v1 * v1', lv 'v1'
+[eva:nonlin] tests/float/nonlin.c:92: non-linear 'v2 * v2', lv 'v2'
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
+[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
 [eva] Recording results for norm
 [eva] Done for function norm
 [eva] computing for function garbled <- main.
-  Called from tests/float/nonlin.c:112.
-[eva] tests/float/nonlin.c:89: 
+  Called from tests/float/nonlin.c:148.
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva] tests/float/nonlin.c:90: 
+  The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
+[eva] tests/float/nonlin.c:99: 
   Assigning imprecise value to f.
   The imprecision originates from Arithmetic
 [eva] Recording results for garbled
 [eva] Done for function garbled
 [eva] computing for function around_zeros <- main.
-  Called from tests/float/nonlin.c:113.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:99.
-[eva] tests/float/nonlin.c:99: 
+  Called from tests/float/nonlin.c:108.
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:99: 
+[eva] tests/float/nonlin.c:108: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:104: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:104: 
+[eva:nonlin] tests/float/nonlin.c:113: non-linear '(f + f) - f', lv 'f'
+[eva:nonlin] tests/float/nonlin.c:113: 
   non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
-[eva:nonlin] tests/float/nonlin.c:104: subdividing on f
+[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
 [eva] Recording results for around_zeros
 [eva] Done for function around_zeros
+[eva] computing for function subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:150.
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:126.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:126: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:130: non-linear 'x_0 * x_0', lv 'x_0'
+[eva:nonlin] tests/float/nonlin.c:130: subdividing on x_0
+[eva:nonlin] tests/float/nonlin.c:135: 
+  non-linear '(x_0 - d_0) * (x_0 - d_0)', lv 'd_0, x_0'
+[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
+[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
+  Called from tests/float/nonlin.c:136.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:136: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:140: subdividing on x_0
+[eva] Recording results for subdivide_strategy
+[eva] Done for function subdivide_strategy
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -259,7 +302,7 @@
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:89}) }}
+      (origin: Arithmetic {tests/float/nonlin.c:98}) }}
   f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
 [eva:final-states] Values at end of function nonlin_f:
   Frama_C_entropy_source ∈ [--..--]
@@ -270,9 +313,11 @@
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
 [eva:final-states] Values at end of function norm:
-  v1 ∈ [-inf .. inf] ∪ {NaN}
-  v2 ∈ [-inf .. inf] ∪ {NaN}
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
   square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
+  square2 ∈ [-inf .. inf] ∪ {NaN}
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
   i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
@@ -290,6 +335,13 @@
 [eva:final-states] Values at end of function split_alarm:
   ff ∈ [-inf .. inf] ∪ {NaN}
   d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
+[eva:final-states] Values at end of function subdivide_strategy:
+  Frama_C_entropy_source ∈ [--..--]
+  x_0 ∈ [-0x1.3880000000000p15 .. 0x1.3880000000000p15]
+  d_0 ∈ {0x1.3880000000000p13}
+  square1 ∈ [-0x1.c1e2e00000000p-13 .. 0x1.3880000000000p13]
+  square2 ∈ [-0x1.fffffe0000000p118 .. inf] ∪ {NaN}
+  square3 ∈ [-0x0.0000000000000p0 .. 0x1.2a05f20000000p31]
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]