diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index d63682d54178874f4cf78329fe3a9a967d9b5293..2d6a0264938aa29a20205f31e02c9ea059fb8163 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
 Plugin WP <next-release>
 #########################
 
+
+- WP          [2020-01-25] Improved -wp-unfold-assigns <depth>
+			   Now recursively applies to all compounds
 -* WP         [2020-01-20] Fixes opaque structures handling
 - TIP         [2020-11-06] New tactic: Sequence unrolling
 - TIP         [2020-11-05] New tactic: Induction
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 05e4e86b828ada52bcde0906bcf93b7df118fddc..668d62a29af65aba6c17c1650a2172fb786f1d27 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -473,13 +473,13 @@ struct
   let cc_logic : (env -> Cil_types.term -> logic) ref
     = ref (fun _ _ -> assert false)
   let cc_region
-    : (env -> unfold:bool -> Cil_types.term -> loc Sigs.region) ref
-    = ref (fun _ ~unfold _ -> ignore unfold ; assert false)
+    : (env -> Cil_types.term -> loc Sigs.region) ref
+    = ref (fun _ -> assert false)
 
   let term env t = !cc_term env t
   let pred polarity env t = !cc_pred polarity env t
   let logic env t = !cc_logic env t
-  let region env ~unfold t = !cc_region env ~unfold t
+  let region env t = !cc_region env t
   let reads env ts = List.iter (fun t -> ignore (logic env t.it_content)) ts
 
   let bootstrap_term cc = cc_term := cc
diff --git a/src/plugins/wp/LogicCompiler.mli b/src/plugins/wp/LogicCompiler.mli
index 9a4352ba05bde4383eb022ef259cc19f452200b9..c99371121b6f6c0244ba24909dd7d777cdbb20f3 100644
--- a/src/plugins/wp/LogicCompiler.mli
+++ b/src/plugins/wp/LogicCompiler.mli
@@ -101,14 +101,12 @@ sig
   val term : env -> Cil_types.term -> term
   val pred : polarity -> env -> predicate -> pred
   val logic : env -> Cil_types.term -> logic
-  val region : env -> unfold:bool -> Cil_types.term -> M.loc Sigs.region
-  (** When [~unfold:true], decompose compound regions field by field *)
+  val region : env -> Cil_types.term -> M.loc Sigs.region
 
   val bootstrap_term : (env -> Cil_types.term -> term) -> unit
   val bootstrap_pred : (polarity -> env -> predicate -> pred) -> unit
   val bootstrap_logic : (env -> Cil_types.term -> logic) -> unit
-  val bootstrap_region :
-    (env -> unfold:bool -> Cil_types.term -> M.loc Sigs.region) -> unit
+  val bootstrap_region : (env -> Cil_types.term -> M.loc Sigs.region) -> unit
 
   (** {3 Application} *)
 
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 682e9adb223dc0f278e5096391f8651254377669..2f18879a02c939e8fbde0266c9c982a3888bbec7 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -899,37 +899,18 @@ struct
   (* --- Set of locations for a term representing a set of l-values         --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let rec compound_offsets = function
-    | C_comp { cfields = Some fields ; cstruct = true } ->
-        List.fold_left
-          (fun offsets fd ->
-             List.fold_left
-               (fun offsets (obj,ofs) ->
-                  (obj , TField(fd,ofs)) :: offsets
-               ) offsets (compound_offsets (Ctypes.object_of fd.ftype))
-          ) [] fields
-    | obj -> [obj , TNoOffset]
-
-  let assignable_lval env ~unfold lv =
+  let assignable_lval env lv =
     match fst lv with
     | TResult _  | TVar{lv_name="\\exit_status"} -> [] (* special case ! *)
     | _ ->
-        let offsets =
-          let obj = Ctypes.object_of_logic_type (Cil.typeOfTermLval lv) in
-          if unfold then compound_offsets obj else [obj , TNoOffset]
-        in
-        List.concat
-          (List.map
-             (fun (obj,offset) ->
-                let lv = Logic_const.addTermOffsetLval offset lv in
-                L.region obj (addr_lval env lv))
-             offsets)
-
-  let assignable env ~unfold t =
+        let obj = Ctypes.object_of_logic_type (Cil.typeOfTermLval lv) in
+        L.region obj (addr_lval env lv)
+
+  let assignable env t =
     match t.term_node with
     | Tempty_set -> []
-    | TLval lv -> assignable_lval env ~unfold lv
-    | Tunion ts -> List.concat (List.map (C.region env ~unfold) ts)
+    | TLval lv -> assignable_lval env lv
+    | Tunion ts -> List.concat (List.map (C.region env) ts)
     | Tinter _ -> Warning.error "Intersection in assigns not implemented yet"
     | Tcomprehension(t,qs,cond) ->
         begin
@@ -945,22 +926,22 @@ struct
                | (Sarray _ | Srange _ | Sdescr _) as sloc ->
                    let ys,l,extend = L.rdescr sloc in
                    Sdescr(xs@ys,l,p_conj (extend :: conditions))
-            ) (C.region env ~unfold t)
+            ) (C.region env t)
         end
 
     | Tat(t,label) ->
-        C.region ~unfold (C.env_at env (Clabels.of_logic label)) t
+        C.region (C.env_at env (Clabels.of_logic label)) t
 
     | Tlet( { l_var_info=v ; l_body=LBterm a } , b ) ->
         let va = C.logic env a in
-        C.region ~unfold (C.env_let env v va) b
+        C.region (C.env_let env v va) b
 
     | Tlet _ ->
         Warning.error "Complex let-binding not implemented yet (%a)"
           Printer.pp_term t
 
     | TCastE (_,t)
-    | TLogic_coerce(_,t) -> C.region env ~unfold t
+    | TLogic_coerce(_,t) -> C.region env t
 
     | TBinOp _ | TUnOp _ | Trange _ | TUpdate _ | Tapp _ | Tif _
     | TConst _ | Tnull | TDataCons _ | Tlambda _
@@ -1023,8 +1004,8 @@ struct
   let logic env t =
     Context.with_current_loc t.term_loc (term_trigger env) t
 
-  let region env ~unfold t =
-    Context.with_current_loc t.term_loc (assignable env ~unfold) t
+  let region env t =
+    Context.with_current_loc t.term_loc (assignable env) t
 
   let () = C.bootstrap_pred pred
   let () = C.bootstrap_term term
