diff --git a/src/kernel_services/abstract_interp/float_interval.ml b/src/kernel_services/abstract_interp/float_interval.ml
index a881b71694746b3f6618aa9965359110d8a2ec4a..3e56c2698cff3c237c42c01559b334b719e0f5bb 100644
--- a/src/kernel_services/abstract_interp/float_interval.ml
+++ b/src/kernel_services/abstract_interp/float_interval.ml
@@ -1100,10 +1100,10 @@ module Make (F: Float_sig.S) = struct
                                    Subdivision
      ------------------------------------------------------------------------ *)
 
-  (* [avg] and [split] implement two different strategies for cutting a
+  (* [avg] and [balance] implement two different strategies for cutting a
      floating-point interval in half: [avg] computes the mathematical average of
-     the two bounds, while [split] balances the number of representable values
-     of the given precision in each resulting intervals. *)
+     the two bounds, while [balance] balances the number of representable double
+     values in each resulting intervals. *)
 
   (* Computes the average between two ocaml doubles. *)
   let avg x y =
@@ -1112,20 +1112,22 @@ module Make (F: Float_sig.S) = struct
     then fy +. (fx -. fy) /. 2.
     else (fx +. fy) /. 2.
 
-  (* assumption: [0. <= x <= y]. returns the median of the range [x..y]
+  (* Assumption: [0. <= x <= y]. Returns the median of the range [x..y]
      in number of double values. *)
-  let split_positive prec x y =
+  let _balance x y =
     let ix = Int64.bits_of_float (F.to_float x) in
     let iy = Int64.bits_of_float (F.to_float y) in
-    let f = Int64.(float_of_bits (add ix (div (sub iy ix) 2L))) in
-    F.of_float Near prec f
+    Int64.(float_of_bits (add ix (div (sub iy ix) 2L)))
 
-  (* assumption: [x <= y] *)
-  let _split prec x y =
+  (* Can be [avg] or [balance]. *)
+  let split_positive = avg
+
+  (* Assumption: [x <= y]. *)
+  let split x y =
     match F.is_negative x, F.is_negative y with
-    | false, false -> split_positive prec x y
-    | true, true -> F.neg (split_positive prec (F.neg x) (F.neg y))
-    | true, false -> Cst.neg_zero prec
+    | false, false -> split_positive x y
+    | true, true -> -. (split_positive (F.neg x) (F.neg y))
+    | true, false -> -0.
     | false, true -> assert false
 
   exception Can_not_subdiv = Abstract_interp.Can_not_subdiv
@@ -1149,7 +1151,7 @@ module Make (F: Float_sig.S) = struct
           else if Cmp.equal (F.next_float prec b) e
           then b, e
           else
-            let midpoint = avg b e in
+            let midpoint = split b e in
             let midpoint = F.of_float Down prec midpoint in
             let smidpoint =
               if F.is_exact prec then F.next_float prec midpoint else midpoint
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e0c3ad84a87a97dff76f7d8deca73869b486aa86..468438d093834bf3d11dcba23ae383702478c9fa 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1414,8 +1414,8 @@ module SpecialFloat =
       let option_name = "-warn-special-float"
       let default = "non-finite"
       let arg_name = "none|nan|non-finite"
-      let help = "generate alarms when special floats are produced: \
-                  infinite floats or NaN (by default), only on NaN or never."
+      let help = "generate alarms when special floats are produced: never, \
+                  only on NaN, or on infinite floats and NaN (by default)."
     end)
 let () = SpecialFloat.set_possible_values ["none"; "nan"; "non-finite"]
 
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 3ab7878306eaa3f8abb5ed4e234a11b1a79f4ffa..8a9e11f7da75422656b6e397593f80a4e2b6fa65 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -639,12 +639,14 @@ module Make
   (* Subdivision of the evaluation of the expression [expr], according to the
      values of a list of lvalues [lvals], in the state [state].
      [subexpr] is the smallest subexpression of [expr] containing all
-     occurrences of the lvalues in [lvals]. At the end of the subdivision, we
-     reduce the final value of [expr], [subexpr], and of the lvalues in [lvals].
+     occurrences of the lvalues in [lvals].
      [valuation] is the result of the evaluation of [expr] without subdivision.
-     This function returns the alarms and the valuation resulting from the
-     subdivided evaluation. *)
-  let subdivide_lvals context valuation subdivnb expr subexpr lvals =
+     The subdivision is stopped after [subdivnb] splits, or as soon as they can
+     no longer improve the precision of the value computed for [expr].
+     The function returns the alarms and the valuation resulting from the
+     subdivided evaluation. In the resulting valuation, the values of [expr],
+     [subexpr] and of the lvalues in [lvals] have been reduced. *)
+  let subdivide_lvals context valuation subdivnb ~expr ~subexpr lvals =
     let Hypotheses.L variables = Hypotheses.from_list lvals in
     (* Split function for the subvalues of [lvals]. *)
     let split = make_split valuation variables in
@@ -742,13 +744,15 @@ module Make
       (* List of non-linear subexpressions [subexpr], with the lvalues that
          appear multiple times in [subexpr], candidates for the subdivision. *)
       let vars = compute_non_linear expr in
