diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 1b1979547e273dc830d327270dd7f025520da255..97c2f46154a2d50a2f3309666249b177e6056614 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -427,6 +427,34 @@ let fold_int ?(increasing=true) f t acc =
 let fold_enum f v acc =
   fold_int (fun x acc -> f (inject_singleton x) acc) v acc
 
+let to_seq ?(increasing=true) t =
+  if increasing then
+    match t.min, t.max with
+    | None, _ -> raise Error_Top
+    | Some l, None -> (* Infinite sequence *)
+      let rec aux i () =
+        Seq.Cons (i, aux (Integer.add i t.modu))
+      in aux l
+    | Some l, Some u ->
+      let rec aux i () =
+        if Integer.le i u
+        then Seq.Cons (i, aux (Integer.add i t.modu))
+        else Seq.Nil
+      in aux l
+  else
+    match t.min, t.max with
+    | _, None -> raise Error_Top
+    | None, Some u -> (* Infinite sequence *)
+      let rec aux i () =
+        Seq.Cons (i, aux (Integer.sub i t.modu))
+      in aux u
+    | Some l, Some u ->
+      let rec aux i () =
+        if Integer.ge i l
+        then Seq.Cons (i, aux (Integer.sub i t.modu))
+        else Seq.Nil
+      in aux u
+
 (* ------------------------------ Arithmetics ------------------------------- *)
 
 let opt_map2 f m1 m2 =
diff --git a/src/kernel_services/abstract_interp/int_interval.mli b/src/kernel_services/abstract_interp/int_interval.mli
index 1e52aa926a144e2311b8f68fc4ed9e86ab4e8da1..7277177b1a653de32c0433c0c710f0d046ac3d4a 100644
--- a/src/kernel_services/abstract_interp/int_interval.mli
+++ b/src/kernel_services/abstract_interp/int_interval.mli
@@ -98,3 +98,4 @@ val reduce_sign: t -> bool -> t or_bottom
 val reduce_bit: int -> t -> bool -> t or_bottom
 
 val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
+val to_seq: ?increasing:bool -> t -> Integer.t Seq.t
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 69bf59a6a0284764997b8876a959acdfb4f02a99..8ef4bf0d01229a912a4b6ca40b7c9167776b04c4 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -199,6 +199,20 @@ let mem v a =
   in
   c 0
 
+let to_seq ?(increasing=true) =
+  if increasing
+  then Array.to_seq
+  else
+    fun a ->
+      let rec aux i () =
+        if i >= 0
+        then
+          let x = Array.unsafe_get a i in
+          Seq.Cons (x, aux (i-1))
+        else Seq.Nil
+      in
+      aux (Array.length a -1)
+
 (* ------------------------------- Set or top ------------------------------- *)
 
 type set_or_top = [ `Set of t | `Top of Integer.t * Integer.t * Integer.t ]
diff --git a/src/kernel_services/abstract_interp/int_set.mli b/src/kernel_services/abstract_interp/int_set.mli
index 979dfbe883a48f9d001ff300c38acfe361cec076..6dc3a3b892debaee961bd5ecda636963f96d66a8 100644
--- a/src/kernel_services/abstract_interp/int_set.mli
+++ b/src/kernel_services/abstract_interp/int_set.mli
@@ -85,6 +85,7 @@ val fold: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
 val map: (Integer.t -> Integer.t) -> t -> t
 val filter: (Integer.t -> bool) -> t -> t or_bottom
 val map_reduce: (Integer.t -> 'a) -> ('a -> 'a -> 'a) -> t -> 'a
