diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index f2f107b7d71bcab897a117084bf09c75464a1e2f..22658b485c9c1ccf9cb4a8a4aeece5a4ecfeb2df 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -83,8 +83,8 @@ struct
     in
     match get_unroll_annot stmt with
     | [] -> warn_no_loop_unroll stmt; default
-    | [None] -> Partition.IntLimit default_loop_unroll
-    | [(Some t)] -> begin
+    | [UnrollFull] -> Partition.IntLimit default_loop_unroll
+    | [UnrollAmount t] -> begin
         (* Inlines the value of const variables in [t]. *)
         let global_init vi =
           try (Globals.Vars.find vi).init with Not_found -> None
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index b3ea2a316b44b9e5788caacd587fff06207f41d5..7ba7cc2f97a77ed84d2c7cf939bcfe41e7ed3bc7 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -29,7 +29,9 @@ type slevel_annotation =
   | SlevelLocal of int
   | SlevelFull
 
-type unroll_annotation = term option
+type unroll_annotation =
+  | UnrollAmount of Cil_types.term
+  | UnrollFull
 
 type flow_annotation =
   | FlowSplit of term
@@ -169,31 +171,32 @@ struct
   let print = Printer.pp_term
 end
 
-module OptionalTermAnnotation =
-struct
-  type t = term option
+module Unroll = Register (struct
+    type t = unroll_annotation
 
-  let parse ~typing_context = function
-    | [] -> None
-    | [t] ->
-      let open Logic_typing in
-      Some (typing_context.type_term typing_context typing_context.pre_state t)
-    | _ -> raise Parse_error
+    let name = "unroll"
+    let is_loop_annot = true
 
-  let export t =
-    Ext_terms (Extlib.list_of_opt t)
+    let parse ~typing_context = function
+      | [{lexpr_node = PLvar "full"}] -> UnrollFull
+      | [t] ->
+        let open Logic_typing in
+        UnrollAmount
+          (typing_context.type_term typing_context typing_context.pre_state t)
+      | _ -> raise Parse_error
 
-  let import = function
-    | Ext_terms l -> Extlib.opt_of_list l
-    | _ -> assert false
+    let export = function
+      | UnrollFull -> Ext_terms [Logic_const.tstring "full"]
+      | UnrollAmount t -> Ext_terms [t]
 
-  let print = Pretty_utils.pp_opt Printer.pp_term
-end
+    let import = function
+      | Ext_terms [{term_node=TConst (LStr "full")}] -> UnrollFull
+      | Ext_terms [t] -> UnrollAmount t
+      | _ -> assert false
 
-module Unroll = Register (struct
-    include OptionalTermAnnotation
-    let name = "unroll"
-    let is_loop_annot = true
+    let print fmt = function
+      | UnrollFull -> Format.pp_print_string fmt "full"
+      | UnrollAmount t -> Printer.pp_term fmt t
   end)
 
 module Split = Register (struct
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index d1435ab8a19ad20bb74a8841a5f7fd7b585cf057..ab29469ee7102d9232128475653456b1e7fbaff2 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -34,7 +34,9 @@ type slevel_annotation =
   | SlevelLocal of int
   | SlevelFull
 
-type unroll_annotation = Cil_types.term option
+type unroll_annotation =
+  | UnrollAmount of Cil_types.term
+  | UnrollFull
 
 type flow_annotation =
   | FlowSplit of Cil_types.term
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index a9fae743efd0996aff15aeedae2a358a4fdcbba6..6e5eb5de0774db41b37a46bbeb4041c218789b85 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -15,6 +15,9 @@
 [eva:loop-unroll] tests/value/partitioning-annots.c:50: 
   loop not completely unrolled
 [eva] tests/value/partitioning-annots.c:50: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:66: 
+  loop not completely unrolled
+[eva] tests/value/partitioning-annots.c:66: starting to merge loop iterations
 [eva] Recording results for test_unroll
 [eva] done for function test_unroll
 [eva] ====== VALUES COMPUTED ======
@@ -33,6 +36,17 @@
    [7] ∈ {36}
    [8] ∈ {9}
    [9] ∈ {1}
+  f[0] ∈ {0}
+   [1] ∈ {1}
+   [2] ∈ {0}
+   [3] ∈ {1}
+   [4] ∈ {0}
+   [5] ∈ {1}
+   [6] ∈ {0}
+   [7] ∈ {1}
+   [8] ∈ {0}
+   [9] ∈ {1}
+   [10..19] ∈ {0; 1} or UNINITIALIZED
 [from] Computing for function test_unroll
 [from] Done for function test_unroll
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -41,7 +55,7 @@
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function test_unroll:
-    a[0..9]; b[0..9]; c[0..9]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1; 
-    i_2; i_3; j_1
+    a[0..9]; b[0..9]; c[0..9]; d[0..19]; e[0..9]; f[0..19]; i; j; i_0; 
+    j_0; i_1; i_2; i_3; j_1; i_4
 [inout] Inputs for function test_unroll:
     \nothing
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index 206434355ca402ec560fa72712e6690fddf5b5f3..a1f5d1c691646abb97a95d1c374d4655ae3b7892 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -6,41 +6,41 @@
   k ∈ {0}
   nondet ∈ [--..--]
 [eva] computing for function Frama_C_interval <- test_split.
-  Called from tests/value/partitioning-annots.c:69.
+  Called from tests/value/partitioning-annots.c:75.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:69: 
+[eva] tests/value/partitioning-annots.c:75: 
   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:70.
-[eva] tests/value/partitioning-annots.c:70: 
+  Called from tests/value/partitioning-annots.c:76.
+[eva] tests/value/partitioning-annots.c:76: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:76: 
+[eva] tests/value/partitioning-annots.c:82: 
   Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79: 
+[eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:79: 
+[eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
-[eva] tests/value/partitioning-annots.c:85: 
+[eva] tests/value/partitioning-annots.c:91: 
   Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
 [eva] Recording results for test_split
 [eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index e12cf3849fc45c326f6dff4382d0242655ff22c5..2f28a2b0b9ecb0d0527a622e57d8102454517e8b 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -6,49 +6,49 @@
   k ∈ {0}
   nondet ∈ [--..--]
 [eva] computing for function Frama_C_interval <- test_split.
-  Called from tests/value/partitioning-annots.c:69.
+  Called from tests/value/partitioning-annots.c:75.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:69: 
+[eva] tests/value/partitioning-annots.c:75: 
   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:70.
-[eva] tests/value/partitioning-annots.c:70: 
+  Called from tests/value/partitioning-annots.c:76.
+[eva] tests/value/partitioning-annots.c:76: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:76: 
+[eva] tests/value/partitioning-annots.c:82: 
   Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79: 
+[eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:79: 
+[eva] tests/value/partitioning-annots.c:85: 
   Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:81: 
+[eva] tests/value/partitioning-annots.c:87: 
   Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:83: 
+[eva] tests/value/partitioning-annots.c:89: 
   Frama_C_show_each_before_second_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:85: 
+[eva] tests/value/partitioning-annots.c:91: 
   Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:85: 
+[eva] tests/value/partitioning-annots.c:91: 
   Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
 [eva] Recording results for test_split
 [eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 6032746a9c9ca1f5d94b5cf7e7e9046138372c2c..c2989a6b2d5f8b44cc240803670bfbfa938f056b 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -6,41 +6,41 @@
   k ∈ {0}
   nondet ∈ [--..--]
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:103: 
+[eva] tests/value/partitioning-annots.c:109: 
   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:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:101: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:107: starting to merge loop iterations
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:103.
+  Called from tests/value/partitioning-annots.c:109.
 [eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/partitioning-annots.c:110: Warning: 
+[eva:alarm] tests/value/partitioning-annots.c:116: Warning: 
   accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {9}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {8}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:116: assertion got status valid.
-[eva] tests/value/partitioning-annots.c:119: 
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:121: Frama_C_show_each: {0}, {42}
+[eva] tests/value/partitioning-annots.c:122: assertion got status valid.
+[eva] tests/value/partitioning-annots.c:125: 
   Frama_C_show_each: {{ "Value 42 not found" }}
 [eva] Recording results for test_loop_split
 [eva] done for function test_loop_split
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index e950a97cac1ee2f5559aa3c149885b567bfe91b1..a008cf605259c4b844e8d11a10ce1b1edeab88e2 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,13 +6,13 @@
   k ∈ {0}
   nondet ∈ [--..--]
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from tests/value/partitioning-annots.c:125.
+  Called from tests/value/partitioning-annots.c:131.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:125: 
+[eva] tests/value/partitioning-annots.c:131: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] tests/value/partitioning-annots.c:134: Warning: 
+[eva] tests/value/partitioning-annots.c:137: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] tests/value/partitioning-annots.c:140: Warning: 
   division by zero. assert j ≢ 0;
 [eva] Recording results for test_history
 [eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
index c03065ca696952fa7f2483180a13542423aaad88..35f1b8e40b2b5950778778608c0ca6ad114531d5 100644
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ b/tests/value/oracle/partitioning-annots.5.res.oracle
@@ -6,13 +6,13 @@
   k ∈ {0}
   nondet ∈ [--..--]
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from tests/value/partitioning-annots.c:125.
+  Called from tests/value/partitioning-annots.c:131.
 [eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:125: 
+[eva] tests/value/partitioning-annots.c:131: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {0}, {0}
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {1}, {1}
+[eva] tests/value/partitioning-annots.c:137: Frama_C_show_each: {0}, {0}
+[eva] tests/value/partitioning-annots.c:137: 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.6.res.oracle b/tests/value/oracle/partitioning-annots.6.res.oracle
index e514eb8f8179d50f74d86ec8a9dbc97b94168081..99f4e6092170c3968e378ffe690522654a4257fc 100644
--- a/tests/value/oracle/partitioning-annots.6.res.oracle
+++ b/tests/value/oracle/partitioning-annots.6.res.oracle
@@ -5,9 +5,9 @@
 [eva:initial-state] Values of globals at initialization
   k ∈ {0}
   nondet ∈ [--..--]
-[eva] tests/value/partitioning-annots.c:148: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:153: starting to merge loop iterations
-[eva] tests/value/partitioning-annots.c:173: 
+[eva] tests/value/partitioning-annots.c:154: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:159: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:179: 
   Trace partitioning superposing up to 100 states
 [eva] Recording results for test_slevel
 [eva] done for function test_slevel
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 019ae54c958206f77a617ef7e23b4b5af062ad40..062adc54226058041e9cd18d7cef9bc683f17362 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -15,7 +15,7 @@
 
 void test_unroll()
 {
-  int a[N], b[N], c[N], d[2*N], e[N];
+  int a[N], b[N], c[N], d[2*N], e[N], f[2*N];
 
   // The inner loop needs to be unrolled to allow strong updates
   // The outer loops doesn't need to be unrolled
@@ -60,6 +60,12 @@ void test_unroll()
       e[j] += e[j-1];
     }
   }
+
+  // Full unroll is limited by option -eva-default-loop-unroll
+  //@ loop unroll full;
+  for (int i = 0 ; i < 2*N ; i++) {
+    f[i] = i % 2;
+  }
 }
 
 int k;