diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 676dc9b6fa4483a8132c3939540f520efd3df9dc..18f57b5196e274749cb4cec156755ad5906757ce 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -20,3 +20,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module List = struct
+
+  let concat_map f l =
+    let rec aux f acc = function
+      | [] -> List.rev acc
+      | x :: l ->
+        let xs = f x in
+        aux f (List.rev_append xs acc) l
+    in aux f [] l
+
+end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 415b987eba7c80bb120dcf25dc0d9a1687ade500..e838d35296fbf19e045a2dc483b9c57594bc22c1 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -32,3 +32,8 @@
 *)
 
 (** {1 OCaml} *)
+
+module List: sig
+  (** since 4.10.0 *)
+  val concat_map: ('a -> 'b list) -> 'a list -> 'b list
+end
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 686e7ab24143eb3e8109230b809c2b36ef7955b8..f44c2e4c112623521a6b4404f2c007e29b3e91b0 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -87,10 +87,17 @@ module Eva_annotations: sig
     | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
     | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
 
+  type split_kind = Static | Dynamic
+  type split_term =
+    | Expression of Cil_types.exp
+    | Predicate of Cil_types.predicate
+
   (** Split/merge annotations for value partitioning.  *)
   type flow_annotation =
-    | FlowSplit of Cil_types.term (** Split states according to a term. *)
-    | FlowMerge of Cil_types.term (** Merge states separated by a previous split. *)
+    | FlowSplit of split_term * split_kind
+    (** Split states according to a term. *)
+    | FlowMerge of split_term
+    (** Merge states separated by a previous split. *)
 
   val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
     Cil_types.stmt -> slevel_annotation -> unit
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index a7138c912d6edcd7e3316299c63486fc1e5ee5aa..4af621c4009d47b7ce15aa6d9947d4cdb4cf5fbb 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -53,7 +53,25 @@ let new_rationing ~limit ~merge = { current = ref 0; limit; merge }
 
 (* --- Keys --- *)
 
-module ExpMap = Cil_datatype.ExpStructEq.Map
+type split_term = Eva_annotations.split_term =
+  | Expression of Cil_types.exp
+  | Predicate of Cil_types.predicate
+
+module SplitTerm = struct
+  type t = split_term
+  let compare x y =
+    match x, y with
+    | Expression e1, Expression e2 -> Cil_datatype.ExpStructEq.compare e1 e2
+    | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
+    | Expression _, Predicate _ -> 1
+    | Predicate _, Expression _ -> -1
+
+  let pretty fmt = function
+    | Expression e -> Printer.pp_exp fmt e
+    | Predicate p -> Printer.pp_predicate fmt p
+end
+
+module SplitMap = Map.Make (SplitTerm)
 module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
 module LoopList = Datatype.List (IntPair)
 module BranchList = Datatype.List (Datatype.Int)
@@ -75,18 +93,19 @@ type branch = int
      (innermost loop first) It also stores the maximum number of unrolling ;
      this number varies from a state to another, as it is computed from
      an expression evaluated when we enter the loop.
-   - Static/Dynamic splits: track the splits applied to the state as a map
-     from the expression of the split to the value of this expression. Since
-     the split creates states in which the expression evalutates to a
+   - Splits: track the splits applied to the state as a map from the term of
+     the split to its value. Terms can be C expresssions or ACSL predicates.
+     Since the split creates states in which the expression evalutates to a
      singleton, the values of the map are integers.
      Static splits are only evaluated when the annotation is encountered
-     whereas dynamic splits are reevaluated regularly. *)
+     whereas dynamic splits are reevaluated regularly; a list of active
+     dynamic splits is also propagated in the key. *)
 type key = {
   ration_stamp : stamp;
   branches : branch list;
   loops : (int * int) list; (* current iteration / max unrolling *)
-  static_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
-  dynamic_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
+  splits : Integer.t SplitMap.t; (* term -> value *)
+  dynamic_splits : split_monitor SplitMap.t; (* term -> monitor *)
 }
 
 module Key =
@@ -98,21 +117,18 @@ struct
     ration_stamp = None;
     branches = [];
     loops = [];
-    static_split = ExpMap.empty;
-    dynamic_split = ExpMap.empty;
+    splits = SplitMap.empty;
+    dynamic_splits = SplitMap.empty;
   }
 
   let compare k1 k2 =
     let (<?>) c (cmp,x,y) =
       if c = 0 then cmp x y else c
     in