+      (* Compute necessary information about the lvalues to be subdivided.
+         Also remove lvalues with pointer or singleton values. *)
+      let make_info = make_info_list context initial_valuation in
+      let vars_info = List.map (fun (e, lvals) -> e, make_info lvals) vars in
+      let vars_info = List.filter (fun (_, infos) -> infos <> []) vars_info in
       let rec subdivide_subexpr vars valuation result alarms =
         match vars with
         | [] -> `Value (valuation, result), alarms
-        | (subexpr, lvals) :: tail ->
-          (* Retrieve necessary information about the lvalues.
-             Also remove lvalues with pointer or singleton values. *)
-          let lvals_info = make_info_list context initial_valuation lvals in
+        | (subexpr, lvals_info) :: tail ->
           match lvals_info with
           | [] -> subdivide_subexpr tail valuation result alarms
           | _ ->
@@ -767,10 +771,29 @@ module Make
             Value_parameters.result ~current:true ~once:true ~dkey
               "subdividing on %a"
               (Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
-            subdivide_lvals context valuation subdivnb expr subexpr lvals_info
-            >>> subdivide_subexpr tail
+            let subdivide =
+              subdivide_lvals context valuation subdivnb lvals_info
+            in
+            (* If there are no other variables to subdivide, stops the
+               subdivision as soon as they can no longer improve the value
+               of the final expression [expr]. *)
+            if tail = []
+            then subdivide ~expr ~subexpr
+            else
+              (* Otherwise, later subdivisions on other sub-expressions may
+                 improve the value of [expr] thanks to a reduction of [subexpr],
+                 even if this reduction has not directly improved the value of
+                 [expr]. Thus, stop the subdivisions according to [subexpr]
+                 instead of [expr]. Use [~expr:subexpr], then evaluate [expr]
+                 with the reduced valuation, then continue to subdivide. *)
+              subdivide ~expr:subexpr ~subexpr >>> fun valuation _ _ ->
+              let valuation =
+                Clear.clear_englobing_exprs valuation ~expr ~subexpr
+              in
+              Eva.evaluate context valuation expr >>>
+              subdivide_subexpr tail
       in
-      subdivide_subexpr vars valuation result alarms
+      subdivide_subexpr vars_info valuation result alarms
 
   let evaluate context valuation ~subdivnb expr =
     if subdivnb = 0 || not activated
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 90deaf2c91746955b9fa3e61f2f3990e4e122b4b..aa8b1acdd17e86cc49a6c0b99653ae250fd3606a 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -142,8 +142,8 @@ end
 let compute_englobing_subexpr ~subexpr ~expr =
   let merge = Extlib.merge_opt (fun _ -> (@)) () in
   (* Returns [Some] of the list of subexpressions of [expr] that contain
-     [subexpr], apart from [expr] and [subexpr] themselves, or [None] if [subexpr]
-     does not appear in [expr]. *)
+     [subexpr], apart [subexpr] itself, or [None] if [subexpr] does not appear
+     in [expr]. *)
   let rec compute expr =
     if Cil_datatype.ExpStructEq.equal expr subexpr
     then Some []
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index fce3e9bc0c74fc2676ab43a99f858d5f474848bd..4d258f382ae1e2e040e0e55988c3b6a782ca1b64 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,8 +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 -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 -warn-special-float none
 */
 
 #include "__fc_builtin.h"
@@ -79,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
@@ -97,10 +108,38 @@ void around_zeros() {
   float f = Frama_C_float_interval(-0, f1);
   /* The +f-f is needed to activate the subdivisions.
      The [f1] value is removed from [f], which must become [-0. .. 0.]
-     and not the singleton {-0.}.  */
+     and not the singleton {-0.}.
+     No reduction when infinities are allowed (with -warn-special-float none). */
   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 ();
@@ -108,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 95c633d605b3c85d119c84dc019c403d42da933d..648a1ae9af5f33b985dcd3411249ebe3e07a77c4 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/nonlin.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/nonlin.c:75: Warning: 
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
   Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -35,116 +35,117 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:105.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:16.
+  Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   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 <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:17.
-[eva] tests/float/nonlin.c:17: 
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:17: 
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:20: assertion got status valid.
-[eva] tests/float/nonlin.c:24: assertion got status valid.
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4000000000000p2 .. 0x1.4800000000000p2],
   {{ "r2" }},
   [0x1.4000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4800000000000p2 .. 0x1.5000000000000p2],
   {{ "r2" }},
   [0x1.4800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5000000000000p2 .. 0x1.5800000000000p2],
   {{ "r2" }},
   [0x1.5000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5800000000000p2 .. 0x1.6000000000000p2],
   {{ "r2" }},
   [0x1.5800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6000000000000p2 .. 0x1.6800000000000p2],
   {{ "r2" }},
   [0x1.6000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6800000000000p2 .. 0x1.7000000000000p2],
   {{ "r2" }},
   [0x1.6800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7000000000000p2 .. 0x1.7800000000000p2],
   {{ "r2" }},
   [0x1.7000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7800000000000p2 .. 0x1.8000000000000p2],
   {{ "r2" }},
   [0x1.7800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8000000000000p2 .. 0x1.8800000000000p2],
   {{ "r2" }},
   [0x1.8000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8800000000000p2 .. 0x1.9000000000000p2],
   {{ "r2" }},
   [0x1.8800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9000000000000p2 .. 0x1.9800000000000p2],
   {{ "r2" }},
   [0x1.9000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9800000000000p2 .. 0x1.a000000000000p2],
   {{ "r2" }},
   [0x1.9800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a000000000000p2 .. 0x1.a800000000000p2],
   {{ "r2" }},
   [0x1.a000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a800000000000p2 .. 0x1.b000000000000p2],
   {{ "r2" }},
   [0x1.a800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b000000000000p2 .. 0x1.b800000000000p2],
   {{ "r2" }},
   [0x1.b000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b800000000000p2 .. 0x1.c000000000000p2],
@@ -153,45 +154,45 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:106.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
-  Called from tests/float/nonlin.c:59.
-[eva] tests/float/nonlin.c:59: 
+  Called from tests/float/nonlin.c:61.
+[eva] tests/float/nonlin.c:61: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:59: 
+[eva] tests/float/nonlin.c:61: 
   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 <- other <- main.
-  Called from tests/float/nonlin.c:60.
-[eva] tests/float/nonlin.c:60: 
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:60: 
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
   accessing out of bounds index.
   assert 0 ≤ (int)((double)((double)(i * i) + 2.0));
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
   accessing out of bounds index.
   assert (int)((double)((double)(i * i) + 2.0)) < 10;
 [eva] computing for function access_bits <- other <- main.
-  Called from tests/float/nonlin.c:67.
+  Called from tests/float/nonlin.c:69.
 [eva] Recording results for access_bits
 [eva] Done for function access_bits
 [eva] computing for function Frama_C_interval <- other <- main.
-  Called from tests/float/nonlin.c:69.
+  Called from tests/float/nonlin.c:71.
 [eva] using specification for function Frama_C_interval
-[eva] tests/float/nonlin.c:69: 
+[eva] tests/float/nonlin.c:71: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:alarm] tests/float/nonlin.c:70: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:107.
-[eva:alarm] tests/float/nonlin.c:74: Warning: 
+  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:75: Warning: 
+[eva:alarm] tests/float/nonlin.c:77: Warning: 
   non-finite double value.
   assert
   \is_finite((double)((double)1 /
@@ -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:108.
-[eva:alarm] tests/float/nonlin.c:79: Warning: 
+  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:80: Warning: 
+[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:109.
-[eva:alarm] tests/float/nonlin.c:87: 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:87: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:87}
-[eva:alarm] tests/float/nonlin.c:88: 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:88: 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:88: 
+[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:110.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:97.
-[eva] tests/float/nonlin.c:97: 
+  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:97: 
+[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:101: 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:87}) }}
+      (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 f1aa30fd850f5bf88444511a31c4390c0696ade2..3ddef66ef496f7061b9f8444af849b2b4bd1bafb 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/nonlin.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/nonlin.c:75: Warning: 
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
   Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -35,120 +35,121 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:105.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:16.
+  Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   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 <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:17.
-[eva] tests/float/nonlin.c:17: 
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:17: 
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:20: assertion got status valid.
-[eva:nonlin] tests/float/nonlin.c:22: non-linear 'a + b * (c - a)', lv 'a'
-[eva:nonlin] tests/float/nonlin.c:22: subdividing on a
-[eva] tests/float/nonlin.c:24: assertion got status valid.
-[eva:nonlin] tests/float/nonlin.c:41: non-linear 'b * (c - a) + a', lv 'a'
-[eva:nonlin] tests/float/nonlin.c:41: subdividing on a
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:24: non-linear 'a + b * (c - a)', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:24: subdividing on a
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:43: non-linear 'b * (c - a) + a', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:43: subdividing on a
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4000000000000p2 .. 0x1.4800000000000p2],
   {{ "r2" }},
   [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4800000000000p2 .. 0x1.5000000000000p2],
   {{ "r2" }},
   [0x1.4800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5000000000000p2 .. 0x1.5800000000000p2],
   {{ "r2" }},
   [0x1.5000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5800000000000p2 .. 0x1.6000000000000p2],
   {{ "r2" }},
   [0x1.5800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6000000000000p2 .. 0x1.6800000000000p2],
   {{ "r2" }},
   [0x1.6000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6800000000000p2 .. 0x1.7000000000000p2],
   {{ "r2" }},
   [0x1.6800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7000000000000p2 .. 0x1.7800000000000p2],
   {{ "r2" }},
   [0x1.7000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7800000000000p2 .. 0x1.8000000000000p2],
   {{ "r2" }},
   [0x1.7800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8000000000000p2 .. 0x1.8800000000000p2],
   {{ "r2" }},
   [0x1.8000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8800000000000p2 .. 0x1.9000000000000p2],
   {{ "r2" }},
   [0x1.8800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9000000000000p2 .. 0x1.9800000000000p2],
   {{ "r2" }},
   [0x1.9000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9800000000000p2 .. 0x1.a000000000000p2],
   {{ "r2" }},
   [0x1.9800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a000000000000p2 .. 0x1.a800000000000p2],
   {{ "r2" }},
   [0x1.a000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a800000000000p2 .. 0x1.b000000000000p2],
   {{ "r2" }},
   [0x1.a800000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b000000000000p2 .. 0x1.b800000000000p2],
   {{ "r2" }},
   [0x1.b000000000000p2 .. 0x1.c0fffffffffffp2]
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b800000000000p2 .. 0x1.c000000000000p2],
@@ -157,109 +158,163 @@
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:106.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
-  Called from tests/float/nonlin.c:59.
-[eva] tests/float/nonlin.c:59: 
+  Called from tests/float/nonlin.c:61.
+[eva] tests/float/nonlin.c:61: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:59: 
+[eva] tests/float/nonlin.c:61: 
   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 <- other <- main.
-  Called from tests/float/nonlin.c:60.
-[eva] tests/float/nonlin.c:60: 
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:60: 
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:61: non-linear 'i * i', lv 'i'
-[eva:nonlin] tests/float/nonlin.c:61: subdividing on i
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
+[eva:nonlin] tests/float/nonlin.c:63: non-linear 'i * i', lv 'i'
+[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
   accessing out of bounds index.
   assert (int)((double)((double)(i * i) + 2.0)) < 10;
-[eva:nonlin] tests/float/nonlin.c:62: non-linear 's - s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:62: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:63: non-linear 's - s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:63: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:64: non-linear 's + s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
 [eva:nonlin] tests/float/nonlin.c:64: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:65: non-linear 's * s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
 [eva:nonlin] tests/float/nonlin.c:65: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:66: non-linear 's * ((double)1 - s)', lv 's'
+[eva:nonlin] tests/float/nonlin.c:66: non-linear 's + s', lv 's'
 [eva:nonlin] tests/float/nonlin.c:66: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:67: non-linear 's * s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:67: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:68: non-linear 's * ((double)1 - s)', lv 's'
+[eva:nonlin] tests/float/nonlin.c:68: subdividing on s
 [eva] computing for function access_bits <- other <- main.
-  Called from tests/float/nonlin.c:67.
+  Called from tests/float/nonlin.c:69.
 [eva] Recording results for access_bits
 [eva] Done for function access_bits
 [eva] computing for function Frama_C_interval <- other <- main.
-  Called from tests/float/nonlin.c:69.
+  Called from tests/float/nonlin.c:71.
 [eva] using specification for function Frama_C_interval
-[eva] tests/float/nonlin.c:69: 
+[eva] tests/float/nonlin.c:71: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:nonlin] tests/float/nonlin.c:70: non-linear '(1 / x) * x', lv 'x'
-[eva:nonlin] tests/float/nonlin.c:70: subdividing on x
-[eva:alarm] tests/float/nonlin.c:70: Warning: division by zero. assert x ≢ 0;
+[eva:nonlin] tests/float/nonlin.c:72: non-linear '(1 / x) * x', lv 'x'
+[eva:nonlin] tests/float/nonlin.c:72: subdividing on x
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:107.
-[eva:alarm] tests/float/nonlin.c:74: Warning: 
+  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:75: 
+[eva:nonlin] tests/float/nonlin.c:77: 
   non-linear '(double)ff * (double)ff', lv 'ff'
-[eva:nonlin] tests/float/nonlin.c:75: subdividing on 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:108.
-[eva:alarm] tests/float/nonlin.c:79: Warning: 
+  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:80: Warning: 
+[eva:alarm] tests/float/nonlin.c:82: Warning: 
   non-finite float value. assert \is_finite(v);
-[eva:nonlin] tests/float/nonlin.c:81: 
+[eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v1 * (double)v1', lv 'v1'
-[eva:nonlin] tests/float/nonlin.c:81: 
+[eva:nonlin] tests/float/nonlin.c:83: 
   non-linear '(double)v2 * (double)v2', lv 'v2'
-[eva:nonlin] tests/float/nonlin.c:81: subdividing on v1
-[eva:nonlin] tests/float/nonlin.c:81: subdividing on 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:109.
-[eva:alarm] tests/float/nonlin.c:87: 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:87: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:87}
-[eva:alarm] tests/float/nonlin.c:88: 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:88: 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:88: 
+[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:110.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:97.
-[eva] tests/float/nonlin.c:97: 
+  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:97: 
+[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:101: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:101: 
+[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:101: subdividing on f
-[eva:alarm] tests/float/nonlin.c:101: 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:87}) }}
+      (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,26 +341,35 @@
   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]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cde0000000p64 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
-  i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+  i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+  zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
-  r ∈ [3..11]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
   x ∈ [1..42]
   y ∈ {0; 1}
-  z ∈ [-171874..171874]
+  z ∈ [-177499..177499]
   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]
+[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 ∈ [0x0.0000000000000p0 .. 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]
@@ -314,15 +378,15 @@
   r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
   r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
-  i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
+  i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.12ffffffffffep4 .. 0x1.12ffffffffffep4]
+  zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.b37ffffffff34p-7 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250000000034p-1]
-  r ∈ [3..11]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
   x ∈ [1..42]
   y ∈ {0; 1}
-  z ∈ [-171874..171874]
+  z ∈ [-177499..177499]
   rbits1 ∈ {0; 1; 2}
   rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index d8f939ec1d88d22950096d4bcd45a9dfe16bc7e4..ba81c19d44c306730614d89d500ccdb7fde507a5 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/nonlin.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/nonlin.c:75: Warning: 
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
   Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -35,271 +35,330 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:105.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:16.
+  Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   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 <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:17.
-[eva] tests/float/nonlin.c:17: 
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:17: 
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:20: assertion got status valid.
-[eva] tests/float/nonlin.c:24: assertion got status valid.
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:24: non-linear 'a + b * (c - a)', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:24: subdividing on a
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:43: non-linear 'b * (c - a) + a', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:43: subdividing on a
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4000000000000p2 .. 0x1.4800000000000p2],
   {{ "r2" }},
-  [0x1.4000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4800000000000p2 .. 0x1.5000000000000p2],
   {{ "r2" }},
-  [0x1.4800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.4800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5000000000000p2 .. 0x1.5800000000000p2],
   {{ "r2" }},
-  [0x1.5000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.5000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5800000000000p2 .. 0x1.6000000000000p2],
   {{ "r2" }},
-  [0x1.5800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.5800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6000000000000p2 .. 0x1.6800000000000p2],
   {{ "r2" }},
-  [0x1.6000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.6000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6800000000000p2 .. 0x1.7000000000000p2],
   {{ "r2" }},
-  [0x1.6800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.6800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7000000000000p2 .. 0x1.7800000000000p2],
   {{ "r2" }},
-  [0x1.7000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.7000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7800000000000p2 .. 0x1.8000000000000p2],
   {{ "r2" }},
-  [0x1.7800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.7800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8000000000000p2 .. 0x1.8800000000000p2],
   {{ "r2" }},
-  [0x1.8000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.8000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8800000000000p2 .. 0x1.9000000000000p2],
   {{ "r2" }},
-  [0x1.8800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.8800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9000000000000p2 .. 0x1.9800000000000p2],
   {{ "r2" }},
-  [0x1.9000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.9000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9800000000000p2 .. 0x1.a000000000000p2],
   {{ "r2" }},
-  [0x1.9800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.9800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a000000000000p2 .. 0x1.a800000000000p2],
   {{ "r2" }},
-  [0x1.a000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.a000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a800000000000p2 .. 0x1.b000000000000p2],
   {{ "r2" }},
-  [0x1.a800000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.a800000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b000000000000p2 .. 0x1.b800000000000p2],
   {{ "r2" }},
-  [0x1.b000000000000p2 .. 0x1.c800000000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.b000000000000p2 .. 0x1.c0fffffffffffp2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b800000000000p2 .. 0x1.c000000000000p2],
   {{ "r2" }},
-  [0x1.b800000000000p2 .. 0x1.c800000000000p2]
+  [0x1.b800000000000p2 .. 0x1.c0fffffffffffp2]
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:106.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
-  Called from tests/float/nonlin.c:59.
-[eva] tests/float/nonlin.c:59: 
+  Called from tests/float/nonlin.c:61.
+[eva] tests/float/nonlin.c:61: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:59: 
+[eva] tests/float/nonlin.c:61: 
   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 <- other <- main.
-  Called from tests/float/nonlin.c:60.
-[eva] tests/float/nonlin.c:60: 
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:60: 
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
+[eva:nonlin] tests/float/nonlin.c:63: non-linear 'i * i', lv 'i'
+[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
   accessing out of bounds index.
-  assert 0 ≤ (int)((double)((double)((float)(i * i)) + 2.0));
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
-  accessing out of bounds index.
-  assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+  assert (int)((double)((double)(i * i) + 2.0)) < 10;
+[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:65: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:66: non-linear 's + s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:66: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:67: non-linear 's * s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:67: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:68: non-linear 's * ((double)1 - s)', lv 's'
+[eva:nonlin] tests/float/nonlin.c:68: subdividing on s
 [eva] computing for function access_bits <- other <- main.
-  Called from tests/float/nonlin.c:67.
+  Called from tests/float/nonlin.c:69.
 [eva] Recording results for access_bits
 [eva] Done for function access_bits
 [eva] computing for function Frama_C_interval <- other <- main.
-  Called from tests/float/nonlin.c:69.
+  Called from tests/float/nonlin.c:71.
 [eva] using specification for function Frama_C_interval
-[eva] tests/float/nonlin.c:69: 
+[eva] tests/float/nonlin.c:71: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:alarm] tests/float/nonlin.c:70: Warning: division by zero. assert x ≢ 0;
+[eva:nonlin] tests/float/nonlin.c:72: non-linear '(1 / x) * x', lv 'x'
+[eva:nonlin] tests/float/nonlin.c:72: subdividing on x
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:107.
-[eva:alarm] tests/float/nonlin.c:74: Warning: 
-  non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:75: Warning: 
-  non-finite double value.
-  assert
-  \is_finite((double)((double)1 /
-                      (double)((double)((double)ff * (double)ff) + 0.000000001)));
+  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:108.
-[eva:alarm] tests/float/nonlin.c:79: Warning: 
-  non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:80: Warning: 
-  non-finite float value. assert \is_finite(v);
+  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:109.
-[eva:alarm] tests/float/nonlin.c:87: Warning: 
-  non-finite float value.
-  assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
-[eva] tests/float/nonlin.c:87: 
+  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:87}
-[eva:alarm] tests/float/nonlin.c:88: Warning: 
-  non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:88: Warning: 
-  non-finite float value. assert \is_finite((float)(a_0 + a_0));
-[eva] tests/float/nonlin.c:88: 
+  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:110.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:97.
-[eva] tests/float/nonlin.c:97: 
+  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:97: 
+[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:101: Warning: 
-  non-finite float value.
-  assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
+[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: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 ======
 [eva:final-states] Values at end of function access_bits:
   rbits1 ∈ {0; 1; 2}
-  x0 ∈ [0..3271884800]
+  x0 ∈ [--..--]
   __retres ∈ {0; 1}
 [eva:final-states] Values at end of function around_zeros:
   Frama_C_entropy_source ∈ [--..--]
   f1 ∈ {0x1.0000000000000p-149}
   f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
-  res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
+  res ∈ [-0x1.0000000000000p0 .. inf]
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:87}) }}
+      (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 ∈ [--..--]
   a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
   b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
   c ∈ {0x1.c000000000000p2}
-  r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
-  r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
+  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 ∈ [-0x1.fffffc0000020p256 .. 0x1.fffffc0000020p256]
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
+  square2 ∈ [0x0.0000000000000p0 .. inf]
 [eva:final-states] Values at end of function other:
   Frama_C_entropy_source ∈ [--..--]
-  i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.1300000000000p8 .. 0x1.1300000000000p8]
+  zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.2718000000000p14 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.2950000000000p14]
-  r ∈ [2..11]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
   x ∈ [1..42]
-  y ∈ [0..42]
-  z ∈ [-2750000..2750000]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
   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.fffffffffffffp1023 .. 0x1.fffffffffffffp1023]
+  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 ∈ [0x0.0000000000000p0 .. 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]
   b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
   c ∈ {0x1.c000000000000p2}
-  r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
-  r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffffffffffp2]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
-  i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  i ∈ [-0x1.8effffffffff7p1 .. 0x1.8680000000000p1]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.1300000000000p8 .. 0x1.1300000000000p8]
+  zf ∈ [-0x1.1bffffffffffcp4 .. 0x1.1bffffffffffcp4]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.2718000000000p14 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.2950000000000p14]
-  r ∈ [2..11]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dfffffffffep-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
   x ∈ [1..42]
-  y ∈ [0..42]
-  z ∈ [-2750000..2750000]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
   rbits1 ∈ {0; 1; 2}
   rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index 1a9170be5a49927871fee4b6f676bc4f1856b6aa..c3e1e9cdb8b72a6f1a433932db7cf78cbfcc82bc 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/float/nonlin.c (with preprocessing)
-[kernel:parser:decimal-float] tests/float/nonlin.c:75: Warning: 
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
   Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [eva] Analyzing a complete application starting at main
@@ -35,294 +35,325 @@
   rbits1 ∈ {0}
   rbits2 ∈ {0}
   v ∈ [--..--]
+  nondet ∈ [--..--]
 [eva] computing for function nonlin_f <- main.
-  Called from tests/float/nonlin.c:105.
+  Called from tests/float/nonlin.c:144.
 [eva] computing for function Frama_C_float_interval <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:16.
+  Called from tests/float/nonlin.c:18.
 [eva] using specification for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:16: 
+[eva] tests/float/nonlin.c:18: 
   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 <- nonlin_f <- main.
-  Called from tests/float/nonlin.c:17.
-[eva] tests/float/nonlin.c:17: 
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:17: 
+[eva] tests/float/nonlin.c:19: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva] tests/float/nonlin.c:20: assertion got status valid.
-[eva:nonlin] tests/float/nonlin.c:22: non-linear 'a + b * (c - a)', lv 'a'
-[eva:nonlin] tests/float/nonlin.c:22: subdividing on a
-[eva] tests/float/nonlin.c:24: assertion got status valid.
-[eva:nonlin] tests/float/nonlin.c:41: non-linear 'b * (c - a) + a', lv 'a'
-[eva:nonlin] tests/float/nonlin.c:41: subdividing on a
-[eva] tests/float/nonlin.c:42: 
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4000000000000p2 .. 0x1.4800000000000p2],
   {{ "r2" }},
-  [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.4000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.4800000000000p2 .. 0x1.5000000000000p2],
   {{ "r2" }},
-  [0x1.4800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.4800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5000000000000p2 .. 0x1.5800000000000p2],
   {{ "r2" }},
-  [0x1.5000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.5000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.5800000000000p2 .. 0x1.6000000000000p2],
   {{ "r2" }},
-  [0x1.5800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.5800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6000000000000p2 .. 0x1.6800000000000p2],
   {{ "r2" }},
-  [0x1.6000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.6000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.6800000000000p2 .. 0x1.7000000000000p2],
   {{ "r2" }},
-  [0x1.6800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.6800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7000000000000p2 .. 0x1.7800000000000p2],
   {{ "r2" }},
-  [0x1.7000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.7000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.7800000000000p2 .. 0x1.8000000000000p2],
   {{ "r2" }},
-  [0x1.7800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.7800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8000000000000p2 .. 0x1.8800000000000p2],
   {{ "r2" }},
-  [0x1.8000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.8000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.8800000000000p2 .. 0x1.9000000000000p2],
   {{ "r2" }},
-  [0x1.8800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.8800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9000000000000p2 .. 0x1.9800000000000p2],
   {{ "r2" }},
-  [0x1.9000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.9000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.9800000000000p2 .. 0x1.a000000000000p2],
   {{ "r2" }},
-  [0x1.9800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.9800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a000000000000p2 .. 0x1.a800000000000p2],
   {{ "r2" }},
-  [0x1.a000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.a000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.a800000000000p2 .. 0x1.b000000000000p2],
   {{ "r2" }},
-  [0x1.a800000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.a800000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b000000000000p2 .. 0x1.b800000000000p2],
   {{ "r2" }},
-  [0x1.b000000000000p2 .. 0x1.c0fffe0000000p2]
-[eva] tests/float/nonlin.c:42: 
+  [0x1.b000000000000p2 .. 0x1.c800000000000p2]
+[eva] tests/float/nonlin.c:44: 
   Frama_C_show_each_a_r2:
   {{ "a" }},
   [0x1.b800000000000p2 .. 0x1.c000000000000p2],
   {{ "r2" }},
-  [0x1.b800000000000p2 .. 0x1.c0fffe0000000p2]
+  [0x1.b800000000000p2 .. 0x1.c800000000000p2]
 [eva] Recording results for nonlin_f
 [eva] Done for function nonlin_f
 [eva] computing for function other <- main.
-  Called from tests/float/nonlin.c:106.
+  Called from tests/float/nonlin.c:145.
 [eva] computing for function Frama_C_float_interval <- other <- main.
-  Called from tests/float/nonlin.c:59.
-[eva] tests/float/nonlin.c:59: 
+  Called from tests/float/nonlin.c:61.
+[eva] tests/float/nonlin.c:61: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:59: 
+[eva] tests/float/nonlin.c:61: 
   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 <- other <- main.
-  Called from tests/float/nonlin.c:60.
-[eva] tests/float/nonlin.c:60: 
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'finite' got status valid.
-[eva] tests/float/nonlin.c:60: 
+[eva] tests/float/nonlin.c:62: 
   function Frama_C_float_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_float_interval
-[eva:nonlin] tests/float/nonlin.c:61: non-linear 'i * i', lv 'i'
-[eva:nonlin] tests/float/nonlin.c:61: subdividing on i
-[eva:alarm] tests/float/nonlin.c:61: Warning: 
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
+  accessing out of bounds index.
+  assert 0 ≤ (int)((double)((double)((float)(i * i)) + 2.0));
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
   accessing out of bounds index.
   assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
-[eva:nonlin] tests/float/nonlin.c:62: non-linear 's - s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:62: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:63: non-linear 's - s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:63: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:64: non-linear 's + s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:65: non-linear 's * s', lv 's'
-[eva:nonlin] tests/float/nonlin.c:65: subdividing on s
-[eva:nonlin] tests/float/nonlin.c:66: non-linear 's * ((float)1 - s)', lv 's'
-[eva:nonlin] tests/float/nonlin.c:66: subdividing on s
 [eva] computing for function access_bits <- other <- main.
-  Called from tests/float/nonlin.c:67.
+  Called from tests/float/nonlin.c:69.
 [eva] Recording results for access_bits
 [eva] Done for function access_bits
 [eva] computing for function Frama_C_interval <- other <- main.
-  Called from tests/float/nonlin.c:69.
+  Called from tests/float/nonlin.c:71.
 [eva] using specification for function Frama_C_interval
-[eva] tests/float/nonlin.c:69: 
+[eva] tests/float/nonlin.c:71: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:nonlin] tests/float/nonlin.c:70: non-linear '(1 / x) * x', lv 'x'
-[eva:nonlin] tests/float/nonlin.c:70: subdividing on x
-[eva:alarm] tests/float/nonlin.c:70: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
 [eva] Recording results for other
 [eva] Done for function other
 [eva] computing for function split_alarm <- main.
-  Called from tests/float/nonlin.c:107.
-[eva:alarm] tests/float/nonlin.c:74: Warning: 
+  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:75: 
-  non-linear '(double)ff * (double)ff', lv 'ff'
-[eva:nonlin] tests/float/nonlin.c:75: subdividing on ff
+[eva:alarm] tests/float/nonlin.c:77: Warning: 
+  non-finite double value.
+  assert
+  \is_finite((double)((double)1 /
+                      (double)((double)((double)ff * (double)ff) + 0.000000001)));
 [eva] Recording results for split_alarm
 [eva] Done for function split_alarm
 [eva] computing for function norm <- main.
-  Called from tests/float/nonlin.c:108.
-[eva:alarm] tests/float/nonlin.c:79: Warning: 
+  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:80: Warning: 
+[eva:alarm] tests/float/nonlin.c:82: Warning: 
   non-finite float value. assert \is_finite(v);
-[eva:nonlin] tests/float/nonlin.c:81: 
-  non-linear '(double)v1 * (double)v1', lv 'v1'
-[eva:nonlin] tests/float/nonlin.c:81: 
-  non-linear '(double)v2 * (double)v2', lv 'v2'
-[eva:nonlin] tests/float/nonlin.c:81: subdividing on v1
-[eva:nonlin] tests/float/nonlin.c:81: 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: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:109.
-[eva:alarm] tests/float/nonlin.c:87: 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:87: 
+[eva] tests/float/nonlin.c:98: 
   Assigning imprecise value to a_0.
-  The imprecision originates from Arithmetic {tests/float/nonlin.c:87}
-[eva:alarm] tests/float/nonlin.c:88: 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:88: 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:88: 
+[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:110.
+  Called from tests/float/nonlin.c:149.
 [eva] computing for function Frama_C_float_interval <- around_zeros <- main.
-  Called from tests/float/nonlin.c:97.
-[eva] tests/float/nonlin.c:97: 
+  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:97: 
+[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:101: non-linear '(f + f) - f', lv 'f'
-[eva:nonlin] tests/float/nonlin.c:101: 
-  non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
-[eva:nonlin] tests/float/nonlin.c:101: subdividing on f
-[eva:alarm] tests/float/nonlin.c:101: 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 ======
 [eva:final-states] Values at end of function access_bits:
   rbits1 ∈ {0; 1; 2}
-  x0 ∈ [0..3224938487]
+  x0 ∈ [0..3271884800]
   __retres ∈ {0; 1}
 [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.fffffe0000000p127 .. 0x1.fffffe0000000p127]
 [eva:final-states] Values at end of function garbled:
   a_0 ∈
      {{ garbled mix of &{x_0}
-      (origin: Arithmetic {tests/float/nonlin.c:87}) }}
+      (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 ∈ [--..--]
   a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
   b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
   c ∈ {0x1.c000000000000p2}
-  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
-  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
+  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]
-  square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  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.714fee0000000p1 .. 0x1.71c0040000000p1]
+  i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+  zf ∈ [-0x1.1300000000000p8 .. 0x1.1300000000000p8]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
-  r ∈ [3..11]
+  sq ∈ [-0x1.2718000000000p14 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.2950000000000p14]
+  r ∈ [2..11]
   x ∈ [1..42]
-  y ∈ {0; 1}
-  z ∈ [-171874..171874]
+  y ∈ [0..42]
+  z ∈ [-2750000..2750000]
   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]
+  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]
   b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
   c ∈ {0x1.c000000000000p2}
-  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
-  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.2000000000000p3]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c800000000000p2]
   d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
-  i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
+  i ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
   s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
-  zf ∈ [-0x1.12fffc0000000p4 .. 0x1.12fffc0000000p4]
+  zf ∈ [-0x1.1300000000000p8 .. 0x1.1300000000000p8]
   s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
-  sq ∈ [-0x1.b37e680000000p-7 .. 0x1.3b10000000000p14]
-  h ∈ [-0x1.38d8000000000p14 .. 0x1.3250680000000p-1]
-  r ∈ [3..11]
+  sq ∈ [-0x1.2718000000000p14 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.2950000000000p14]
+  r ∈ [2..11]
   x ∈ [1..42]
-  y ∈ {0; 1}
-  z ∈ [-171874..171874]
+  y ∈ [0..42]
+  z ∈ [-2750000..2750000]
   rbits1 ∈ {0; 1; 2}
   rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2f06c2710cf66d8592b8fdae363e0a41589b4481
--- /dev/null
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -0,0 +1,392 @@
+[kernel] Parsing tests/float/nonlin.c (with preprocessing)
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
+  Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  a ∈ {0}
+  b ∈ {0}
+  c ∈ {0}
+  r1 ∈ {0}
+  r2 ∈ {0}
+  d ∈ {0}
+  i ∈ {0}
+  s ∈ {0}
+  zf ∈ {0}
+  s2 ∈ {0}
+  sq ∈ {0}
+  h ∈ {0}
+  t[0] ∈ {1}
+   [1] ∈ {2}
+   [2] ∈ {3}
+   [3] ∈ {4}
+   [4] ∈ {5}
+   [5] ∈ {6}
+   [6] ∈ {7}
+   [7] ∈ {8}
+   [8] ∈ {9}
+   [9] ∈ {10}
+  r ∈ {0}
+  x ∈ {0}
+  y ∈ {0}
+  z ∈ {0}
+  rbits1 ∈ {0}
+  rbits2 ∈ {0}
+  v ∈ [--..--]
+  nondet ∈ [--..--]
+[eva] computing for function nonlin_f <- main.
+  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
+[eva] tests/float/nonlin.c:18: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:18: 
+  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 <- nonlin_f <- main.
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:19: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:24: non-linear 'a + b * (c - a)', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:24: subdividing on a
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:43: non-linear 'b * (c - a) + a', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:43: subdividing on a
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.4000000000000p2 .. 0x1.4800000000000p2],
+  {{ "r2" }},
+  [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.4800000000000p2 .. 0x1.5000000000000p2],
+  {{ "r2" }},
+  [0x1.4800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.5000000000000p2 .. 0x1.5800000000000p2],
+  {{ "r2" }},
+  [0x1.5000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.5800000000000p2 .. 0x1.6000000000000p2],
+  {{ "r2" }},
+  [0x1.5800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.6000000000000p2 .. 0x1.6800000000000p2],
+  {{ "r2" }},
+  [0x1.6000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.6800000000000p2 .. 0x1.7000000000000p2],
+  {{ "r2" }},
+  [0x1.6800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.7000000000000p2 .. 0x1.7800000000000p2],
+  {{ "r2" }},
+  [0x1.7000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.7800000000000p2 .. 0x1.8000000000000p2],
+  {{ "r2" }},
+  [0x1.7800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.8000000000000p2 .. 0x1.8800000000000p2],
+  {{ "r2" }},
+  [0x1.8000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.8800000000000p2 .. 0x1.9000000000000p2],
+  {{ "r2" }},
+  [0x1.8800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.9000000000000p2 .. 0x1.9800000000000p2],
+  {{ "r2" }},
+  [0x1.9000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.9800000000000p2 .. 0x1.a000000000000p2],
+  {{ "r2" }},
+  [0x1.9800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.a000000000000p2 .. 0x1.a800000000000p2],
+  {{ "r2" }},
+  [0x1.a000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.a800000000000p2 .. 0x1.b000000000000p2],
+  {{ "r2" }},
+  [0x1.a800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.b000000000000p2 .. 0x1.b800000000000p2],
+  {{ "r2" }},
+  [0x1.b000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.b800000000000p2 .. 0x1.c000000000000p2],
+  {{ "r2" }},
+  [0x1.b800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] Recording results for nonlin_f
+[eva] Done for function nonlin_f
+[eva] computing for function other <- main.
+  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: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:61: 
+  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 <- other <- main.
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:62: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:63: non-linear 'i * i', lv 'i'
+[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
+  accessing out of bounds index.
+  assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:65: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:66: non-linear 's + s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:66: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:67: non-linear 's * s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:67: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:68: non-linear 's * ((float)1 - s)', lv 's'
+[eva:nonlin] tests/float/nonlin.c:68: subdividing on s
+[eva] computing for function access_bits <- other <- main.
+  Called from tests/float/nonlin.c:69.
+[eva] Recording results for access_bits
+[eva] Done for function access_bits
+[eva] computing for function Frama_C_interval <- other <- main.
+  Called from tests/float/nonlin.c:71.
+[eva] using specification for function Frama_C_interval
+[eva] tests/float/nonlin.c:71: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:nonlin] tests/float/nonlin.c:72: non-linear '(1 / x) * x', lv 'x'
+[eva:nonlin] tests/float/nonlin.c:72: subdividing on x
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
+[eva] Recording results for other
+[eva] Done for function other
+[eva] computing for function split_alarm <- main.
+  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: 
+  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: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: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: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: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:98: 
+  Assigning imprecise value to a_0.
+  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:99: Warning: 
+  non-finite float value. assert \is_finite((float)(a_0 + a_0));
+[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:149.
+[eva] computing for function Frama_C_float_interval <- around_zeros <- main.
+  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: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: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: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 ======
+[eva:final-states] Values at end of function access_bits:
+  rbits1 ∈ {0; 1; 2}
+  x0 ∈ [0..3225911288]
+  __retres ∈ {0; 1}
+[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}
+[eva:final-states] Values at end of function garbled:
+  a_0 ∈
+     {{ garbled mix of &{x_0}
+      (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 ∈ [--..--]
+  a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+  b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
+  c ∈ {0x1.c000000000000p2}
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+[eva:final-states] Values at end of function norm:
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cde0000000p64 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  square ∈ [0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+  square2 ∈ [0x0.0000000000000p0 .. 0x1.fffffe0000000p127]
+[eva:final-states] Values at end of function other:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
+  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
+  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
+  x ∈ [1..42]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
+  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]
+[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 ∈ [0x0.0000000000000p0 .. 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]
+  b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
+  c ∈ {0x1.c000000000000p2}
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+  i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
+  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
+  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
+  x ∈ [1..42]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
+  rbits1 ∈ {0; 1; 2}
+  rbits2 ∈ {0; 1}
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a26018dc5a7b1e8f6e79c7f951bc2d4b1e746db0
--- /dev/null
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -0,0 +1,364 @@
+[kernel] Parsing tests/float/nonlin.c (with preprocessing)
+[kernel:parser:decimal-float] tests/float/nonlin.c:77: Warning: 
+  Floating-point constant 0.000000001 is not represented exactly. Will use 0x1.12e0be826d695p-30.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  a ∈ {0}
+  b ∈ {0}
+  c ∈ {0}
+  r1 ∈ {0}
+  r2 ∈ {0}
+  d ∈ {0}
+  i ∈ {0}
+  s ∈ {0}
+  zf ∈ {0}
+  s2 ∈ {0}
+  sq ∈ {0}
+  h ∈ {0}
+  t[0] ∈ {1}
+   [1] ∈ {2}
+   [2] ∈ {3}
+   [3] ∈ {4}
+   [4] ∈ {5}
+   [5] ∈ {6}
+   [6] ∈ {7}
+   [7] ∈ {8}
+   [8] ∈ {9}
+   [9] ∈ {10}
+  r ∈ {0}
+  x ∈ {0}
+  y ∈ {0}
+  z ∈ {0}
+  rbits1 ∈ {0}
+  rbits2 ∈ {0}
+  v ∈ [--..--]
+  nondet ∈ [--..--]
+[eva] computing for function nonlin_f <- main.
+  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
+[eva] tests/float/nonlin.c:18: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:18: 
+  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 <- nonlin_f <- main.
+  Called from tests/float/nonlin.c:19.
+[eva] tests/float/nonlin.c:19: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:19: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] tests/float/nonlin.c:22: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:24: non-linear 'a + b * (c - a)', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:24: subdividing on a
+[eva] tests/float/nonlin.c:26: assertion got status valid.
+[eva:nonlin] tests/float/nonlin.c:43: non-linear 'b * (c - a) + a', lv 'a'
+[eva:nonlin] tests/float/nonlin.c:43: subdividing on a
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.4000000000000p2 .. 0x1.4800000000000p2],
+  {{ "r2" }},
+  [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.4800000000000p2 .. 0x1.5000000000000p2],
+  {{ "r2" }},
+  [0x1.4800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.5000000000000p2 .. 0x1.5800000000000p2],
+  {{ "r2" }},
+  [0x1.5000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.5800000000000p2 .. 0x1.6000000000000p2],
+  {{ "r2" }},
+  [0x1.5800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.6000000000000p2 .. 0x1.6800000000000p2],
+  {{ "r2" }},
+  [0x1.6000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.6800000000000p2 .. 0x1.7000000000000p2],
+  {{ "r2" }},
+  [0x1.6800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.7000000000000p2 .. 0x1.7800000000000p2],
+  {{ "r2" }},
+  [0x1.7000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.7800000000000p2 .. 0x1.8000000000000p2],
+  {{ "r2" }},
+  [0x1.7800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.8000000000000p2 .. 0x1.8800000000000p2],
+  {{ "r2" }},
+  [0x1.8000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.8800000000000p2 .. 0x1.9000000000000p2],
+  {{ "r2" }},
+  [0x1.8800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.9000000000000p2 .. 0x1.9800000000000p2],
+  {{ "r2" }},
+  [0x1.9000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.9800000000000p2 .. 0x1.a000000000000p2],
+  {{ "r2" }},
+  [0x1.9800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.a000000000000p2 .. 0x1.a800000000000p2],
+  {{ "r2" }},
+  [0x1.a000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.a800000000000p2 .. 0x1.b000000000000p2],
+  {{ "r2" }},
+  [0x1.a800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.b000000000000p2 .. 0x1.b800000000000p2],
+  {{ "r2" }},
+  [0x1.b000000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] tests/float/nonlin.c:44: 
+  Frama_C_show_each_a_r2:
+  {{ "a" }},
+  [0x1.b800000000000p2 .. 0x1.c000000000000p2],
+  {{ "r2" }},
+  [0x1.b800000000000p2 .. 0x1.c0fffe0000000p2]
+[eva] Recording results for nonlin_f
+[eva] Done for function nonlin_f
+[eva] computing for function other <- main.
+  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: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:61: 
+  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 <- other <- main.
+  Called from tests/float/nonlin.c:62.
+[eva] tests/float/nonlin.c:62: 
+  function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] tests/float/nonlin.c:62: 
+  function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva:nonlin] tests/float/nonlin.c:63: non-linear 'i * i', lv 'i'
+[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
+[eva:alarm] tests/float/nonlin.c:63: Warning: 
+  accessing out of bounds index.
+  assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:65: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:66: non-linear 's + s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:66: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:67: non-linear 's * s', lv 's'
+[eva:nonlin] tests/float/nonlin.c:67: subdividing on s
+[eva:nonlin] tests/float/nonlin.c:68: non-linear 's * ((float)1 - s)', lv 's'
+[eva:nonlin] tests/float/nonlin.c:68: subdividing on s
+[eva] computing for function access_bits <- other <- main.
+  Called from tests/float/nonlin.c:69.
+[eva] Recording results for access_bits
+[eva] Done for function access_bits
+[eva] computing for function Frama_C_interval <- other <- main.
+  Called from tests/float/nonlin.c:71.
+[eva] using specification for function Frama_C_interval
+[eva] tests/float/nonlin.c:71: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:nonlin] tests/float/nonlin.c:72: non-linear '(1 / x) * x', lv 'x'
+[eva:nonlin] tests/float/nonlin.c:72: subdividing on x
+[eva:alarm] tests/float/nonlin.c:72: Warning: division by zero. assert x ≢ 0;
+[eva] Recording results for other
+[eva] Done for function other
+[eva] computing for function split_alarm <- main.
+  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: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:148.
+[eva] tests/float/nonlin.c:98: 
+  Assigning imprecise value to a_0.
+  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:149.
+[eva] computing for function Frama_C_float_interval <- around_zeros <- main.
+  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: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: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: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 ======
+[eva:final-states] Values at end of function access_bits:
+  rbits1 ∈ {0; 1; 2}
+  x0 ∈ [0..3225911288]
+  __retres ∈ {0; 1}
+[eva:final-states] Values at end of function around_zeros:
+  Frama_C_entropy_source ∈ [--..--]
+  f1 ∈ {0x1.0000000000000p-149}
+  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}
+      (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 ∈ [--..--]
+  a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+  b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
+  c ∈ {0x1.c000000000000p2}
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+[eva:final-states] Values at end of function norm:
+  Frama_C_entropy_source ∈ [--..--]
+  v1 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  v2 ∈ [-0x1.0f0cf00000000p73 .. 0x1.bc16d60000000p59]
+  square ∈ [0x0.0000000000000p0 .. inf] ∪ {NaN}
+  square2 ∈ [0x0.0000000000000p0 .. inf]
+[eva:final-states] Values at end of function other:
+  Frama_C_entropy_source ∈ [--..--]
+  i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
+  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
+  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
+  x ∈ [1..42]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
+  rbits1 ∈ {0; 1; 2}
+  rbits2 ∈ {0; 1}
+[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 ∈ [0x0.0000000000000p0 .. 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]
+  b ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p0]
+  c ∈ {0x1.c000000000000p2}
+  r1 ∈ [0x1.4000000000000p2 .. 0x1.cffffe0000000p2]
+  r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
+  d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
+  i ∈ [-0x1.8efff00000000p1 .. 0x1.8680000000000p1]
+  s ∈ [-0x1.0a00000000000p7 .. 0x1.1c00000000000p7]
+  zf ∈ [-0x1.1bfff80000000p4 .. 0x1.1bfff80000000p4]
+  s2 ∈ [-0x1.0a00000000000p8 .. 0x1.1c00000000000p8]
+  sq ∈ [0x0.0000000000000p0 .. 0x1.3b10000000000p14]
+  h ∈ [-0x1.38d8000000000p14 .. 0x1.f9dffc0000000p-2]
+  r ∈ {4; 5; 6; 7; 8; 9; 10; 11}
+  x ∈ [1..42]
+  y ∈ {0; 1}
+  z ∈ [-177499..177499]
+  rbits1 ∈ {0; 1; 2}
+  rbits2 ∈ {0; 1}
diff --git a/tests/misc/oracle/widen_hints_float.res.oracle b/tests/misc/oracle/widen_hints_float.res.oracle
index 087bdf14a4f43512c507d0c4b70676200187f5e3..45e531fdbc470f765c870b2955bad55c59c4f6e8 100644
--- a/tests/misc/oracle/widen_hints_float.res.oracle
+++ b/tests/misc/oracle/widen_hints_float.res.oracle
@@ -145,7 +145,7 @@
   Frama_C_entropy_source ∈ [--..--]
   f1 ∈ [-0. .. 71.]
   f2 ∈ [-80. .. 0.]
-  f3 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  f3 ∈ [-1.79769313486e+308 .. 10000000000.]
 [eva:final-states] Values at end of function trigo:
   Frama_C_entropy_source ∈ [--..--]
   f1 ∈ [-1. .. 1.]
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index 7395d9b0d4b5940e73762857645d559c76835fe9..1a05ef68d3147308ca183a5a8b6a18b65e876d76 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -54,11 +54,9 @@ void subdivide_several_variables () {
   int z = Frama_C_interval(-10, 10);
   /* A subdivision on each variable separately is more efficient here. */
   int norm = x * x + y * y;
-  /* Subdivide on x, then on y.
-     This evaluation is currently imprecise as the subdivision is stopped when
-     it seems not to improve the bounds of the result. Here however, the
-     subdivision on x would improve the value of x*x, and the subdivision on y
-     would then improve the value of the expression. */
+  /* Subdivide on x, then on y. Note that the subdivision on x does not improve
+     the result but only the value of x*x, while the later subdivision on y
+     improve the value of the result thanks to the reduced value of x*x. */
   int mult = ((x*x)*y)*y;
   /* A subdivision on both variables is more efficient here. */
   int zero = x * y - y * x;
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index ca1b870962dc9a89c3d58e9d29bea23a70cbdfec..de062d28c580191ea1a8cdb6de19c2f0ac49020a 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -24,7 +24,7 @@
        [31] ∈ {5}
        [32..35] ∈ {0}
 [eva] computing for function subdivide_integer <- main.
-  Called from tests/value/nonlin.c:121.
+  Called from tests/value/nonlin.c:119.
 [eva:nonlin] tests/value/nonlin.c:31: 
   non-linear '((int)z + 675) * ((int)z + 675)', lv 'z'
 [eva:nonlin] tests/value/nonlin.c:31: subdividing on z
@@ -45,7 +45,7 @@
 [eva] Recording results for subdivide_integer
 [eva] Done for function subdivide_integer
 [eva] computing for function subdivide_pointer <- main.
-  Called from tests/value/nonlin.c:122.
+  Called from tests/value/nonlin.c:120.
 [eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
   Called from tests/value/nonlin.c:12.
 [eva] using specification for function Frama_C_interval
@@ -68,7 +68,7 @@
 [eva] Recording results for subdivide_pointer
 [eva] Done for function subdivide_pointer
 [eva] computing for function subdivide_several_variables <- main.
-  Called from tests/value/nonlin.c:123.
+  Called from tests/value/nonlin.c:121.
 [eva] computing for function Frama_C_interval <- subdivide_several_variables <- 
                           main.
   Called from tests/value/nonlin.c:51.
@@ -97,61 +97,61 @@
 [eva:nonlin] tests/value/nonlin.c:56: non-linear 'y * y', lv 'y'
 [eva:nonlin] tests/value/nonlin.c:56: subdividing on x
 [eva:nonlin] tests/value/nonlin.c:56: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * x', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:62: non-linear '((x * x) * y) * y', lv 'y'
-[eva:nonlin] tests/value/nonlin.c:62: subdividing on x
-[eva:nonlin] tests/value/nonlin.c:62: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:64: non-linear 'x * y - y * x', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:64: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:67: 
+[eva:nonlin] tests/value/nonlin.c:60: non-linear 'x * x', lv 'x'
+[eva:nonlin] tests/value/nonlin.c:60: non-linear '((x * x) * y) * y', lv 'y'
+[eva:nonlin] tests/value/nonlin.c:60: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:60: subdividing on y
+[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * y - y * x', lv 'y, x'
+[eva:nonlin] tests/value/nonlin.c:62: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:65: 
   non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:67: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:68: 
+[eva:nonlin] tests/value/nonlin.c:65: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:66: 
   non-linear '(x * x + y * y) - (2 * x) * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:70: 
+[eva:nonlin] tests/value/nonlin.c:66: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:68: 
   non-linear '(z * x + x * y) + y * z', lv 'z, y, x'
-[eva:nonlin] tests/value/nonlin.c:70: non-linear 'w * w', lv 'w'
-[eva:nonlin] tests/value/nonlin.c:70: subdividing on x, y, z
-[eva:nonlin] tests/value/nonlin.c:70: subdividing on w
+[eva:nonlin] tests/value/nonlin.c:68: non-linear 'w * w', lv 'w'
+[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y, z
+[eva:nonlin] tests/value/nonlin.c:68: subdividing on w
 [eva] Recording results for subdivide_several_variables
 [eva] Done for function subdivide_several_variables
 [eva] computing for function subdivide_table <- main.
-  Called from tests/value/nonlin.c:124.
-[eva] tests/value/nonlin.c:89: loop invariant got status valid.
-[eva] tests/value/nonlin.c:90: starting to merge loop iterations
-[eva:nonlin] tests/value/nonlin.c:91: 
+  Called from tests/value/nonlin.c:122.
+[eva] tests/value/nonlin.c:87: loop invariant got status valid.
+[eva] tests/value/nonlin.c:88: starting to merge loop iterations
+[eva:nonlin] tests/value/nonlin.c:89: 
   non-linear '(4 + ((x >> 2) * 3 << 2)) + x % 4', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:91: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:89: subdividing on x
 [eva] Recording results for subdivide_table
 [eva] Done for function subdivide_table
 [eva] computing for function subdivide_reduced_value <- main.
-  Called from tests/value/nonlin.c:125.
-[eva:nonlin] tests/value/nonlin.c:103: non-linear 't1[i] - t2[i]', lv 'i'
-[eva:nonlin] tests/value/nonlin.c:103: subdividing on i
-[eva:alarm] tests/value/nonlin.c:103: Warning: 
+  Called from tests/value/nonlin.c:123.
+[eva:nonlin] tests/value/nonlin.c:101: non-linear 't1[i] - t2[i]', lv 'i'
+[eva:nonlin] tests/value/nonlin.c:101: subdividing on i
+[eva:alarm] tests/value/nonlin.c:101: Warning: 
   accessing out of bounds index. assert 0 ≤ i;
-[eva:alarm] tests/value/nonlin.c:103: Warning: 
+[eva:alarm] tests/value/nonlin.c:101: Warning: 
   accessing out of bounds index. assert i < 2;
 [eva] Recording results for subdivide_reduced_value
 [eva] Done for function subdivide_reduced_value
 [eva] computing for function local_subdivide <- main.
-  Called from tests/value/nonlin.c:126.
+  Called from tests/value/nonlin.c:124.
 [eva] computing for function Frama_C_interval <- local_subdivide <- main.
-  Called from tests/value/nonlin.c:109.
-[eva] tests/value/nonlin.c:109: 
+  Called from tests/value/nonlin.c:107.
+[eva] tests/value/nonlin.c:107: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- local_subdivide <- main.
-  Called from tests/value/nonlin.c:110.
-[eva] tests/value/nonlin.c:110: 
+  Called from tests/value/nonlin.c:108.
+[eva] tests/value/nonlin.c:108: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:nonlin] tests/value/nonlin.c:114: 
+[eva:nonlin] tests/value/nonlin.c:112: 
   non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:114: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:112: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:113: subdividing on x, y
 [eva:nonlin] tests/value/nonlin.c:115: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:117: subdividing on x, y
 [eva] Recording results for local_subdivide
 [eva] Done for function local_subdivide
 [eva] Recording results for main
@@ -198,7 +198,7 @@
   y ∈ [-10..10]
   z ∈ [-10..10]
   norm ∈ [0..200]
-  mult ∈ [-10000..10000]
+  mult ∈ [0..10000]
   zero ∈ [-26..26]
   square ∈ [-48..400]
   square2 ∈ [-48..400]