@@ -1037,17 +1018,17 @@ struct
   (* --- Regions                                                            --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let assigned_of_lval env ~unfold (lv : Cil_types.lval) =
-    assignable_lval env ~unfold (Logic_utils.lval_to_term_lval lv)
+  let assigned_of_lval env (lv : Cil_types.lval) =
+    assignable_lval env (Logic_utils.lval_to_term_lval lv)
 
-  let assigned_of_froms env ~unfold froms =
+  let assigned_of_froms env froms =
     List.concat
       (List.map
-         (fun ({it_content=wr},_deps) -> region env ~unfold wr) froms)
+         (fun ({it_content=wr},_deps) -> region env wr) froms)
 
-  let assigned_of_assigns env ~unfold = function
+  let assigned_of_assigns env = function
     | WritesAny -> None
-    | Writes froms -> Some (assigned_of_froms env ~unfold froms)
+    | Writes froms -> Some (assigned_of_froms env froms)
 
   let occurs_opt x = function None -> false | Some t -> F.occurs x t
 
@@ -1082,12 +1063,63 @@ struct
   (* --- CheckAssigns                                                       --- *)
   (* -------------------------------------------------------------------------- *)
 
-  let check_assigns sigma ~written ~assignable =
+  let rec assignable_region unfold reg assignable =
+    let inclusion = p_any (L.included reg) assignable in
+    if unfold = 0 then inclusion
+    else p_or inclusion (assignable_unfolded_region unfold reg assignable)
+
+  (* Note that when a region cannot be unfolded anymore (that is, when it is a
+     [Sloc] with atomic type, including unknown size arrays and opaque structs),
+     the function return [p_false]. *)
+  and assignable_unfolded_region unfold (obj, sloc) assignable =
+    let range size = Some e_zero, Some (e_sub (e_int size) e_one) in
+    match sloc with
+    | Sloc loc ->
+        begin match obj with
+          | C_pointer _ | C_int _ | C_float _
+          | C_comp { cfields = None } | C_array { arr_flat = None } ->
+              (* Nothing to unfold *)
+              p_false
+
+          | C_comp { cfields = Some fields } ->
+              let assignable_field f =
+                let reg = Ctypes.object_of f.ftype, Sloc (M.field loc f) in
+                assignable_region (unfold-1) reg assignable
+              in
+              p_conj (List.map assignable_field fields)
+
+          | C_array { arr_flat = Some { arr_size=len ; arr_cell=typ } } ->
+              let obj = Ctypes.object_of typ in
+              assignable_unfolded_range unfold loc obj (range len) assignable
+        end
+
+    | Sarray (loc, obj, len) ->
+        assignable_unfolded_range unfold loc obj (range len) assignable
+
+    | Srange (loc, obj, b, e) ->
+        assignable_unfolded_range unfold loc obj (b, e) assignable
+
+    | Sdescr (xs, loc, guard) ->
+        assignable_unfolded_descr unfold obj xs loc guard assignable
+
+  and assignable_unfolded_range unfold loc obj (low, up) =
+    let x = Lang.freshvar ~basename:"k" Lang.t_int in
+    let k = e_var x in
+    let guard = Vset.in_range k low up in
+    let loc = M.shift loc obj k in
+    assignable_unfolded_descr unfold obj [x] loc guard
+
+  and assignable_unfolded_descr unfold obj xs loc guard assignable =
+    p_forall xs
+      (p_imply guard
+         (assignable_region (unfold-1) (obj, Sloc loc) assignable))
+
+  let check_assigns ~unfold sigma ~written ~assignable =
     p_all
-      (fun seg ->
+      (fun reg ->
          p_imply
-           (p_not (L.invalid sigma seg))
-           (p_any (L.included seg) assignable)
+           (p_not (L.invalid sigma reg))
+           (assignable_region unfold reg assignable)
       ) (written : region)
 
 end
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 1b594803754f617a5c0b63f94f1216275517fed2..5474a05068ca7c5e1a429631d7654620c7976746 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -773,22 +773,21 @@ sig
   val pred : polarity -> env -> Cil_types.predicate -> pred
 
   (** Compile a term representing a set of memory locations into an abstract
-      region. When [~unfold:true], compound memory locations are expanded
-      field-by-field. *)
-  val region : env -> unfold:bool -> Cil_types.term -> region
+      region.  *)
+  val region : env -> Cil_types.term -> region
 
   (** Computes the region assigned by a list of froms. *)
   val assigned_of_lval :
-    env -> unfold:bool -> Cil_types.lval -> region
+    env -> Cil_types.lval -> region
 
   (** Computes the region assigned by a list of froms. *)
   val assigned_of_froms :
-    env -> unfold:bool -> from list -> region
+    env -> from list -> region
 
   (** Computes the region assigned by an assigns clause.
       [None] means everyhting is assigned. *)
   val assigned_of_assigns :
-    env -> unfold:bool -> assigns -> region option
+    env -> assigns -> region option
 
   (** Same as [term] above but reject any set of locations. *)
   val val_of_term : env -> Cil_types.term -> term
@@ -810,9 +809,12 @@ sig
 
   (** Check assigns inclusion.
       Compute a formula that checks whether written locations are either
-      invalid (at the given memory location)
-      or included in some assignable region. *)
-  val check_assigns : sigma -> written:region -> assignable:region -> pred
+      invalid (at the given memory location) or included in some assignable
+      region. When [~unfold:n && n <> 0], compound memory locations are expanded
+      field-by-field and arrays, cell-by-cell (by quantification). Up to [n]
+      levels are unfolded, -1 means unlimited. *)
+  val check_assigns :
+    unfold:int -> sigma -> written:region -> assignable:region -> pred
 
 end
 
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 4272a3333deb1d013d8d4681454ad19a04edd7b2..f5236949e0ae9c9826c14289b87253d90caf0a88 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -479,7 +479,7 @@ struct
     let lenv = L.mk_env () in (* TODO: lenv for ghost code. *)
     let here = Sigma.create () in
     let authorized_region = L.in_frame frame
