diff --git a/Makefile b/Makefile
index dd8b0234365cedef0c3d91c5f996c5e09fd151ae..77433b677c0f16679408e43853e1e56de7579ce5 100644
--- a/Makefile
+++ b/Makefile
@@ -860,9 +860,10 @@ endif
 # General rules for ordering files within PLUGIN_CMO:
 # - try to keep the legacy Value before Eva
 PLUGIN_CMO:= partitioning/split_strategy value_parameters \
-	utils/value_perf utils/value_util utils/red_statuses \
+	utils/value_perf utils/partitioning_annots \
+        utils/value_util utils/red_statuses \
 	utils/mark_noresults \
-	utils/widen_hints_ext utils/widen utils/partitioning_annots \
+	utils/widen_hints_ext utils/widen \
 	partitioning/split_return \
 	partitioning/per_stmt_slevel \
 	utils/library_functions \
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/partitioning_annots.ml
index 804c3c8e15f37979764c7bd0e1194606339a5261..767cf487636ff235b6e01cd46d9b498eb3c9c624 100644
--- a/src/plugins/value/utils/partitioning_annots.ml
+++ b/src/plugins/value/utils/partitioning_annots.ml
@@ -224,3 +224,30 @@ 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
+
+
+module Subdivision = Register (struct
+    type t = int
+    let name = "subdivide"
+    let is_loop_annot = false
+
+    let parse ~typing_context:_ = function
+      | [{lexpr_node = PLconstant (IntConstant i)}] ->
+        let i =
+          try int_of_string i
+          with Failure _ -> raise Parse_error
+        in
+        if i < 0 then raise Parse_error;
+        i
+      | _ -> raise Parse_error
+
+    let export i = Ext_terms [Logic_const.tinteger i]
+    let import = function
+      | Ext_terms [{term_node = TConst (Integer (i, _))}] -> Integer.to_int i
+      | _ -> assert false
+
+    let print fmt i = Format.pp_print_int fmt i
+  end)
+
+let get_subdivision_annot = Subdivision.get
+let add_subdivision_annot = Subdivision.add
diff --git a/src/plugins/value/utils/partitioning_annots.mli b/src/plugins/value/utils/partitioning_annots.mli
index a95de0105a702588333f4b03f8d12a7da496211e..3d86f2f40076ea0f421cc2c55287f9a5dfa8e62c 100644
--- a/src/plugins/value/utils/partitioning_annots.mli
+++ b/src/plugins/value/utils/partitioning_annots.mli
@@ -34,6 +34,7 @@ type flow_annotation =
 val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
 val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
 val get_flow_annot : Cil_types.stmt -> flow_annotation list
+val get_subdivision_annot : Cil_types.stmt -> int list
 
 val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> slevel_annotation -> unit
@@ -41,3 +42,5 @@ val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> unroll_annotation -> unit
 val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
   Cil_types.stmt -> flow_annotation -> unit
+val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+  Cil_types.stmt -> int -> unit
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 24df6f735e5e927b8ce97ea0a9a55b4c3eef7026..6db4c29ae6781d1a00ab709c5a73a5918439f254 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -71,12 +71,22 @@ let get_slevel kf =
   try Value_parameters.SlevelFunction.find kf
   with Not_found -> Value_parameters.SemanticUnrollingLevel.get ()
 
-let get_subdivision stmt =
+let get_subdivision_option stmt =
   try
     let kf = Kernel_function.find_englobing_kf stmt in
     Value_parameters.LinearLevelFunction.find kf
   with Not_found -> Value_parameters.LinearLevel.get ()
 
+let get_subdivision stmt =
+  match Partitioning_annots.get_subdivision_annot stmt with
+  | [] -> get_subdivision_option stmt
+  | [x] -> x
+  | x :: _ ->
+    Value_parameters.warning ~current:true ~once:true
+      "Several subdivision annotations at the same statement; selecting %i\
+       and ignoring the others." x;
+    x
+
 let pretty_actuals fmt actuals =
   let pp fmt (e,x,_) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
   Pretty_utils.pp_flowlist pp fmt actuals