+val to_seq: ?increasing:bool -> t -> Integer.t Seq.t
 
 (** Sets whose cardinal exceeds a certain limit must be converted into
     intervals. Functions that make sets grow returns either a set small enough,
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index be2348def1b411777fe9b050fad0d991ec950611..7ea8bcd89c1c76d67b90fd84f274d5b4290523c3 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -221,6 +221,10 @@ let fold_int ?(increasing=true) f v acc =
 
 let fold_enum f v acc = fold_int (fun x acc -> f (inject_singleton x) acc) v acc
 
+let to_seq ?(increasing=true) = function
+  | Itv i -> Int_interval.to_seq ~increasing i
+  | Set s -> Int_set.to_seq ~increasing s
+
 (* -------------------------------- Accessors ------------------------------- *)
 
 let min_int = function
diff --git a/src/kernel_services/abstract_interp/int_val.mli b/src/kernel_services/abstract_interp/int_val.mli
index 807fab7bfdd27d49926ef5c030bf4f1a14f88af3..e750ceec9d0d719da7dbc60d45e8d46f15888c95 100644
--- a/src/kernel_services/abstract_interp/int_val.mli
+++ b/src/kernel_services/abstract_interp/int_val.mli
@@ -189,3 +189,9 @@ val complement_under: size:int -> signed:bool -> t -> t or_bottom
     by default. If [increasing] is set to false, iterate by decreasing order.
     @raise Abstract_interp.Error_Top if the abstraction is unbounded. *)
 val fold_int: ?increasing:bool -> (Integer.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+(** Builds a sequence of all integers represented by an abstraction, in
+    increasing order (resp. decreasing order if [increasing is set to false])
+    @raise Abstract_interp.Error_Top if the abstraction has no lower bound
+    (resp. no upper bound) *)
+val to_seq: ?increasing:bool -> t -> Integer.t Seq.t
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 2ff6f24df697f122f27a031ceb72af5d645c87a0..bc5105154287b8a167675d366f86e106daf4f65e 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -418,6 +418,12 @@ let fold_enum f v acc =
   | Float _ -> raise Error_Top
   | Int _ -> fold_int (fun x acc -> f (inject_singleton x) acc) v acc
 
+let to_int_seq v =
+  match v with
+  | Bottom -> Seq.empty
+  | Float _ -> raise Error_Top
+  | Int i -> Int_val.to_seq i
+
 let is_included t1 t2 =
   (t1 == t2) ||
   match t1, t2 with
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index 4323fd006c445e69ab7770f5aa2699219d473dfe..edec2e8cecc71049687bcd9e47ce5493a260251d 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -215,6 +215,11 @@ val fold_int_bounds: (t -> 'a -> 'a) -> t -> 'a -> 'a
     [max] are infinite, [f] is called with an argument [i'] unreduced
     in the corresponding direction(s). *)
 
+val to_int_seq: t -> Integer.t Seq.t
+(** Builds a sequence of integer values of the ival in increasing order. The
+    Raise {!Abstract_interp.Error_Top} if the argument is a float or a
+    potentially infinite integer. *)
+
 (** Subdivisions into two intervals *)
 val subdivide: size:Integer.t -> t -> t * t
 
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 0a16b809c69db96209c84ba1bff1d55e61f109c4..b172766a335f9d1a31adabf8fce85dab19511d88 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -95,7 +95,9 @@ module Location_Bytes = struct
     | Top _ -> raise Error_Top
     | Map m -> MapLattice.fold f m acc
   let fold_topset_ok = fold
-
+  let to_seq_i = function
+    | Top _ -> raise Error_Top
+    | Map m -> MapLattice.to_seq m
   let inject_ival i = inject Base.null i
 
   let inject_float f =
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index 00b3749be4659ae9db24070e426659bc486485d3..bcb7f17f367e4e2e0d641384b6a210ed5ca37401 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -145,6 +145,8 @@ module Location_Bytes : sig
       presented to [f]. Raises {!Error_Top} if [loc] is [Top _] or if
       one offset cannot be enumerated. *)
 
+  val to_seq_i : t -> (Base.t * Ival.t) Seq.t
+
   val cached_fold:
     cache_name:string ->
     temporary:bool ->
diff --git a/src/libraries/stdlib/transitioning.ml b/src/libraries/stdlib/transitioning.ml
index f11d88cb8a4a5ae5b86380cc0a7b66bb6f418b58..ba4203fb98deeb9b1d4b1fe8753fd8564e52cc6b 100644
--- a/src/libraries/stdlib/transitioning.ml
+++ b/src/libraries/stdlib/transitioning.ml
@@ -56,4 +56,38 @@ module Seq = struct
 
   let unzip seq =
     map fst seq, map snd seq
+
+  let rec append xs ys () =
+    match xs () with
+    | Nil -> ys ()
+    | Cons (x, xt) -> Cons (x, append xt ys)
+
+  let take n xs =
+    if n < 0 then invalid_arg "Seq.take";
+    let rec aux n xs =
+      if n = 0
+      then empty
+      else fun () ->
+        match xs () with
+        | Nil -> Nil
+        | Cons (x, xs) -> Cons (x, aux (n-1) xs)
+    in
+    aux n xs
+
+  let drop n xs =
+    if n < 0
+    then invalid_arg "Seq.drop"
+    else if n = 0
+    then xs
+    else
+      let rec aux n xs =
+        match xs () with
+        | Nil -> Nil
+        | Cons (_, xs) ->
+          let n = n - 1 in
+          if n = 0
+          then xs ()
+          else aux n xs
+      in
+      fun () -> aux n xs
 end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index be40531442b3ef2af3bbd28f313dd78beea4a80e..eff4a5548f621e20e40a606d6cfaaacf557a619f 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -44,9 +44,20 @@ module List: sig
 end
 
 module Seq: sig
+  open Stdlib.Seq
+
+  (** since 4.14.0 *)
+  val mapi: (int -> 'a -> 'b) -> 'a t -> 'b t
+
+  (** since 4.14.0 *)
+  val unzip : ('a * 'b) t -> 'a t * 'b t
+
+  (** since 4.11.0 *)
+  val append : 'a t -> 'a t -> 'a t
+
   (** since 4.14.0 *)
-  val mapi: (int -> 'a -> 'b) -> 'a Seq.t -> 'b Seq.t
+  val take : int -> 'a t -> 'a t
 
   (** since 4.14.0 *)