-        (L.assigned_of_assigns ~unfold:false lenv) a in
+        (L.assigned_of_assigns lenv) a in
     match authorized_region with
     | None -> goto (env @: Clabels.here) (env @: Clabels.next)
     | Some region ->
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ebf53f21db45ecbb6bf1ff01e0d28e5bc80355b2..10e8f697cc36b0b6661322887304f508016772cb 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -437,7 +437,7 @@ struct
     let from = ainfo.WpPropId.a_label in
     let sigma = L.mem_frame from in
     let authorized_region =
-      L.assigned_of_assigns ~unfold:false
+      L.assigned_of_assigns
         (match ainfo.a_kind with
          | StmtAssigns -> L.move_at env sigma
          | LoopAssigns -> env)
@@ -517,7 +517,8 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   let assigns_condition (region : L.region) (e:effect) : F.pred =
-    L.check_assigns e.e_valid ~written:region ~assignable:e.e_region
+    let unfold = Wp_parameters.UnfoldAssigns.get () in
+    L.check_assigns ~unfold e.e_valid ~written:region ~assignable:e.e_region
 
   exception COLLECTED
 
@@ -567,8 +568,8 @@ struct
       ) effects vcs
 
   let do_assigns ?descr ?stmt ~source ?hpid ?warn sequence
-      ~assigned ?(unfolded=assigned) effects vcs =
-    let vcs = check_assigns stmt source ?warn unfolded effects vcs in
+      ~assigned effects vcs =
+    let vcs = check_assigns stmt source ?warn assigned effects vcs in
     let eqmem = A.apply_assigns sequence assigned in
     gmap (assume_vc ?descr ?hpid ?stmt ?warn eqmem) vcs
 
@@ -582,13 +583,9 @@ struct
          add_vc target ?warn F.p_false vcs)
       effects vcs
 
-  let cc_region ~unfold cc data =
-    let assigned = cc ~unfold:false data in
-    assigned , if unfold then cc ~unfold:true data else assigned
-
-  let cc_assigned env ~unfold kind froms =
+  let cc_assigned env kind froms =
     let dummy = Sigma.create () in
-    let r0 = L.assigned_of_froms ~unfold:false (L.move_at env dummy) froms in
+    let r0 = L.assigned_of_froms (L.move_at env dummy) froms in
     let d0 = A.domain r0 in
     let s1 = L.current env in
     let s0 = Sigma.havoc s1 d0 in
@@ -597,9 +594,9 @@ struct
       | LoopAssigns -> s1
     in
     let cc_assigned = L.assigned_of_froms (L.move_at env sref) in
-    let assigned,unfolded = cc_region ~unfold cc_assigned froms in
+    let assigned = cc_assigned froms in
     let sequence = { pre=s0 ; post=s1 } in
-    sequence , assigned , unfolded
+    sequence , assigned
 
   let use_assigns wenv stmt hpid ainfo wp = in_wenv wenv wp
       begin fun env wp ->
@@ -612,17 +609,16 @@ struct
 
         | Writes froms ->
             let kind = ainfo.WpPropId.a_kind in
-            let unfold = Wp_parameters.UnfoldAssigns.get () in
             let outcome =
               Warning.catch ~severe:true ~effect:"Assigns everything"
-                (cc_assigned env ~unfold kind) froms
+                (cc_assigned env kind) froms
             in
             match outcome with
-            | Warning.Result(warn,(sequence,assigned,unfolded)) ->
+            | Warning.Result(warn,(sequence,assigned)) ->
                 let vcs =
                   do_assigns ~source:FromCode
                     ?hpid ?stmt ~warn sequence
-                    ~assigned ~unfolded
+                    ~assigned
                     wp.effects wp.vcs in
                 { sigma = Some sequence.pre ; vcs=vcs ; effects = wp.effects }
             | Warning.Failed warn ->
@@ -708,14 +704,7 @@ struct
             { sigma = Some sigma ; vcs=vcs ; effects = wp.effects }
         | Warning.Result(l_warn,(obj,dom,seq,loc)) ->
             (* L-Value has been translated *)
-            let unfold = Wp_parameters.UnfoldAssigns.get () in
-            let assigned,unfolded =
-              if unfold && Ctypes.is_compound obj then
-                let env_pre = L.move_at env seq.pre in
-                cc_region ~unfold (L.assigned_of_lval env_pre) lv
-              else
-                let region = [obj,Sloc loc] in region,region
-            in
+            let assigned = [obj,Sloc loc] in
             let outcome = Warning.catch
                 ~severe:false ~effect:"Havoc l-value (unknown r-value)"
                 (cc_stored lv seq loc obj) expr in
@@ -725,7 +714,7 @@ struct
                 (* R-Value is unknown or L-Value is volatile *)
                 let warn = Warning.Set.union l_warn r_warn in
                 let vcs = do_assigns ~source:FromCode
-                    ~stmt ~warn seq ~assigned ~unfolded wp.effects wp.vcs in
+                    ~stmt ~warn seq ~assigned wp.effects wp.vcs in
                 { sigma = Some seq.pre ; vcs=vcs ; effects = wp.effects }
             | Warning.Result(r_warn,Some stored) ->
                 (* R-Value and effects has been translated *)
@@ -741,7 +730,7 @@ struct
                   else vc in
                 let vcs = gmap update wp.vcs in
                 let vcs =
-                  check_assigns (Some stmt) FromCode unfolded wp.effects vcs in
+                  check_assigns (Some stmt) FromCode assigned wp.effects vcs in
                 { sigma = Some seq.pre ; vcs=vcs ; effects = wp.effects }
       end
 
@@ -1048,8 +1037,7 @@ struct
         let env = L.move_at env0 dummy in
         let init = L.mem_at env0 Clabels.init in
         let frame = L.call_pre init (L.call kf vs) dummy in
-        let unfold = Wp_parameters.UnfoldAssigns.get () in
-        let cc_froms = L.assigned_of_froms ~unfold env in
+        let cc_froms = L.assigned_of_froms env in
         Some (A.domain (L.in_frame frame cc_froms froms))
 
   let cc_havoc d s = match d with
@@ -1102,14 +1090,12 @@ struct
         }
     | Writes froms ->
         let env = L.move_at env0 cenv.sigma_pre in
-        let unfold = Wp_parameters.UnfoldAssigns.get () in
-        let assigned,unfolded = L.in_frame cenv.frame_pre
-            (cc_region ~unfold (L.assigned_of_froms env))
-            froms in
+        let assigned = L.in_frame cenv.frame_pre
+            (L.assigned_of_froms env) froms in
         let vcs_post = do_assigns ~descr:"Call Effects" ~source:FromCall