-    let compare_split (i1,_m1) (i2,_m2) =
-      Integer.compare i1 i2
-    in
     Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
     <?> (LoopList.compare, k1.loops, k2.loops)
-    <?> (ExpMap.compare compare_split, k1.static_split, k2.static_split)
-    <?> (ExpMap.compare compare_split, k1.dynamic_split, k2.dynamic_split)
+    <?> (SplitMap.compare Integer.compare, k1.splits, k2.splits)
+    <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
     <?> (BranchList.compare, k1.branches, k2.branches)
 
   let pretty fmt key =
@@ -129,11 +145,11 @@ struct
       fmt
       key.loops;
     Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
-      (fun fmt (e,(i,_m)) -> Format.fprintf fmt "%a:%a"
-          Cil_printer.pp_exp e
+      (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
+          SplitTerm.pretty t
           (Integer.pretty ~hexa:false) i)
       fmt
-      (ExpMap.bindings key.static_split @ ExpMap.bindings key.dynamic_split)
+      (SplitMap.bindings key.splits)
 
   let exceed_rationing key = key.ration_stamp = None
 end
@@ -166,7 +182,7 @@ type unroll_limit =
   | IntLimit of int
   | AutoUnroll of Cil_types.stmt * int * int
 
-type split_kind = Static | Dynamic
+type split_kind = Eva_annotations.split_kind = Static | Dynamic
 
 type action =
   | Enter_loop of unroll_limit
@@ -175,8 +191,8 @@ type action =
   | Branch of branch * int
   | Ration of rationing
   | Restrict of Cil_types.exp * Integer.t list
-  | Split of Cil_types.exp * split_kind * split_monitor
-  | Merge of Cil_types.exp * split_kind
+  | Split of split_term * split_kind * split_monitor
+  | Merge of split_term
   | Update_dynamic_splits
 
 exception InvalidAction
@@ -328,6 +344,26 @@ struct
     | Failure _ ->
       fail ~exp "this partitioning parameter is too big"
 
+  let split_by_predicate state predicate =
+    let env =
+      let states = function _ -> Abstract.Dom.top in
+      Abstract_domain.{ states; result = None }
+    in
+    let source = fst (predicate.Cil_types.pred_loc) in
+    let aux positive =
+      Abstract.Dom.reduce_by_predicate env state predicate positive
+      >>-: fun state' ->
+      let x = Abstract.Dom.evaluate_predicate env state' predicate in
+      if x == Unknown
+      then
+        Value_parameters.warning ~source ~once:true
+          "failing to learn perfectly from split predicate";
+      if Abstract.Dom.equal state' state then raise Operation_failed;
+      let value = if positive then Integer.one else Integer.zero in
+      value, state'
+    in
+    Bottom.all [ aux true; aux false ]
+
   (* --- Applying partitioning actions onto flows --------------------------- *)
 
   let stamp_by_value = match Abstract.Val.get Main_values.CVal.key with
@@ -352,42 +388,42 @@ struct
             None
           end
 
-  let split_state ~monitor (kind : split_kind) (exp : Cil_types.exp)
-      (key : key) (state : state) : (key * state) list =
+  let split_state ~monitor term (key, state) : (key * state) list =
     try
-      let add value map = ExpMap.add exp (value, monitor) map in
-      let update_key (v,x) =
-        let k =
-          match kind with
-          | Static -> { key with static_split = add v key.static_split }
-          | Dynamic -> { key with dynamic_split = add v key.dynamic_split }
-        in
-        (k,x)
+      let update_key (v, x) =
+        { key with splits = SplitMap.add term v key.splits }, x
       in
-      List.map update_key (split_by_value ~monitor state exp)
-    with Operation_failed ->
-      [(key,state)]
-
-  let split ~monitor (kind : split_kind) (exp : Cil_types.exp) (p : t) =
-    let add_split acc (key,state) =
-      split_state ~monitor kind exp key state @ acc
+      let states =
+        match term with
+        | Expression exp -> split_by_value ~monitor state exp
+        | Predicate pred -> split_by_predicate state pred
+      in
+      List.map update_key states
+    with Operation_failed -> [(key,state)]
+
+  let split ~monitor (kind : split_kind) (term : split_term) (p : t) =
+    let add_split (key, state) =
+      let dynamic_splits =
+        match kind with
+        | Static -> SplitMap.remove term key.dynamic_splits
+        | Dynamic -> SplitMap.add term monitor key.dynamic_splits
+      in
+      let key = { key with dynamic_splits } in
+      split_state ~monitor term (key, state)
     in
-    List.fold_left add_split [] p
+    Transitioning.List.concat_map add_split p
 
   let update_dynamic_splits p =
     (* Update one state *)
-    let update_state acc (key,state) =
+    let update_state (key, state) =
       (* Split the states in the list l for the given exp *)
-      let update_exp exp (_i,monitor) l =
-        let resplit acc (k,x) =
-          split_state ~monitor Dynamic exp k x @ acc
-        in
-        List.fold_left resplit [] l
+      let update_exp term monitor l =
+        Transitioning.List.concat_map (split_state ~monitor term) l
       in
       (* Foreach exp in original state: split *)
-      ExpMap.fold update_exp key.dynamic_split [(key,state)] @ acc
+      SplitMap.fold update_exp key.dynamic_splits [(key,state)]
     in
-    List.fold_left update_state [] p
+    Transitioning.List.concat_map update_state p
 
   let map_keys (f : key -> state -> key) (p : t) : t =
     List.map (fun (k,x) -> f k x, x) p
@@ -471,11 +507,9 @@ struct
         | Restrict (expr, expected_values) -> fun k s ->
           { k with ration_stamp = stamp_by_value expr expected_values s}
 
-        | Merge (exp, Static) -> fun k _x ->
-          { k with static_split = ExpMap.remove exp k.static_split }
-
-        | Merge (exp, Dynamic) -> fun k _x ->
-          { k with dynamic_split = ExpMap.remove exp k.dynamic_split }
+        | Merge term -> fun k _x ->
+          { k with splits = SplitMap.remove term k.splits;
+                   dynamic_splits = SplitMap.remove term k.dynamic_splits }
       in
       map_keys transfer p
 
diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli
index a5a3a569b37aa90168a42418279e6918552c9450..fe3dc9f303f8332f8009fdf419dc10f6676509c1 100644
--- a/src/plugins/value/partitioning/partition.mli
+++ b/src/plugins/value/partitioning/partition.mli
@@ -92,7 +92,12 @@ type unroll_limit =
       split point, and the key is then kept unchanged until a merge.
     - dynamic splits are regularly redone: the expression is re-evaluated, and
       states are then split or merged accordingly. *)