-  val unzip : ('a * 'b) Seq.t -> 'a Seq.t * 'b Seq.t
+  val drop : int -> 'a t -> 'a t
 end
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 6a722557d67e9a3fc127bc5cc0249e7da5158051..15622103b2b1eb7dffe642f3b5f38e8bae4f9c60 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -338,6 +338,13 @@ module Shape(Key: Id_Datatype) = struct
     | Branch (_, _, tree0, tree1, _) ->
       fold_rev f tree0 (fold_rev f tree1 accu)
 
+  let rec to_seq m () =
+    match m with
+    | Empty -> Seq.Nil
+    | Leaf (key, data, _) -> Seq.Cons ((key, data), Seq.empty)
+    | Branch (_, _, tree0, tree1, _) ->
+      Transitioning.Seq.append (to_seq tree0) (to_seq tree1) ()
+
   (* This reference will contain a list of functions that will clear
      all the transient caches used in this module *)
   let clear_caches_ref = ref []
diff --git a/src/libraries/utils/hptmap_sig.ml b/src/libraries/utils/hptmap_sig.ml
index f1937bb3a9f822f6c297c571f19a2cec250dc795..b75c35b4be657ae35d58a2a021f5f399e61ef0f7 100644
--- a/src/libraries/utils/hptmap_sig.ml
+++ b/src/libraries/utils/hptmap_sig.ml
@@ -112,6 +112,11 @@ module type Shape = sig
   (** [fold_rev] performs exactly the same job as [fold], but presents keys
       to [f] in the opposite order. *)
 