-            ~stmt cenv.seq_post ~assigned ~unfolded wpost.effects wpost.vcs in
+            ~stmt cenv.seq_post ~assigned wpost.effects wpost.vcs in
         let vcs_exit = do_assigns ~descr:"Exit Effects" ~source:FromCall
-            ~stmt cenv.seq_exit ~assigned ~unfolded wexit.effects wexit.vcs in
+            ~stmt cenv.seq_exit ~assigned wexit.effects wexit.vcs in
         let vcs_result =
           match cenv.loc_result with
           | None -> vcs_post (* no result *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 2b8883193da78ee750e872a9c73aa84695972f98..c44452f15e11463a5d8e28fa88ae47ce095a7f49 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -956,12 +956,16 @@ weakest precondition calculus.
   a call (default is: \texttt{yes}).
 \item[\tt -wp-(no)-precond-weakening] discard pre-conditions of side behaviours (sound but
   incomplete optimisation, default is: \texttt{no}).
-\item[\tt -wp-(no)-unfold-assigns] prove assigns goal of \texttt{struct}
-  compound types field by field. This allows for proving that assigning
-  a complete structure is still included into an assignment field by field.
-  This option is not set by default, because it is generally not necessary
-  and it can generates a large number of verifications for structures
-  with many (nested) fields (defaults to \texttt{no}).
+\item[\tt -wp-unfold-assigns <{\it n}>] when proving assigns, unfold up to
+  \textit{n} levels of \texttt{struct} compounds types or access via ranges.
+  \texttt{struct} are unfolded field by field, ranges are unfolded cell by
+  cell (via a universal quantification over the index of the cell).
+  This allows for proving that assigning a complete structure is still included
+  into an assignment field by field, or that assigning a range is still included
+  in a union of subranges. This option is set to \texttt{0} by default, because
+  it is generally not necessary and it can generates a large number of
+  verifications for structures with many (nested) fields. \texttt{-1} enables
+  full unfolding.
 \item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
   thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
 \end{description}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index 60291308af6ae635ff1c00dd98d81a973bf7cae4..2d1564ec103f271134e9c6d88437e7821b2bb94a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -6,8 +6,8 @@
   Function ASSIGN_NO_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 62) in 'ASSIGN_NO_UNFOLD_KO':
-Effect at line 65
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 66) in 'ASSIGN_NO_UNFOLD_KO':
+Effect at line 69
 Assume {
   (* Heap *)
   Type: (region(s.base) <= 0) /\ linked(Malloc_0).
@@ -21,17 +21,77 @@ Prove: false.
   Function ASSIGN_NO_UNFOLD_OK
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFOLD_OK':
-Effect at line 59
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 60) in 'ASSIGN_NO_UNFOLD_OK':
+Effect at line 63
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Assume {
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Assume {
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: included(s, 4, shift_sint32(shiftfield_F2_With_array_t(s), 1), n).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function NO_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 33) in 'NO_UNFOLD_KO':
-Call Effect at line 35
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
 Assume {
   (* Heap *)
   Type: (region(s.base) <= 0) /\ linked(Malloc_0).
@@ -42,8 +102,8 @@ Prove: false.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 33) in 'NO_UNFOLD_KO':
-Call Effect at line 35
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
 Assume {
   (* Heap *)
   Type: (region(s.base) <= 0) /\ linked(Malloc_0).
@@ -57,14 +117,14 @@ Prove: false.
   Function NO_UNFOLD_OK_1
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 18) in 'NO_UNFOLD_OK_1':
-Call Effect at line 20
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 18) in 'NO_UNFOLD_OK_1':
-Call Effect at line 20
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
 Prove: true.
 
 ------------------------------------------------------------
@@ -72,14 +132,14 @@ Prove: true.
   Function NO_UNFOLD_OK_2
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 23) in 'NO_UNFOLD_OK_2':
-Call Effect at line 25
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 23) in 'NO_UNFOLD_OK_2':
-Call Effect at line 25
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
 Prove: true.
 
 ------------------------------------------------------------
@@ -87,22 +147,168 @@ Prove: true.
   Function NO_UNFOLD_OK_3
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3':
-Call Effect at line 30
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3':
-Call Effect at line 30
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint32(p, 0), 5).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, a, x).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+    included(a, x, shift_sint32(p, n), 1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, a, x).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+    included(a, x, shift_sint32(p, n), 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_S2_With_array(s, 0), 12).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 1).
+Let a_2 = shiftfield_F2_With_array_t(a).
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, a, x_1).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
+    included(a, x_1, shift_sint32(a_2, 0), 1) \/
+    included(a, x_1, shift_sint32(a_2, 1), m) \/
+    included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 1).
+Let a_2 = shiftfield_F2_With_array_t(a).
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, a, x_1).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, shift_S2_With_array(s, 2), x - 4) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_1), 1) \/
+    included(a, x_1, shift_sint32(a_2, 0), 1) \/
+    included(a, x_1, shift_sint32(a_2, 1), m) \/
+    included(a, x_1, shift_sint32(shiftfield_F2_With_array_t(a_1), 0), 1 + m).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function USE_ASSIGN_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 48) in 'USE_ASSIGN_UNFOLD_KO':
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
 Let a = Load_S1_S(q, Mint_0).
 Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
 Assume {
@@ -116,8 +322,8 @@ Prove: EqS1_S(a_1, a).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 49) in 'USE_ASSIGN_UNFOLD_KO':
-Call Effect at line 53
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
 Assume {
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0).
@@ -128,8 +334,8 @@ Prove: false.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 49) in 'USE_ASSIGN_UNFOLD_KO':
-Call Effect at line 53
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
 Assume {
   (* Heap *)
   Type: (region(p.base) <= 0) /\ linked(Malloc_0).
@@ -143,7 +349,7 @@ Prove: false.
   Function USE_ASSIGN_UNFOLD_OK
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 39) in 'USE_ASSIGN_UNFOLD_OK':
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
 Let a = Load_S1_S(q, Mint_0).
 Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
 Assume {
@@ -157,14 +363,14 @@ Prove: EqS1_S(a_1, a).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 40) in 'USE_ASSIGN_UNFOLD_OK':
-Call Effect at line 44
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 40) in 'USE_ASSIGN_UNFOLD_OK':
-Call Effect at line 44
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index f681ec0f92309c15f8c0dc760963fec77f356d88..f535f35f15d35c0a3db92e765e1965df17cb0d0f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -6,8 +6,8 @@
   Function ASSIGN_NO_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 62) in 'ASSIGN_NO_UNFOLD_KO':