-type split_kind = Static | Dynamic
+type split_kind = Eva_annotations.split_kind = Static | Dynamic
+
+(** Splits can be performed according to a C expression or an ACSL predicate. *)
+type split_term = Eva_annotations.split_term =
+  | Expression of Cil_types.exp
+  | Predicate of Cil_types.predicate
 
 (** Split monitor: prevents splits from generating too many states. *)
 type split_monitor
@@ -137,7 +142,7 @@ type action =
       – all other states are joined together.
       Previous rationing is erased and replaced by this new stamping.
       Implementation of the option -eva-split-return. *)
-  | Split of Cil_types.exp * split_kind * split_monitor
+  | Split of split_term * split_kind * split_monitor
   (** [Split (exp, kind, monitor)] tries to separate states such as the [exp]
       evaluates to a singleton value in each state in the flow. If necessary and
       possible, splits states into multiple states. States in which the [exp]
@@ -145,7 +150,7 @@ type action =
       if [exp] evaluates to more than [limit] values, [limit] being the split
       limit of the [monitor]. A same monitor can be used for successive splits
       on different flows. *)
-  | Merge of Cil_types.exp * split_kind
+  | Merge of split_term
   (** Forgets the split of an expression: states that were kept separate only
       by the split of this expression will be joined together. *)
   | Update_dynamic_splits
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index d77a88990c76c64b530c0617eff3e2b26d58fef8..519e2fc02290aabc32213050079494afe4a23073 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -116,7 +116,8 @@ struct
       try
         let vi = Globals.Vars.find_from_astinfo name VGlobal in
         let monitor = Partition.new_monitor ~split_limit in
-        Partition.Split (Cil.evar vi, Partition.Dynamic, monitor) :: l
+        let expr = Partition.Expression (Cil.evar vi) in
+        Partition.Split (expr, Partition.Dynamic, monitor) :: l
       with Not_found ->
         warn ~current:false "cannot find the global variable %s for value \
                              partitioning; ignoring" name;
@@ -125,14 +126,13 @@ struct
     ValuePartitioning.fold add []
 
   let flow_actions stmt =
-    let kind = Partition.Static in
     let map_annot acc t =
       try
         let monitor = Partition.new_monitor ~split_limit in
         let action =
           match t with