+  val to_seq : 'v map -> (key * 'v) Seq.t
+  (** [to_seq m] builds a sequence of each pair of key and datume in the
+      map [m]. Keys are presented in the sequence in increasing order according
+      to the map's ordering. *)
+
   val cached_fold :
     cache_name:string ->
     temporary:bool ->
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 078d015efca2d002e5cdbf5416ddb2b56934db29..993c989e2d446545caec4aa8b57676cb655abb22 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -24,50 +24,49 @@ open Cil_types
 open Dive_types
 
 module Graph = Dive_graph
+module Seq =
+struct
+  include Stdlib.Seq
+  include Transitioning.Seq
+end
 
 let dkey = Self.register_category "build"
 
-(* --- Utility function --- *)
-
-(* Breaks a list at n-th element into two sublists *)
-let rec list_break n l =
-  if n <= 0 then ([], l)
-  else match l with
-    | [] -> ([], [])
-    | a :: l ->
-      let l1, l2 = list_break (n - 1) l in
-      (a :: l1, l2)
-
 
 (* --- Lval enumeration --- *)
 
-module IterLval =
+module EnumLvals =
 struct
-  let visitor f =
+  let visitor () =
     object
       inherit Visitor.frama_c_inplace
-      method! vlval lval = f lval; Cil.SkipChildren
+      val mutable acc = []
+      method get_acc = acc
+      method! vlval lval = acc <- lval :: acc; Cil.SkipChildren
     end
 
-  let from_exp f exp =
-    ignore (Visitor.visitFramacExpr (visitor f) exp)
+  let in_exp exp =
+    let vis = visitor () in
+    ignore (Visitor.visitFramacExpr (vis :> Visitor.frama_c_inplace) exp);
+    List.rev vis#get_acc
 
-  let from_init f vi init =
-    ignore (Visitor.visitFramacInit (visitor f) vi NoOffset init)
+  let in_init vi init =
+    let vis = visitor () in
+    ignore (Visitor.visitFramacInit (vis :> Visitor.frama_c_inplace) vi NoOffset init);
+    List.rev vis#get_acc
 
-  let from_alarm f = function
+  let in_alarm = function
     | Alarms.Division_by_zero e | Index_out_of_bound (e, _) | Invalid_shift (e,_)
     | Overflow (_,e,_,_) | Float_to_int (e,_,_) | Is_nan_or_infinite (e,_)
     | Is_nan (e,_) | Function_pointer (e,_) | Invalid_pointer e ->
-      from_exp f e
+      in_exp e
     | Pointer_comparison (opt_e1,e2) ->
-      Option.iter (from_exp f) opt_e1;
-      from_exp f e2
+      Option.fold ~none:[] ~some:in_exp opt_e1 @ in_exp e2
     | Differing_blocks (e1,e2) ->
-      from_exp f e1; from_exp f e2
+      in_exp e1 @ in_exp e2
     | Memory_access _ | Not_separated _ | Overlap _
-    | Uninitialized _ | Dangling _ | Uninitialized_union _ -> ()
-    | Invalid_bool lv -> f lv
+    | Uninitialized _ | Dangling _ | Uninitialized_union _ -> []
+    | Invalid_bool lv -> [lv]
 end
 
 
@@ -113,21 +112,15 @@ struct
     Self.debug ~dkey "%d found" (List.length reads);
     reads
 
-  let does_cil_read_zone iter stmt cil zone =
-    let intersects lval =
-      let zone' = to_zone (Kstmt stmt) lval in
-      Locations.Zone.intersects zone' zone
-    in
-    try iter (fun lval -> if intersects lval then raise Exit) cil; false
-    with Exit -> true
+  let does_lval_read_zone zone stmt lval =
+    let zone' = to_zone (Kstmt stmt) lval in
+    Locations.Zone.intersects zone' zone
 
-  let does_exp_read_zone stmt exp zone =
-    does_cil_read_zone IterLval.from_exp stmt exp zone
+  let does_exp_read_zone zone stmt exp =
+    List.exists (does_lval_read_zone zone stmt) (EnumLvals.in_exp exp)
 
-  let does_init_read_zone stmt vi init zone =
-    does_cil_read_zone
-      (fun f init -> IterLval.from_init f vi init)
-      stmt init zone
+  let does_init_read_zone zone stmt vi init  =
+    List.exists (does_lval_read_zone zone stmt) (EnumLvals.in_init vi init)
 end
 
 
@@ -152,45 +145,37 @@ let is_foldable_type typ =
   | TNamed _ -> assert false (* the type have been unrolled *)
 
 
-exception Too_many_deps of node_kind list
-exception Unknown_location
-
-let enumerate_cells ~is_folded_base ~limit lval kinstr =
+let enumerate_cells ~is_folded_base lval kinstr =
   (* If possible, refine the lval to a non-symbolic one *)
   let typ = Cil.typeOfLval lval in
   let location = Eval.to_location kinstr lval in
   let open Locations in
-  let add (acc,count) node_kind =
-    if count >= limit then
-      raise (Too_many_deps acc);
-    (node_kind :: acc, count+1)
-  in
-  let add_base base ival (acc,count) =
+  let map_base (base,ival) =
     match base with
     | Base.Var (vi,_) | Allocated (vi,_,_) ->
       begin
         if is_foldable_type vi.vtype && is_folded_base vi then
-          add (acc,count) (Composite (vi))
+          Seq.return (Composite (vi))
         else
-          let add_cell offset (acc,count) =
+          let map_offset offset =
             let matching = Bit_utils.MatchType typ in
             let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in
-            let node_kind = Scalar (vi, typ, offset') in
-            add (acc,count) node_kind
+            Scalar (vi, typ, offset')
           in
           try
-            Ival.fold_int add_cell ival (acc,count)
+            Ival.to_int_seq ival |> Seq.map map_offset
           with Abstract_interp.Error_Top | Bit_utils.NoMatchingOffset ->
             (* fallback to composite node *)
-            add (acc,count) (Composite (vi))
+            Seq.return (Composite (vi))
       end
-    | CLogic_Var _ -> add (acc,count) (Error "logic variables not supported")
-    | Null -> add (acc,count) AbsoluteMemory
-    | String (i,cs) -> add (acc,count) (String (i, cs))
+    | CLogic_Var _ -> Seq.return (Error "logic variables not supported")
+    | Null -> Seq.return AbsoluteMemory
+    | String (i,cs) -> Seq.return (String (i, cs))
   in
   try
-    fst (Location_Bits.fold_i add_base location.loc ([],0))
-  with Abstract_interp.Error_Top -> raise Unknown_location
+    Location_Bits.to_seq_i location.loc |> Seq.flat_map map_base
+  with Abstract_interp.Error_Top ->
+    Seq.return (Unknown (lval, kinstr))
 
 let build_node_kind ~is_folded_base lval kinstr =
   match lval with
@@ -198,12 +183,11 @@ let build_node_kind ~is_folded_base lval kinstr =
     (* Build a scalar node even if kinstr is dead *)
     Scalar (vi, Cil.typeOfLval lval, offset)
   | Mem _, _ ->
-    match enumerate_cells ~is_folded_base ~limit:1 lval kinstr with
+    match
+      enumerate_cells ~is_folded_base lval kinstr |> Seq.take 2 |> List.of_seq
+    with
     | [node_kind] -> node_kind
-    | [] (* happens if kinstr is dead code *) -> Scattered (lval, kinstr)
-    | _ -> assert false
-    | exception (Too_many_deps _) -> Scattered (lval, kinstr)
-    | exception Unknown_location -> Unknown (lval, kinstr)
+    | _ -> Scattered (lval, kinstr)
 
 let default_node_locality callstack =
   match callstack with
@@ -257,23 +241,6 @@ let build_node context callstack lval kinstr =
   let node_kind = build_node_kind ~is_folded_base lval kinstr in
   add_or_update_node context callstack node_kind
 
-let build_all_scattered_node ~limit context callstack kinstr lval =
-  let is_folded_base = Context.is_folded context in
-  let cells, complete =
-    try
-      enumerate_cells ~is_folded_base ~limit lval kinstr, true
-    with Too_many_deps cells -> cells, false
-  in
-  let add node_kind =
-    let node = add_or_update_node context callstack node_kind in
-    begin match Node_kind.to_lval node_kind with
-      | Some lval' -> update_node_values node kinstr lval';
-      | _ -> ()
-    end;
-    node
-  in
-  List.map add cells, complete
-
 let build_var context callstack varinfo =
   let lval = Var varinfo, NoOffset in
   build_node context callstack lval Kglobal
@@ -291,32 +258,30 @@ let build_alarm context callstack stmt alarm =
 
 (* --- Writes --- *)
 
+type deps_builder = unit Seq.t
+
 let build_node_writes context node =
   let graph = Context.get_graph context
-  and max_dep_fetch_count = Context.get_max_dep_fetch_count context in
-
-  let rec build_write_deps callstack kinstr lval =
-    let writes = match node.node_writes_computation with
-      | Done -> []
-      | Partial writes -> writes
-      | NotDone ->
-        let writes = Eval.writes kinstr lval in
-        node.node_writes_stmts <- writes @ build_arg_deps callstack;
-        writes
-    and add_deps = function
+  and is_folded_base = Context.is_folded context in
+
+  let rec build_write_deps callstack kinstr lval : deps_builder =
+    let add_deps = function
       | { skind=Instr instr } as stmt ->
-        let callstacks = find_compatible_callstacks stmt callstack in
-        List.iter (fun cs -> build_instr_deps cs stmt instr) callstacks
+        List.to_seq (find_compatible_callstacks stmt callstack) |>
+        Seq.flat_map (fun cs -> build_instr_deps cs stmt instr)
       | _ -> assert false (* Studia invariant *)
     in
-    let sub,rest = list_break max_dep_fetch_count writes in
-    List.iter add_deps sub;
-    if rest = [] then Done else Partial rest
+    let writes = Eval.writes kinstr lval in
+    let args_seq, callee_stmts = build_arg_deps callstack in
+    let compare = Cil_datatype.Stmt_Id.compare in
+    node.node_writes_stmts <- List.sort_uniq compare (writes @ callee_stmts);
+    Seq.append args_seq (Seq.flat_map add_deps (List.to_seq writes))
 
-  and build_alarm_deps callstack stmt alarm =
-    IterLval.from_alarm (build_lval_deps callstack stmt Data) alarm
+  and build_alarm_deps callstack stmt alarm : deps_builder =
+    List.to_seq (EnumLvals.in_alarm alarm) |>
+    Seq.flat_map (build_lval_deps callstack stmt Data)
 
-  and build_instr_deps callstack stmt = function
+  and build_instr_deps callstack stmt : Cil_types.instr -> deps_builder = function
     | Set (_, exp, _) ->
       build_exp_deps callstack stmt Data exp
     | Call (_, callee, args, _) ->
@@ -327,10 +292,11 @@ let build_node_writes context node =
       in
       Cil.treat_constructor_as_func as_func dest f args k loc
     | Local_init (vi, AssignInit init, _)  ->
-      IterLval.from_init (build_lval_deps callstack stmt Data) vi init
-    | Asm _ | Skip _ | Code_annot _ -> () (* Cases not returned by Studia *)
+      List.to_seq (EnumLvals.in_init vi init) |>
+      Seq.flat_map (build_lval_deps callstack stmt Data)
+    | Asm _ | Skip _ | Code_annot _ -> Seq.empty (* Cases not returned by Studia *)
 
-  and build_arg_deps callstack =
+  and build_arg_deps callstack : deps_builder * stmt list =
     match Node_kind.get_base node.node_kind with
     (* TODO refine formal dependency computation for non-scalar formals *)
     | Some vi when vi.vformal ->
@@ -344,145 +310,135 @@ let build_node_writes context node =
         | None ->
           let callsites = Kernel_function.find_syntactic_callsites kf in
           List.map (fun (kf,stmt) -> (stmt,Callstack.init kf)) callsites
-      and add_deps (stmt,callstack) =
+      and add_deps (stmt,callstack) : unit Seq.t =
         match stmt.skind with
-        | Instr (Call (_,_,args,_))
-        | Instr (Local_init (_, ConsInit (_, args, _), _)) ->
+        | Instr
+            (Call (_,_,args,_) |
+             (Local_init (_, ConsInit (_, args, _), _))) ->
           let exp = List.nth args pos in
           build_exp_deps callstack stmt Data exp
         | _ ->
           assert false (* Callsites can only be Call or ConsInit *)
       in
-      List.iter add_deps callsites;
-      List.map fst callsites
-    | _ -> []
+      Seq.flat_map add_deps (List.to_seq callsites), List.map fst callsites
+    | _ -> Seq.empty, []
 
-  and build_return_deps callstack stmt args kf =
+  and build_return_deps callstack stmt args kf : deps_builder =
     match Kernel_function.find_return kf with
     | {skind = Return (Some {enode = Lval lval_res},_)} as return_stmt ->
       let callstack = Callstack.push (kf,stmt) callstack in
       build_lval_deps callstack return_stmt Data lval_res
-    | {skind = Return (None, _)} -> () (* return void *)
+    | {skind = Return (None, _)} -> Seq.empty (* return void *)
     | _ -> assert false (* Cil invariant *)
     | exception Kernel_function.No_Statement ->
       (* the function is only a prototype *)
       (* TODO: read assigns instead *)
-      List.iter (build_exp_deps callstack stmt Data) args
+      List.to_seq args |>
+      Seq.flat_map (build_exp_deps callstack stmt Data)
 
-  and build_call_deps callstack stmt callee args =
-    begin match callee.enode with
-      | Lval (Var _vi, _offset) -> ()
+  and build_call_deps callstack stmt callee args : deps_builder =
+    let callee_deps = match callee.enode with
+      | Lval (Var _vi, _offset) -> Seq.empty
       | Lval (Mem exp, _offset) ->
         build_exp_deps callstack stmt Callee exp
       | _ ->
         Self.warning "Cannot compute all callee dependencies for %a"
           Cil_printer.pp_stmt stmt;
-    end;
-    let l = Eval.to_kf_list (Kstmt stmt) callee in
-    List.iter (build_return_deps callstack stmt args) l
+        Seq.empty
+    and return_deps =
+      List.to_seq (Eval.to_kf_list (Kstmt stmt) callee) |>
+      Seq.flat_map (build_return_deps callstack stmt args)
+    in
+    Seq.append callee_deps return_deps
 
-  and build_exp_deps callstack stmt kind exp =
-    IterLval.from_exp (build_lval_deps callstack stmt kind) exp
+  and build_exp_deps callstack stmt kind exp : deps_builder =
+    List.to_seq (EnumLvals.in_exp exp) |>
+    Seq.flat_map (build_lval_deps callstack stmt kind)
 
-  and build_lval_deps callstack stmt kind lval =
+  and build_lval_deps callstack stmt kind lval : deps_builder =
     let kinstr = Kstmt stmt in
     let dst = build_lval context callstack kinstr lval in
-    Graph.create_dependency graph kinstr dst kind node
-
-  and build_scattered_deps callstack kinstr lval =
-    let succ_count = List.length (Graph.pred graph node) in
-    let limit = succ_count + max_dep_fetch_count in
-    let nodes, complete =
-      build_all_scattered_node ~limit context callstack kinstr lval
+    Seq.return (Graph.create_dependency graph kinstr dst kind node)
+
+  and build_scattered_deps callstack kinstr lval : deps_builder =
+    let add_cell node_kind =
+      let node' = add_or_update_node context callstack node_kind in
+      begin match Node_kind.to_lval node_kind with
+        | Some lval' -> update_node_values node kinstr lval';
+        | _ -> ()
+      end;
+      Graph.create_dependency graph kinstr node' Composition node
     in
-    let kind = Composition in
-    let add_dep dst =
-      Graph.create_dependency graph kinstr dst kind node
-    in
-    List.iter add_dep nodes;
-    if complete then Done else Partial []
-
+    enumerate_cells ~is_folded_base lval kinstr |> Seq.map add_cell
   in
+
   let callstack = node.node_locality.loc_callstack in
-  let writes_computation =
-    match node.node_kind with
-    | Scalar (vi,_typ,offset) ->
-      build_write_deps callstack Kglobal (Cil_types.Var vi, offset)
-    | Composite (vi) ->
-      build_write_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
-    | Scattered (lval,kinstr) ->
-      build_scattered_deps callstack kinstr lval
-    | Alarm (stmt,alarm) ->
-      build_alarm_deps callstack stmt alarm;
-      Done
-    | Unknown _ | AbsoluteMemory | String _ | Error _ ->
-      Done
-  in
-  node.node_writes_computation <- writes_computation;
-  let compare_stmt = Cil_datatype.Stmt_Id.compare in
-  node.node_writes_stmts <- List.sort compare_stmt node.node_writes_stmts;
-  Context.update_diff context node
+  match node.node_kind with
+  | Scalar (vi,_typ,offset) ->
+    build_write_deps callstack Kglobal (Cil_types.Var vi, offset)
+  | Composite (vi) ->
+    build_write_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
+  | Scattered (lval,kinstr) ->
+    build_scattered_deps callstack kinstr lval
+  | Alarm (stmt,alarm) ->
+    build_alarm_deps callstack stmt alarm
+  | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+    Seq.empty
 
 
 (* --- Reads --- *)
 
 let build_node_reads context node =
-  let graph = Context.get_graph context
-  and max_dep_fetch_count = Context.get_max_dep_fetch_count context in
-
-  let rec build_reads_deps callstack kinstr lval =
-    let reads = match node.node_reads_computation with
-      | Done -> []
-      | Partial reads -> reads
-      | NotDone -> Eval.reads kinstr lval
-    and add_deps stmt =
+  let graph = Context.get_graph context in
+
+  let rec build_reads_deps callstack kinstr lval : deps_builder =
+    let add_deps stmt =
       let zone = Some (Eval.to_zone kinstr lval) in
-      let callstacks = find_compatible_callstacks stmt callstack in
-      List.iter (fun cs -> build_stmt_deps cs zone stmt) callstacks
+      List.to_seq (find_compatible_callstacks stmt callstack) |>
+      Seq.flat_map (fun cs -> build_stmt_deps cs zone stmt)
     in
-    let sub,rest = list_break max_dep_fetch_count reads in
-    List.iter add_deps sub;
-    if rest = [] then Done else Partial rest
+    List.to_seq (Eval.reads kinstr lval) |>
+    Seq.flat_map add_deps
 
   and exp_contains_read zone stmt exp =
     match zone with
     | None -> true
     | Some zone' ->
-      Eval.does_exp_read_zone stmt exp zone'
+      Eval.does_exp_read_zone zone' stmt exp
 
   and init_contains_read zone stmt vi init =
     match zone with
     | None -> true
     | Some zone' ->
-      Eval.does_init_read_zone stmt vi init zone'
+      Eval.does_init_read_zone zone' stmt vi init
 
   and build_kinstr_deps callstack zone = function
-    | Kglobal -> () (* Do nothing *)
+    | Kglobal -> Seq.empty (* Do nothing *)
     | Kstmt stmt -> build_stmt_deps callstack zone stmt
 
   and build_stmt_deps callstack zone stmt =
     match stmt.skind with
     | Instr instr -> build_instr_deps callstack zone stmt instr
-    | Return (Some exp,_) ->
-      if exp_contains_read zone stmt exp then
-        build_return_deps callstack stmt
-    | _ -> ()
+    | Return (Some exp,_)
+      when exp_contains_read zone stmt exp ->
+      build_return_deps callstack stmt
+    | _ -> Seq.empty
 
   and build_instr_deps callstack zone stmt = function
-    | Set (lval, exp, _) ->
-      if exp_contains_read zone stmt exp then
-        build_lval_deps callstack stmt lval
+    | Set (lval, exp, _)
+      when exp_contains_read zone stmt exp ->
+      build_lval_deps callstack stmt lval
     | Local_init (dest, ConsInit (f, args, k), loc) ->
       let as_func _dest callee args _loc =
         build_call_deps callstack zone stmt callee args
       in
       Cil.treat_constructor_as_func as_func dest f args k loc
-    | Local_init (vi, AssignInit init, _)  ->
-      if init_contains_read zone stmt vi init then
-        build_var_deps callstack stmt vi
+    | Local_init (vi, AssignInit init, _)
+      when init_contains_read zone stmt vi init ->
+      build_var_deps callstack stmt vi
     | Call (_, callee, args, _) ->
       build_call_deps callstack zone stmt callee args
-    | _ -> ()
+    | _ -> Seq.empty
 
   and build_return_deps callstack stmt =
     let kf = Kernel_function.find_englobing_kf stmt in
@@ -496,7 +452,7 @@ let build_node_reads context node =
         List.map (fun (kf,stmt) -> (stmt,Callstack.init kf)) callsites
     and add_deps (stmt,callstack) =
       match stmt.skind with
-      | Instr (Call (None,_,_,_)) -> ()
+      | Instr (Call (None,_,_,_)) -> Seq.empty
       | Instr (Call (Some lval,_,_,_)) ->
         build_lval_deps callstack stmt lval
       | Instr (Local_init (vi,_,_)) ->
@@ -504,11 +460,11 @@ let build_node_reads context node =
       | _ ->
         assert false (* Callsites can only be Call or ConsInit *)
     in
-    List.iter add_deps callsites;
+    Seq.flat_map add_deps (List.to_seq callsites);
 
   and build_call_deps callstack zone stmt callee args =
-    let l = Eval.to_kf_list (Kstmt stmt) callee in
-    List.iter (build_args_deps callstack zone stmt args) l
+    List.to_seq (Eval.to_kf_list (Kstmt stmt) callee) |>
+    Seq.flat_map (build_args_deps callstack zone stmt args)
 
   and build_args_deps callstack zone stmt args callee_kf =
     let callstack = Callstack.push (callee_kf,stmt) callstack in
@@ -516,36 +472,33 @@ let build_node_reads context node =
     (* For Frama_C_show_each and functions called through pointers, there may
        be more arguments than formal parameters declared. *)
     let used_args = Extlib.list_first_n (List.length formals) args in
-    List.iter2 (build_arg_dep callstack stmt zone) used_args formals
+    List.to_seq (List.combine used_args formals) |>
+    Seq.flat_map (build_arg_dep callstack stmt zone)
 
-  and build_arg_dep callstack stmt zone arg formal =
-    if exp_contains_read zone stmt arg then
-      build_var_deps callstack stmt formal
+  and build_arg_dep callstack stmt zone (arg,formal) =
+    if exp_contains_read zone stmt arg
+    then build_var_deps callstack stmt formal
+    else Seq.empty
 
   and build_lval_deps callstack stmt lval =
     let kinstr = Kstmt stmt in
     let src = build_lval context callstack kinstr lval in
-    Graph.create_dependency graph kinstr node Data src
+    Seq.return (Graph.create_dependency graph kinstr node Data src)
 
   and build_var_deps callstack stmt vi =
     build_lval_deps callstack stmt (Cil.var vi)
 
   in
   let callstack = node.node_locality.loc_callstack in
-  let reads_computation =
-    match node.node_kind with
-    | Scalar (vi,_typ,offset) ->
-      build_reads_deps callstack Kglobal (Cil_types.Var vi, offset)
-    | Composite (vi) ->
-      build_reads_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
-    | Scattered (_lval,kinstr) ->
-      build_kinstr_deps callstack None kinstr;
-      Done
-    | Alarm _ | Unknown _ | AbsoluteMemory | String _ | Error _ ->
-      Done
-  in
-  node.node_reads_computation <- reads_computation;
-  Context.update_diff context node
+  match node.node_kind with
+  | Scalar (vi,_typ,offset) ->
+    build_reads_deps callstack Kglobal (Cil_types.Var vi, offset)
+  | Composite (vi) ->
+    build_reads_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
+  | Scattered (_lval,kinstr) ->
+    build_kinstr_deps callstack None kinstr
+  | Alarm _ | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+    Seq.empty
 
 
 (* --- Exploration --- *)
@@ -569,19 +522,41 @@ let bfs ~depth ~iter_succ f root =
     end
   done
 
+let advance_computation context seq =
+  let n = Context.get_max_dep_fetch_count context in
+  match Seq.drop n seq () with
+  | Seq.Nil -> Done
+  | node -> Partial (fun () -> node)
+
 let explore_backward ~depth context root =
   let iter_succ f n = Graph.iter_pred f (Context.get_graph context) n
   and explore_node n =
-    if n.node_writes_computation <> Done && should_explore n root then
-      build_node_writes context n
+    if n.node_writes_computation <> Done && should_explore n root then begin
+      let deps_builder =
+        match n.node_writes_computation with
+        | Done -> Seq.empty
+        | Partial builder -> builder
+        | NotDone -> build_node_writes context n
+      in
+      n.node_writes_computation <- advance_computation context deps_builder;
+      Context.update_diff context n
+    end
   in
   bfs ~depth ~iter_succ explore_node root
 
 let explore_forward ~depth context root =
   let iter_succ f n = Graph.iter_succ f (Context.get_graph context) n
   and explore_node n =
-    if n.node_reads_computation <> Done && should_explore n root then
-      build_node_reads context n;
+    if n.node_reads_computation <> Done && should_explore n root then begin
+      let deps_builder =
+        match n.node_writes_computation with
+        | Done -> Seq.empty
+        | Partial builder -> builder
+        | NotDone -> build_node_reads context n
+      in
+      n.node_reads_computation <- advance_computation context deps_builder;
+      Context.update_diff context n
+    end
   in
   bfs ~depth ~iter_succ explore_node root
 
diff --git a/src/plugins/dive/dive_types.ml b/src/plugins/dive/dive_types.ml
index 0028b31669b8fb4dc21178dc31b8897add8f4406..56a623226171794d9aa9e00bf4318d98e70c407e 100644
--- a/src/plugins/dive/dive_types.ml
+++ b/src/plugins/dive/dive_types.ml
@@ -43,7 +43,7 @@ type node_range =
   | Normal of int (* From 0 = almost singleton to 100 = almost all possible values *)
   | Wide (* Too many values for the type to be reasonable *)
 
-type 'a computation = NotDone | Partial of 'a | Done
+type computation = NotDone | Partial of (unit Seq.t) | Done
 
 type node = {
   node_key : int;
@@ -53,8 +53,8 @@ type node = {
   mutable node_hidden : bool;
   mutable node_values : Cvalue.V.t option;
   mutable node_range : node_range;
-  mutable node_writes_computation : (Cil_types.stmt list) computation;
-  mutable node_reads_computation : (Cil_types.stmt list) computation;
+  mutable node_writes_computation : computation;
+  mutable node_reads_computation : computation;
   mutable node_writes_stmts : Cil_types.stmt list;
 }
 
diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot
index 90a8124631ff921f59bdd6cc81ff903c1fa9a842..bcffeba804e729b864d5f0dfae03c06f4e6adf63 100644
--- a/src/plugins/dive/tests/dive/oracle/manydeps.dot
+++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot
@@ -11,23 +11,13 @@ digraph G {
         style="filled", ];
   cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
         style="filled", ];
-  cp14 [label=<t1>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp16 [label=<t9>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp18 [label=<t8>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp20 [label=<t7>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp22 [label=<t6>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
-        style="filled", ];
-  cp24 [label=<__retres>, shape=box, style="bold", ];
-  cp25 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
+  cp14 [label=<__retres>, shape=box, style="bold", ];
+  cp15 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
         color="#88AAFF", style="filled,dotted", ];
   
-  subgraph cluster_cs_1 { label=<many_writes>; cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;cp2;
+  subgraph cluster_cs_1 { label=<many_writes>; cp12;cp10;cp8;cp6;cp4;cp2;
      };
-  subgraph cluster_cs_2 { label=<many_values>; cp25;cp24;
+  subgraph cluster_cs_2 { label=<many_values>; cp15;cp14;
      };
   
   cp2 -> cp2 [style="bold", ];
@@ -36,11 +26,6 @@ digraph G {
   cp8 -> cp2;
   cp10 -> cp2;
   cp12 -> cp2;
-  cp14 -> cp2;
-  cp16 -> cp2;
-  cp18 -> cp2;
-  cp20 -> cp2;
-  cp22 -> cp2;
-  cp25 -> cp24;
+  cp15 -> cp14;
   
   }
\ No newline at end of file