-Effect at line 65
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 66) in 'ASSIGN_NO_UNFOLD_KO':
+Effect at line 69
 Prove: true.
 
 ------------------------------------------------------------
@@ -15,23 +15,81 @@ Prove: true.
   Function ASSIGN_NO_UNFOLD_OK
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 56) in 'ASSIGN_NO_UNFOLD_OK':
-Effect at line 59
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 60) in 'ASSIGN_NO_UNFOLD_OK':
+Effect at line 63
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Have: 0 < i.
+  Have: i <= 2.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: (i = (-1)) \/ included(s, 4, a_1, n) \/ included(a, 3, a_1, n) \/
+    included(shift_sint32(a, i), 1, a_1, n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Have: 0 < i.
+  Have: i <= 2.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: (i = (-1)) \/ included(s, 4, a_1, n) \/ included(a, 3, a_1, n) \/
+    included(shift_sint32(a, i), 1, a_1, n).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function NO_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 33) in 'NO_UNFOLD_KO':
-Call Effect at line 35
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 33) in 'NO_UNFOLD_KO':
-Call Effect at line 35
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
 Prove: true.
 
 ------------------------------------------------------------
@@ -39,14 +97,14 @@ Prove: true.
   Function NO_UNFOLD_OK_1
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 18) in 'NO_UNFOLD_OK_1':
-Call Effect at line 20
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 18) in 'NO_UNFOLD_OK_1':
-Call Effect at line 20
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
 Prove: true.
 
 ------------------------------------------------------------
@@ -54,14 +112,14 @@ Prove: true.
   Function NO_UNFOLD_OK_2
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 23) in 'NO_UNFOLD_OK_2':
-Call Effect at line 25
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 23) in 'NO_UNFOLD_OK_2':
-Call Effect at line 25
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
 Prove: true.
 
 ------------------------------------------------------------
@@ -69,22 +127,226 @@ Prove: true.
   Function NO_UNFOLD_OK_3
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3':
-Call Effect at line 30
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3':
-Call Effect at line 30
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Let x = 4 * i.
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: (i = 2) \/
+    (((i = 0) \/ (i = 1) \/ (2 <= i)) /\
+     ((i = 1) \/ (2 <= i) \/
+      (forall i_1 : Z. let x_1 = i_1 + x in ((0 <= i_1) -> ((i_1 <= 2) ->
+       ((x_1 = (-1)) \/ (x_1 = 0) \/ (x_1 = 3) \/
+        ((0 < x_1) /\ (x_1 <= 2)) \/ ((4 <= x_1) /\ (x_1 <= 6)) \/
+        ((7 <= x_1) /\ (x_1 <= 10)))))))).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Let x = 4 * i.
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: (i = 2) \/
+    (((i = 0) \/ (i = 1) \/ (2 <= i)) /\
+     ((i = 1) \/ (2 <= i) \/
+      (forall i_1 : Z. let x_1 = i_1 + x in ((0 <= i_1) -> ((i_1 <= 2) ->
+       ((x_1 = (-1)) \/ (x_1 = 0) \/ (x_1 = 3) \/
+        ((0 < x_1) /\ (x_1 <= 2)) \/ ((4 <= x_1) /\ (x_1 <= 6)) \/
+        ((7 <= x_1) /\ (x_1 <= 10)))))))).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Let a_7 = shiftfield_F2_With_array_x(a_2).
+Let a_8 = shiftfield_F2_With_array_t(a_2).
+Let x_4 = 4 * i.
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3) \/
+    (((i = 0) \/ (i = 1) \/ included(a_7, 1, a_1, x_2) \/
+      included(a_7, 1, a_5, m) \/ included(a_7, 1, a_6, x_3)) /\
+     (included(a_8, 3, a_1, x_2) \/ included(a_8, 3, a_5, m) \/
+      included(a_8, 3, a_6, x_3) \/
+      (forall i_1 : Z. let x_5 = i_1 + x_4 in
+       let a_9 = shift_sint32(a_8, i_1) in ((0 <= i_1) -> ((i_1 <= 2) ->
+       ((x_5 = (-1)) \/ (x_5 = 0) \/ (x_5 = 3) \/
+        included(a_9, 1, a_1, x_2) \/ included(a_9, 1, a_5, m) \/
+        included(a_9, 1, a_6, x_3))))))).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Let a_7 = shiftfield_F2_With_array_x(a_2).
+Let a_8 = shiftfield_F2_With_array_t(a_2).
+Let x_4 = 4 * i.
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3) \/
+    (((i = 0) \/ (i = 1) \/ included(a_7, 1, a_1, x_2) \/
+      included(a_7, 1, a_5, m) \/ included(a_7, 1, a_6, x_3)) /\
+     (included(a_8, 3, a_1, x_2) \/ included(a_8, 3, a_5, m) \/
+      included(a_8, 3, a_6, x_3) \/
+      (forall i_1 : Z. let x_5 = i_1 + x_4 in
+       let a_9 = shift_sint32(a_8, i_1) in ((0 <= i_1) -> ((i_1 <= 2) ->
+       ((x_5 = (-1)) \/ (x_5 = 0) \/ (x_5 = 3) \/
+        included(a_9, 1, a_1, x_2) \/ included(a_9, 1, a_5, m) \/
+        included(a_9, 1, a_6, x_3))))))).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function USE_ASSIGN_UNFOLD_KO
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 48) in 'USE_ASSIGN_UNFOLD_KO':
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
 Let a = Load_S1_S(q, Mint_0).
 Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
 Assume {
@@ -98,14 +360,14 @@ Prove: EqS1_S(a_1, a).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 49) in 'USE_ASSIGN_UNFOLD_KO':
-Call Effect at line 53
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 49) in 'USE_ASSIGN_UNFOLD_KO':
-Call Effect at line 53
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
 Prove: true.
 
 ------------------------------------------------------------