-          | FlowSplit t -> Partition.Split (term_to_exp t, kind, monitor)
-          | FlowMerge t -> Partition.Merge (term_to_exp t, kind)
+          | FlowSplit (t, kind) -> Partition.Split (t, kind, monitor)
+          | FlowMerge t -> Partition.Merge t
         in
         action :: acc
       with
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 9cbcd7d3f9d2813ca42019e4c764488b0dfd55fb..8aaefcaecca96a0f90540696ca4defd6a4d44378 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -33,9 +33,14 @@ type unroll_annotation =
   | UnrollAmount of Cil_types.term
   | UnrollFull
 
+type split_kind = Static | Dynamic
+type split_term =
+  | Expression of Cil_types.exp
+  | Predicate of Cil_types.predicate
+
 type flow_annotation =
-  | FlowSplit of term
-  | FlowMerge of term
+  | FlowSplit of split_term * split_kind
+  | FlowMerge of split_term
 
 type taint_annotation = Cil_types.term list
 
@@ -153,26 +158,6 @@ module Slevel = Register (struct
       | SlevelFull -> Format.pp_print_string fmt "full"
   end)
 
-module SimpleTermAnnotation =
-struct
-  type t = term
-
-  let parse ~typing_context = function
-    | [t] ->
-      let open Logic_typing in
-      typing_context.type_term typing_context typing_context.pre_state t
-    | _ -> raise Parse_error
-
-  let export t =
-    Ext_terms [t]
-
-  let import = function
-    | Ext_terms [t] -> t
-    | _ -> assert false
-
-  let print = Printer.pp_term
-end
-
 module ListTermAnnotation =
 struct
   type t = term list
@@ -220,18 +205,67 @@ module Unroll = Register (struct
       | UnrollAmount t -> Printer.pp_term fmt t
   end)
 
+module SplitTermAnnotation =
+struct
+  (* [split_term] plus the original term before conversion to a C expression,
+     when possible, to avoid changes due to its reconversion to a C term. *)
+  type t = split_term * Cil_types.term option
+
+  let term_to_exp = !Db.Properties.Interp.term_to_exp ~result:None
+
+  let parse ~typing_context:context = function
+    | [t] ->
+      begin
+        let open Logic_typing in
+        let exception No_term in
+        try
+          let error _loc _fmt = raise No_term in
+          let context = { context with error } in
+          let term = context.type_term context context.pre_state t in
+          Expression (term_to_exp term), Some term
+        with
+        | No_term ->
+          Predicate (context.type_predicate context context.pre_state t), None
+        | Db.Properties.Interp.No_conversion ->
+          Kernel.warning ~wkey:Kernel.wkey_annot_error ~once:true ~current:true
+            "split/merge expressions must be valid expressions; ignoring";
+          raise Parse_error
+      end
+    | _ -> raise Parse_error
+
+  let export = function
+    | Expression _, Some term -> Ext_terms [ term ]
+    | Expression expr, None -> Ext_terms [ Logic_utils.expr_to_term expr ]
+    | Predicate pred, _ -> Ext_preds [pred]
+
+  let import = function
+    | Ext_terms [term] -> Expression (term_to_exp term), Some term
+    | Ext_preds [pred] -> Predicate pred, None
+    | _ -> assert false
+
+  let print fmt = function
+    | Expression expr, _ -> Printer.pp_exp fmt expr
+    | Predicate pred, _ -> Printer.pp_predicate fmt pred
+end
+
 module Split = Register (struct
-    include SimpleTermAnnotation
+    include SplitTermAnnotation
     let name = "split"
     let is_loop_annot = false
   end)
 
 module Merge = Register (struct
-    include SimpleTermAnnotation
+    include SplitTermAnnotation
     let name = "merge"
     let is_loop_annot = false
   end)
 
+module DynamicSplit = Register (struct
+    include SplitTermAnnotation
+    let name = "dynamic_split"
+    let is_loop_annot = false
+  end)
+
 module Taint = Register (struct
     include ListTermAnnotation
     let name = "taint"
@@ -248,17 +282,23 @@ let get_slevel_annot stmt =
 let get_unroll_annot stmt = Unroll.get stmt
 
 let get_flow_annot stmt =
-  List.map (fun a -> FlowSplit a) (Split.get stmt) @
-  List.map (fun a -> FlowMerge a) (Merge.get stmt)
+  List.map (fun (a, _) -> FlowSplit (a, Static)) (Split.get stmt) @
+  List.map (fun (a, _) -> FlowSplit (a, Dynamic)) (DynamicSplit.get stmt) @
+  List.map (fun (a, _) -> FlowMerge a) (Merge.get stmt)
 
 
 let add_slevel_annot = Slevel.add
 
 let add_unroll_annot = Unroll.add
 
-let add_flow_annot ~emitter ~loc stmt = function
-  | FlowSplit annot -> Split.add ~emitter ~loc stmt annot
-  | FlowMerge annot -> Merge.add ~emitter ~loc stmt annot
+let add_flow_annot ~emitter ~loc stmt flow_annotation =
+  let f, annot =
+    match flow_annotation with
+    | FlowSplit (annot, Static) -> Split.add, annot
+    | FlowSplit (annot, Dynamic) -> DynamicSplit.add, annot
+    | FlowMerge annot -> Merge.add, annot
+  in
+  f ~emitter ~loc stmt (annot, None)
 
 
 module Subdivision = Register (struct
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 2299ead597d043d37a436f870f2958c88decd946..dd7d580bdb463911ea778c79cce32184008d0859 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -38,9 +38,15 @@ type unroll_annotation =
   | UnrollAmount of Cil_types.term
   | UnrollFull
 
+type split_kind = Static | Dynamic
+
+type split_term =
+  | Expression of Cil_types.exp
+  | Predicate of Cil_types.predicate
+
 type flow_annotation =
-  | FlowSplit of Cil_types.term
-  | FlowMerge of Cil_types.term
+  | FlowSplit of split_term * split_kind
+  | FlowMerge of split_term
 
 type taint_annotation = Cil_types.term list
 
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index f6e785c3e31abc712bb1928fe1560f418cd4180e..4bf575a86cd583e6667c60fe93145adcf4430756 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -1,10 +1,18 @@
 [kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_unroll
+[eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  k ∈ {0}
   nondet ∈ [--..--]
+  k ∈ {0}
+[eva] computing for function test_slevel <- main.
+  Called from tests/value/partitioning-annots.c:205.
+[eva] tests/value/partitioning-annots.c:170: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:175: starting to merge loop iterations
+[eva] Recording results for test_slevel
+[eva] Done for function test_slevel
+[eva] computing for function test_unroll <- main.
+  Called from tests/value/partitioning-annots.c:206.
 [eva:loop-unroll] tests/value/partitioning-annots.c:26: 
   loop not completely unrolled
 [eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations
@@ -19,8 +27,98 @@
   loop not completely unrolled
 [eva] tests/value/partitioning-annots.c:54: starting to merge loop iterations
 [eva] Recording results for test_unroll
-[eva] done for function test_unroll
+[eva] Done for function test_unroll
+[eva] computing for function test_split <- main.
+  Called from tests/value/partitioning-annots.c:207.
+[eva] computing for function Frama_C_interval <- test_split <- main.
+  Called from tests/value/partitioning-annots.c:73.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:73: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_split <- main.
+  Called from tests/value/partitioning-annots.c:74.
+[eva] tests/value/partitioning-annots.c:74: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:80: 
+  Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:83: 
+  Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:83: 
+  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:85: 
+  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
+[eva] tests/value/partitioning-annots.c:89: 
+  Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
+[eva] Recording results for test_split
+[eva] Done for function test_split
+[eva] computing for function test_dynamic_split <- main.
+  Called from tests/value/partitioning-annots.c:208.
+[eva] tests/value/partitioning-annots.c:95: Warning: 
+  this partitioning parameter cannot be evaluated safely on all states
+[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
+  Called from tests/value/partitioning-annots.c:97.
+[eva] tests/value/partitioning-annots.c:97: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:100: 
+  Frama_C_show_each_split_with_uninit: {2}, {2}
+[eva] tests/value/partitioning-annots.c:100: 
+  Frama_C_show_each_split_with_uninit: {1}, {1}
+[eva] tests/value/partitioning-annots.c:100: 
+  Frama_C_show_each_split_with_uninit: {0}, {0}
+[eva] tests/value/partitioning-annots.c:100: 
+  Frama_C_show_each_split_with_uninit: Bottom, Bottom
+[eva] tests/value/partitioning-annots.c:102: 
+  Frama_C_show_each_no_split: {0}, {0; 1; 2}
+[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
+  Called from tests/value/partitioning-annots.c:103.
+[eva] tests/value/partitioning-annots.c:103: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {2}
+[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {1}
+[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {0}
+[eva] tests/value/partitioning-annots.c:109: 
+  Frama_C_show_each_no_split: {0}, {0; 1; 2}
+[eva] Recording results for test_dynamic_split
+[eva] Done for function test_dynamic_split
+[eva] Recording results for main
+[eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_dynamic_split:
+  Frama_C_entropy_source ∈ [--..--]
+  a ∈ {0}
+  b ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_slevel:
+  a[0..9] ∈ {42}
+  b[0..9] ∈ {42} or UNINITIALIZED
+  c[0..3] ∈ {33; 42}
+   [4..9] ∈ {33; 42} or UNINITIALIZED
+  d[0..9] ∈ {33; 42}
+  e[0..3] ∈ {33; 42}
+[eva:final-states] Values at end of function test_split:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ {0; 1}
+  i ∈ {0; 1}
+  j ∈ {0; 1; 2}
 [eva:final-states] Values at end of function test_unroll:
   a[0..9] ∈ {42}
   b[0..9] ∈ {42}
@@ -46,15 +144,57 @@
    [7] ∈ {36}
    [8] ∈ {9}
    [9] ∈ {1}
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  k ∈ {0; 1}
+[from] Computing for function test_dynamic_split
+[from] Computing for function Frama_C_interval <-test_dynamic_split
+[from] Done for function Frama_C_interval
+[from] Done for function test_dynamic_split
+[from] Computing for function test_slevel
+[from] Done for function test_slevel
+[from] Computing for function test_split
+[from] Done for function test_split
 [from] Computing for function test_unroll
 [from] Done for function test_unroll
+[from] Computing for function main
+[from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; min; max
+[from] Function test_dynamic_split:
+  Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
+[from] Function test_slevel:
+  NO EFFECTS
+[from] Function test_split:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  k FROM Frama_C_entropy_source
 [from] Function test_unroll:
   NO EFFECTS
+[from] Function main:
+  Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
+  k FROM Frama_C_entropy_source
 [from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_dynamic_split:
+    Frama_C_entropy_source; a; b
+[inout] Inputs for function test_dynamic_split:
+    Frama_C_entropy_source; nondet
+[inout] Out (internal) for function test_slevel:
+    a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
+[inout] Inputs for function test_slevel:
+    nondet
+[inout] Out (internal) for function test_split:
+    Frama_C_entropy_source; k; i; j
+[inout] Inputs for function test_split:
+    Frama_C_entropy_source; k
 [inout] Out (internal) for function test_unroll:
     a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1; 
     i_2; i_3; j_1
 [inout] Inputs for function test_unroll:
     \nothing
+[inout] Out (internal) for function main:
+    Frama_C_entropy_source; k
+[inout] Inputs for function main:
+    Frama_C_entropy_source; nondet; k
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index 3a489cae4e139ed96a227bc728636827a423aff7..10704f7b9a550d3d2fa4c500be708b4ec8206f79 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -3,8 +3,8 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  k ∈ {0}
   nondet ∈ [--..--]
+  k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_split.
   Called from tests/value/partitioning-annots.c:73.
 [eva] using specification for function Frama_C_interval
@@ -35,13 +35,21 @@
 [eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_before_first_merge: {0}, {0}, {0}
 [eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
+  Frama_C_show_each_before_second_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {1}, {1}, {1}
 [eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
+  Frama_C_show_each_before_second_merge: {1}, {0}, {1}
 [eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
+  Frama_C_show_each_before_second_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:87: 
+  Frama_C_show_each_before_second_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:89: 
+  Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
 [eva] tests/value/partitioning-annots.c:89: 
-  Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
+  Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
 [eva] Recording results for test_split
 [eva] done for function test_split
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index 64a0b52e080ccb1be2263ff9f2a956d0722b9641..da1dee03a864d7ec4bfbbfcafaa36a21158a914f 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -1,77 +1,68 @@
 [kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_split
+[eva] Analyzing a complete application starting at test_loop_split
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  k ∈ {0}
   nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_split.
-  Called from tests/value/partitioning-annots.c:73.
+  k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:73: 
+[eva] tests/value/partitioning-annots.c:127: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_split.
-  Called from tests/value/partitioning-annots.c:74.
-[eva] tests/value/partitioning-annots.c:74: 
-  function Frama_C_interval: precondition 'order' got status valid.
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:125: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:80: 
-  Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:83: 
-  Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:85: 
-  Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:87: 
-  Frama_C_show_each_before_second_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:89: 
-  Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:89: 
-  Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
-[eva] Recording results for test_split
-[eva] done for function test_split
+[eva:alarm] tests/value/partitioning-annots.c:134: Warning: 
+  accessing uninitialized left-value. assert \initialized(&A[i]);
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {0}, {42}
+[eva] tests/value/partitioning-annots.c:140: assertion got status valid.
+[eva] tests/value/partitioning-annots.c:143: 
+  Frama_C_show_each: {{ "Value 42 not found" }}
+[eva] Recording results for test_loop_split
+[eva] done for function test_loop_split
 [eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_split:
+[eva:final-states] Values at end of function test_loop_split:
   Frama_C_entropy_source ∈ [--..--]
-  k ∈ {0; 1}
-  i ∈ {0; 1}
-  j ∈ {0; 1; 2}
-[from] Computing for function test_split
-[from] Computing for function Frama_C_interval <-test_split
+  A[0] ∈ [0..100]
+   [1..9] ∈ [0..100] or UNINITIALIZED
+  i ∈ [0..10]
+[from] Computing for function test_loop_split
+[from] Computing for function Frama_C_interval <-test_loop_split
 [from] Done for function Frama_C_interval
-[from] Done for function test_split
+[from] Done for function test_loop_split
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function Frama_C_interval:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   \result FROM Frama_C_entropy_source; min; max
-[from] Function test_split:
+[from] Function test_loop_split:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-  k FROM Frama_C_entropy_source
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_split:
-    Frama_C_entropy_source; k; i; j
-[inout] Inputs for function test_split:
-    Frama_C_entropy_source; k
+[inout] Out (internal) for function test_loop_split:
+    Frama_C_entropy_source; A[0..9]; i
+[inout] Inputs for function test_loop_split:
+    Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 0726db35992e2719e1cf18e08112b16089225dbc..eeb698d400e482bf2fb9c492d5f74fe2fb0b81fd 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -1,68 +1,40 @@
 [kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_loop_split
+[eva] Analyzing a complete application starting at test_history
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  k ∈ {0}
   nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
+  k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_history.
+  Called from tests/value/partitioning-annots.c:149.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:107: 
+[eva] tests/value/partitioning-annots.c:149: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:105: starting to merge loop iterations
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:107.
-[eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/partitioning-annots.c:114: Warning: 
-  accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {9}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {8}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:120: assertion got status valid.
-[eva] tests/value/partitioning-annots.c:123: 
-  Frama_C_show_each: {{ "Value 42 not found" }}
-[eva] Recording results for test_loop_split
-[eva] done for function test_loop_split
+[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] tests/value/partitioning-annots.c:158: Warning: 
+  division by zero. assert j ≢ 0;
+[eva] Recording results for test_history
+[eva] done for function test_history
 [eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_loop_split:
+[eva:final-states] Values at end of function test_history:
   Frama_C_entropy_source ∈ [--..--]
-  A[0] ∈ [0..100]
-   [1..9] ∈ [0..100] or UNINITIALIZED
-  i ∈ [0..10]
-[from] Computing for function test_loop_split
-[from] Computing for function Frama_C_interval <-test_loop_split
+  i ∈ {0; 1}
+  j ∈ {0; 1}
+  k_0 ∈ {1}
+[from] Computing for function test_history
+[from] Computing for function Frama_C_interval <-test_history
 [from] Done for function Frama_C_interval
-[from] Done for function test_loop_split
+[from] Done for function test_history
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
 [from] Function Frama_C_interval:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   \result FROM Frama_C_entropy_source; min; max
-[from] Function test_loop_split:
+[from] Function test_history:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_loop_split:
-    Frama_C_entropy_source; A[0..9]; i
-[inout] Inputs for function test_loop_split:
+[inout] Out (internal) for function test_history:
+    Frama_C_entropy_source; i; j; k_0
+[inout] Inputs for function test_history:
     Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index 95b65614d116d230e504958ec3342e0fabfeb3db..1718f8213307143be4ea8df27c930e7540c14ba9 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -3,17 +3,16 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  k ∈ {0}
   nondet ∈ [--..--]
+  k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from tests/value/partitioning-annots.c:129.
+  Called from tests/value/partitioning-annots.c:149.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:129: 
+[eva] tests/value/partitioning-annots.c:149: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] tests/value/partitioning-annots.c:138: Warning: 
-  division by zero. assert j ≢ 0;
+[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {0}, {0}
+[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {1}, {1}
 [eva] Recording results for test_history
 [eva] done for function test_history
 [eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
deleted file mode 100644
index e2009fcbb60b0627e86a3d9db8d7ee5cd946709e..0000000000000000000000000000000000000000
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ /dev/null
@@ -1,39 +0,0 @@
-[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_history
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  k ∈ {0}
-  nondet ∈ [--..--]
-[eva] computing for function Frama_C_interval <- test_history.
-  Called from tests/value/partitioning-annots.c:129.
-[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:129: 
-  function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0}, {0}
-[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {1}, {1}
-[eva] Recording results for test_history
-[eva] done for function test_history
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_history:
-  Frama_C_entropy_source ∈ [--..--]
-  i ∈ {0; 1}
-  j ∈ {0; 1}
-  k_0 ∈ {1}
-[from] Computing for function test_history
-[from] Computing for function Frama_C_interval <-test_history
-[from] Done for function Frama_C_interval
-[from] Done for function test_history
-[from] ====== DEPENDENCIES COMPUTED ======
-  These dependencies hold at termination for the executions that terminate:
-[from] Function Frama_C_interval:
-  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-  \result FROM Frama_C_entropy_source; min; max
-[from] Function test_history:
-  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_history:
-    Frama_C_entropy_source; i; j; k_0
-[inout] Inputs for function test_history:
-    Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.6.res.oracle b/tests/value/oracle/partitioning-annots.6.res.oracle
deleted file mode 100644
index 405717c890d17bf711d9670096fd4680318c231e..0000000000000000000000000000000000000000
--- a/tests/value/oracle/partitioning-annots.6.res.oracle
+++ /dev/null
@@ -1,30 +0,0 @@
-[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
-[eva] Analyzing a complete application starting at test_slevel
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  k ∈ {0}
-  nondet ∈ [--..--]
-[eva] tests/value/partitioning-annots.c:152: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:157: starting to merge loop iterations
-[eva] Recording results for test_slevel
-[eva] done for function test_slevel
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function test_slevel:
-  a[0..9] ∈ {42}
-  b[0..9] ∈ {42} or UNINITIALIZED
-  c[0..3] ∈ {33; 42}
-   [4..9] ∈ {33; 42} or UNINITIALIZED
-  d[0..9] ∈ {33; 42}
-  e[0..3] ∈ {33; 42}
-[from] Computing for function test_slevel
-[from] Done for function test_slevel
-[from] ====== DEPENDENCIES COMPUTED ======
-  These dependencies hold at termination for the executions that terminate:
-[from] Function test_slevel:
-  NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function test_slevel:
-    a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
-[inout] Inputs for function test_slevel:
-    nondet
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 4aa95cc322dfd534d5126825fdb966d9e7e68d12..a0a6b0161c0fe51695fbf948f723a10cda7e372e 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -1,18 +1,18 @@
 /* run.config*
    
-   STDOPT: #"-main test_unroll -eva-default-loop-unroll 10"
-   STDOPT: #"-main test_split"
+   STDOPT: #"-eva-default-loop-unroll 10"
    STDOPT: +"-main test_split -eva-partition-value k"
    STDOPT: #"-main test_loop_split -eva-partition-history 1"
    STDOPT: #"-main test_history -eva-partition-history 0"
    STDOPT: #"-main test_history -eva-partition-history 1"
-   STDOPT: #"-main test_slevel"
    */
 
 #include "__fc_builtin.h"
 
 #define N 10
 
+volatile nondet;
+
 void test_unroll()
 {
   int a[N], b[N], c[2*N], d[2*N], e[N];
@@ -89,6 +89,26 @@ void test_split()
   Frama_C_show_each_end(i,j,k);
 }
 
+void test_dynamic_split()
+{
+  int a, b;
+  //@ dynamic_split a;
+  if (nondet) {
+    a = Frama_C_interval(0, 2);
+    b = a;
+  }
+  Frama_C_show_each_split_with_uninit(a, b);
+  a = 0;
+  Frama_C_show_each_no_split(a, b);
+  a = Frama_C_interval(0, 2);
+  b = a;
+  //@ split a;
+  a = 0;
+  Frama_C_show_each_split(a, b);
+  //@ merge a;
+  Frama_C_show_each_no_split(a, b);
+}
+
 void test_loop_split()
 {
   int A[N];
@@ -138,8 +158,6 @@ void test_history()
     k = k / j;
 }
 
-volatile nondet;
-
 void test_slevel()
 {
   int a[N], b[N], c[N], d[N], e[4];
@@ -187,6 +205,6 @@ void main(void)
   test_slevel();
   test_unroll();
   test_split();
-  test_loop_split();
+  test_dynamic_split();
 }