@@ -113,7 +375,7 @@ Prove: true.
   Function USE_ASSIGN_UNFOLD_OK
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 39) in 'USE_ASSIGN_UNFOLD_OK':
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
 Let a = Load_S1_S(q, Mint_0).
 Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
 Assume {
@@ -127,14 +389,14 @@ Prove: EqS1_S(a_1, a).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 40) in 'USE_ASSIGN_UNFOLD_OK':
-Call Effect at line 44
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 40) in 'USE_ASSIGN_UNFOLD_OK':
-Call Effect at line 44
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..033ab3d4f1c96a2be3b8fe64a10e2e1b1d3a9d12
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.2.res.oracle
@@ -0,0 +1,378 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function ASSIGN_NO_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 66) in 'ASSIGN_NO_UNFOLD_KO':
+Effect at line 69
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function ASSIGN_NO_UNFOLD_OK
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 60) in 'ASSIGN_NO_UNFOLD_OK':
+Effect at line 63
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Have: 0 < i.
+  Have: i <= 2.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: (i = (-1)) \/ included(s, 4, a_1, n) \/ included(a, 3, a_1, n) \/
+    included(shift_sint32(a, i), 1, a_1, n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Have: 0 < i.
+  Have: i <= 2.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: (i = (-1)) \/ included(s, 4, a_1, n) \/ included(a, 3, a_1, n) \/
+    included(shift_sint32(a, i), 1, a_1, n).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_1
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_2
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_3
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: (i = 2) \/
+    (((i = 1) \/ (2 <= i)) /\ ((i = 0) \/ (i = 1) \/ (2 <= i))).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: (i = 2) \/
+    (((i = 1) \/ (2 <= i)) /\ ((i = 0) \/ (i = 1) \/ (2 <= i))).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Let a_7 = shiftfield_F2_With_array_t(a_2).
+Let a_8 = shiftfield_F2_With_array_x(a_2).
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3) \/
+    ((included(a_7, 3, a_1, x_2) \/ included(a_7, 3, a_5, m) \/
+      included(a_7, 3, a_6, x_3)) /\
+     ((i = 0) \/ (i = 1) \/ included(a_8, 1, a_1, x_2) \/
+      included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_3))).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Let a_7 = shiftfield_F2_With_array_t(a_2).
+Let a_8 = shiftfield_F2_With_array_x(a_2).
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3) \/
+    ((included(a_7, 3, a_1, x_2) \/ included(a_7, 3, a_5, m) \/
+      included(a_7, 3, a_6, x_3)) /\
+     ((i = 0) \/ (i = 1) \/ included(a_8, 1, a_1, x_2) \/
+      included(a_8, 1, a_5, m) \/ included(a_8, 1, a_6, x_3))).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function USE_ASSIGN_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
+Let a = Load_S1_S(q, Mint_0).
+Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Assume {
+  Type: IsS1_S(a) /\ IsS1_S(a_1).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
+  (* Goal *)
+  When: separated(p, 2, q, 2).
+}
+Prove: EqS1_S(a_1, a).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function USE_ASSIGN_UNFOLD_OK
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
+Let a = Load_S1_S(q, Mint_0).
+Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Assume {
+  Type: IsS1_S(a) /\ IsS1_S(a_1).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
+  (* Goal *)
+  When: separated(p, 2, q, 2).
+}
+Prove: EqS1_S(a_1, a).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d6391ac676aed68ae010ebb11022285ddb5b4ced
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.3.res.oracle
@@ -0,0 +1,370 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function ASSIGN_NO_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 66) in 'ASSIGN_NO_UNFOLD_KO':
+Effect at line 69
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function ASSIGN_NO_UNFOLD_OK
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 60) in 'ASSIGN_NO_UNFOLD_OK':
+Effect at line 63
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 95) in 'NESTED_ARRAY_STATIC':
+Call Effect at line 97
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: included(s, 4, a_1, n) \/ included(a, 3, a_1, n).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 102) in 'NESTED_ARRAY_VARS':
+Call Effect at line 104
+Let a = shiftfield_F2_With_array_t(s).
+Let a_1 = shift_sint32(a, 1).
+Assume {
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, s, 4).
+  (* Pre-condition *)
+  Have: 3 <= n.
+}
+Prove: included(s, 4, a_1, n) \/ included(a, 3, a_1, n).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 37) in 'NO_UNFOLD_KO':
+Call Effect at line 39
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_1
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 22) in 'NO_UNFOLD_OK_1':
+Call Effect at line 24
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_2
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 27) in 'NO_UNFOLD_OK_2':
+Call Effect at line 29
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function NO_UNFOLD_OK_3
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 32) in 'NO_UNFOLD_OK_3':
+Call Effect at line 34
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 75) in 'PARTIAL_ASSIGNS_STATIC':
+Call Effect at line 77
+Assume {
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 4) /\ (!invalid(Malloc_0, shift_sint32(p, 0), 5)).
+}
+Prove: (i = 0) \/ (i = 4) \/ ((0 < i) /\ (i <= 3)).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function PARTIAL_ASSIGNS_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 81) in 'PARTIAL_ASSIGNS_VARS':
+Call Effect at line 83
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Let a_1 = shift_sint32(p, 1).
+Let x_1 = n - 1.
+Assume {
+  Have: 0 <= n.
+  Type: is_uint32(n).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x)).
+  (* Pre-condition *)
+  Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/ (n <= 0) \/ included(a, x, a_1, x_1) \/
+    included(a, x, shift_sint32(p, n), 1) \/
+    included(shift_sint32(p, i), 1, a_1, x_1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_STATIC
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: i = 2.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 111) in 'RANGE_NESTED_ARRAY_STATIC':
+Call Effect at line 116
+Assume {
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2) /\
+      (!invalid(Malloc_0, shift_S2_With_array(s, 0), 12)).
+}
+Prove: i = 2.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function RANGE_NESTED_ARRAY_VARS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 121) in 'RANGE_NESTED_ARRAY_VARS':
+Call Effect at line 126
+Let a = shift_S2_With_array(s, 0).
+Let x = 4 * n.
+Let x_1 = 4 + x.
+Let a_1 = shift_S2_With_array(s, 2).
+Let x_2 = x - 4.
+Let a_2 = shift_S2_With_array(s, i).
+Let a_3 = shift_S2_With_array(s, 1).
+Let a_4 = shiftfield_F2_With_array_t(a).
+Let a_5 = shift_sint32(a_4, 1).
+Let a_6 = shift_sint32(shiftfield_F2_With_array_t(a_3), 0).
+Let x_3 = 1 + m.
+Assume {
+  Type: is_uint32(m) /\ is_uint32(n).
+  (* Heap *)
+  Type: (region(s.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: (0 <= i) /\ (i <= n) /\ (!invalid(Malloc_0, a, x_1)).
+  (* Pre-condition *)
+  Have: (3 <= n) /\ (4 <= m).
+}
+Prove: (n < 0) \/ included(a, x_1, a_1, x_2) \/ included(a_2, 4, a_1, x_2) \/
+    included(a, x_1, shiftfield_F2_With_array_x(a_3), 1) \/
+    included(a, x_1, shift_sint32(a_4, 0), 1) \/ included(a, x_1, a_5, m) \/
+    included(a, x_1, a_6, x_3) \/ included(a_2, 4, a_5, m) \/
+    included(a_2, 4, a_6, x_3).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function USE_ASSIGN_UNFOLD_KO
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 52) in 'USE_ASSIGN_UNFOLD_KO':
+Let a = Load_S1_S(q, Mint_0).
+Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Assume {
+  Type: IsS1_S(a) /\ IsS1_S(a_1).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
+  (* Goal *)
+  When: separated(p, 2, q, 2).
+}
+Prove: EqS1_S(a_1, a).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 53) in 'USE_ASSIGN_UNFOLD_KO':
+Call Effect at line 57
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function USE_ASSIGN_UNFOLD_OK
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/unfold_assigns.i, line 43) in 'USE_ASSIGN_UNFOLD_OK':
+Let a = Load_S1_S(q, Mint_0).
+Let a_1 = Load_S1_S(q, havoc(Mint_undef_0, Mint_0, p, 2)).
+Assume {
+  Type: IsS1_S(a) /\ IsS1_S(a_1).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
+  (* Goal *)
+  When: separated(p, 2, q, 2).
+}
+Prove: EqS1_S(a_1, a).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 44) in 'USE_ASSIGN_UNFOLD_OK':
+Call Effect at line 48
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..32f7db5c4ff69fdade8bc819347b2c04b06f58a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.0.res.oracle
@@ -0,0 +1,53 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 28 goals scheduled
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_OK_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_KO_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_normal : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_OK_assigns : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_KO_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_normal : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_exit : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_normal : Valid
+[wp] Proved goals:   28 / 28
+  Qed:            16 
+  Alt-Ergo:       12
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  NO_UNFOLD_OK_1            2        -        2       100%
+  NO_UNFOLD_OK_2            2        -        2       100%
+  NO_UNFOLD_OK_3            2        -        2       100%
+  NO_UNFOLD_KO              2        -        2       100%
+  USE_ASSIGN_UNFOLD_OK      2        1        3       100%
+  USE_ASSIGN_UNFOLD_KO      2        1        3       100%
+  ASSIGN_NO_UNFOLD_OK       1        -        1       100%
+  ASSIGN_NO_UNFOLD_KO       1        -        1       100%
+  PARTIAL_ASSIGNS_STATIC    -        2        2       100%
+  PARTIAL_ASSIGNS_VARS      -        2        2       100%
+  NESTED_ARRAY_STATIC       2        -        2       100%
+  NESTED_ARRAY_VARS         -        2        2       100%
+  RANGE_NESTED_ARRAY_STATIC   -      2        2       100%
+  RANGE_NESTED_ARRAY_VARS   -        2        2       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..124ab3bba6dc0b56ff61fea2cbdc4d9f9ef52a76
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.1.res.oracle
@@ -0,0 +1,53 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 28 goals scheduled
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_OK_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_KO_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_normal : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_OK_assigns : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_KO_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_normal : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_exit : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_normal : Unsuccess
+[wp] Proved goals:   24 / 28
+  Qed:            16 
+  Alt-Ergo:        8  (unsuccess: 4)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  NO_UNFOLD_OK_1            2        -        2       100%
+  NO_UNFOLD_OK_2            2        -        2       100%
+  NO_UNFOLD_OK_3            2        -        2       100%
+  NO_UNFOLD_KO              2        -        2       100%
+  USE_ASSIGN_UNFOLD_OK      2        1        3       100%
+  USE_ASSIGN_UNFOLD_KO      2        1        3       100%
+  ASSIGN_NO_UNFOLD_OK       1        -        1       100%
+  ASSIGN_NO_UNFOLD_KO       1        -        1       100%
+  PARTIAL_ASSIGNS_STATIC    -        2        2       100%
+  PARTIAL_ASSIGNS_VARS      -        2        2       100%
+  NESTED_ARRAY_STATIC       2        -        2       100%
+  NESTED_ARRAY_VARS         -        2        2       100%
+  RANGE_NESTED_ARRAY_STATIC   -      -        2       0.0%
+  RANGE_NESTED_ARRAY_VARS   -        -        2       0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a31c87f8d8dfa5dca2163c934886b178a4299730
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.2.res.oracle
@@ -0,0 +1,53 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 28 goals scheduled
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_OK_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_KO_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_normal : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_OK_assigns : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_KO_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_STATIC_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_STATIC_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_normal : Unsuccess
+[wp] Proved goals:   20 / 28
+  Qed:            14 
+  Alt-Ergo:        6  (unsuccess: 8)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  NO_UNFOLD_OK_1            2        -        2       100%
+  NO_UNFOLD_OK_2            2        -        2       100%
+  NO_UNFOLD_OK_3            2        -        2       100%
+  NO_UNFOLD_KO              2        -        2       100%
+  USE_ASSIGN_UNFOLD_OK      2        1        3       100%
+  USE_ASSIGN_UNFOLD_KO      2        1        3       100%
+  ASSIGN_NO_UNFOLD_OK       1        -        1       100%
+  ASSIGN_NO_UNFOLD_KO       1        -        1       100%
+  PARTIAL_ASSIGNS_STATIC    -        2        2       100%
+  PARTIAL_ASSIGNS_VARS      -        2        2       100%
+  NESTED_ARRAY_STATIC       -        -        2       0.0%
+  NESTED_ARRAY_VARS         -        -        2       0.0%
+  RANGE_NESTED_ARRAY_STATIC   -      -        2       0.0%
+  RANGE_NESTED_ARRAY_VARS   -        -        2       0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..32f7db5c4ff69fdade8bc819347b2c04b06f58a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unfold_assigns.res.oracle
@@ -0,0 +1,53 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/unfold_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 28 goals scheduled
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_1_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_2_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_OK_3_assigns_normal : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_NO_UNFOLD_KO_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_OK_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_OK_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_USE_ASSIGN_UNFOLD_KO_ensures : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_exit : Valid
+[wp] [Qed] Goal typed_USE_ASSIGN_UNFOLD_KO_assigns_normal : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_OK_assigns : Valid
+[wp] [Qed] Goal typed_ASSIGN_NO_UNFOLD_KO_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_PARTIAL_ASSIGNS_VARS_assigns_normal : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_exit : Valid
+[wp] [Qed] Goal typed_NESTED_ARRAY_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_NESTED_ARRAY_VARS_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_STATIC_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_RANGE_NESTED_ARRAY_VARS_assigns_normal : Valid
+[wp] Proved goals:   28 / 28
+  Qed:            16 
+  Alt-Ergo:       12
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  NO_UNFOLD_OK_1            2        -        2       100%
+  NO_UNFOLD_OK_2            2        -        2       100%
+  NO_UNFOLD_OK_3            2        -        2       100%
+  NO_UNFOLD_KO              2        -        2       100%
+  USE_ASSIGN_UNFOLD_OK      2        1        3       100%
+  USE_ASSIGN_UNFOLD_KO      2        1        3       100%
+  ASSIGN_NO_UNFOLD_OK       1        -        1       100%
+  ASSIGN_NO_UNFOLD_KO       1        -        1       100%
+  PARTIAL_ASSIGNS_STATIC    -        2        2       100%
+  PARTIAL_ASSIGNS_VARS      -        2        2       100%
+  NESTED_ARRAY_STATIC       2        -        2       100%
+  NESTED_ARRAY_VARS         -        2        2       100%
+  RANGE_NESTED_ARRAY_STATIC   -      2        2       100%
+  RANGE_NESTED_ARRAY_VARS   -        2        2       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
index 54ba848675c17ebfc2d7605e528b461568515c34..6da04abc8c6ea02b4cfa2ae5ab69a2f8067e17ec 100644
--- a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
+++ b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
@@ -1,10 +1,14 @@
 /* run.config
    OPT:
-   OPT: -wp-unfold-assigns
+   OPT: -wp-unfold-assigns -1
+   OPT: -wp-unfold-assigns 2
+   OPT: -wp-unfold-assigns 1
  */
 
 /* run.config_qualif
-   DONTRUN:
+   OPT: -wp-unfold-assigns -1
+   OPT: -wp-unfold-assigns 2
+   OPT: -wp-unfold-assigns 1
  */
 
 struct S { int a,b; };
@@ -64,3 +68,60 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) {
   struct S p = { 0,1 };
   *s = p ;
 }
+
+/*@ assigns *(p+(0..n)); */
+void f_assigns_range(int *p, unsigned n);
+
+/*@ assigns *(p+0), *(p+(1..3)), *(p+4); */
+void PARTIAL_ASSIGNS_STATIC(int *p) {
+  f_assigns_range(p, 4);
+}
+
+/*@ requires n > 4 ;
+    assigns *(p+0), *(p+(1..n-1)), *(p+n); */
+void PARTIAL_ASSIGNS_VARS(int *p, unsigned n) {
+  f_assigns_range(p, n);
+}
+
+struct With_array {
+  int x ;
+  int t [3] ;
+};
+
+//@ assigns *s ;
+void f_assigns_with_array(struct With_array* s);
+
+// FAILS AT UNFOLD LEVEL 1
+//@ assigns s->x, s->t[0], s->t[1..2] ;
+void NESTED_ARRAY_STATIC(struct With_array *s){
+  f_assigns_with_array(s);
+}
+
+// FAILS AT UNFOLD LEVEL 1
+/*@ requires n > 2 ;
+    assigns s->x, s->t[0], s->t[1..n] ; */
+void NESTED_ARRAY_VARS(struct With_array *s, unsigned n){
+  f_assigns_with_array(s);
+}
+
+//@ assigns *(s+(0..n)) ;
+void f_assigns_range_with_array(struct With_array* s, unsigned n);
+
+// FAILS AT UNFOLD LEVEL 2
+/*@ assigns s[0].x, s[0].t[0], s[0].t[1..2],
+            s[1].x, s[1].t[0..2],
+            s[2];
+*/
+void RANGE_NESTED_ARRAY_STATIC(struct With_array* s){
+  f_assigns_range_with_array(s, 2);
+}
+
+// FAILS AT UNFOLD LEVEL 2
+/*@ requires n > 2 && m > 3 ;
+    assigns s[0].x, s[0].t[0], s[0].t[1..m],
+            s[1].x, s[1].t[0..m],
+            s[2 .. n];
+*/
+void RANGE_NESTED_ARRAY_VARS(struct With_array* s, unsigned n, unsigned m){
+  f_assigns_range_with_array(s, n);
+}
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 233f8cb1f45c84386b52e41635e93dd28a1011da..d7b3d0fe369265d8c80a3aec067944bf8c16295a 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -415,9 +415,12 @@ module Split =
 
 let () = Parameter_customize.set_group wp_strategy
 module UnfoldAssigns =
-  False(struct
+  Int(struct
     let option_name = "-wp-unfold-assigns"
-    let help = "Unfold aggregates in assigns."
+    let default = 0
+    let arg_name = "n"
+    let help = "Unfold up to <n> levels of aggregates and arrays in assigns.\n\
+                Value -1 means unlimited depth (default 0)"
   end)
 
 let () = Parameter_customize.set_group wp_strategy
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index a276a4b4a33b01b914e6da3f7a18e9d1db89be1d..c8f5803dd2f37e3e59713d6786841327edcfe1fe 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -88,7 +88,7 @@ module Prenex: Parameter_sig.Bool
 module Ground: Parameter_sig.Bool
 module Reduce: Parameter_sig.Bool
 module ExtEqual : Parameter_sig.Bool
-module UnfoldAssigns : Parameter_sig.Bool
+module UnfoldAssigns : Parameter_sig.Int
 module Split: Parameter_sig.Bool
 module SplitMax: Parameter_sig.Int
 module SplitDepth: Parameter_sig.Int