diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 7dd1486b6392c83a551f712d82ae8ec3194d6242..88d853e711713b55f8710cee0bbe54806fc842d6 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -99,11 +99,39 @@ let collect_calls ~bhv stmt =
         x vf args kind loc
   | _ -> Fset.empty
 
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization Key                                                    --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Key =
+struct
+  type t = { kf: Kernel_function.t ; bhv : string list ; prop : string list }
+  let compare a b =
+    let cmp = Kernel_function.compare a.kf b.kf in
+    if cmp <> 0 then cmp else
+      let cmp = Stdlib.compare a.bhv b.bhv in
+      if cmp <> 0 then cmp else
+        Stdlib.compare a.prop b.prop
+  let pp_filter kind fmt xs =
+    match xs with
+    | [] -> ()
+    | x::xs ->
+        Format.fprintf fmt "~%s:%s" kind x ;
+        List.iter (Format.fprintf fmt ",%s") xs
+  let pretty fmt k =
+    begin
+      Kernel_function.pretty fmt k.kf ;
+      pp_filter "bhv" fmt k.bhv ;
+      pp_filter "prop" fmt k.prop ;
+    end
+end
+
 (* -------------------------------------------------------------------------- *)
 (* --- Main Collection Pass                                               --- *)
 (* -------------------------------------------------------------------------- *)
 
-let collect kf cfg ?(bhv=[]) ?(prop=[]) () =
+let compile Key.{ kf ; bhv ; prop } =
+  let cfg = Cfg.get_automaton kf in
   let infos = {
     cfg ;
     annots = false ;
@@ -134,3 +162,18 @@ let collect kf cfg ?(bhv=[]) ?(prop=[]) () =
   infos
 
 (* -------------------------------------------------------------------------- *)
+(* --- Memoization Data                                                   --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Generator = WpContext.StaticGenerator(Key)
+    (struct
+      type key = Key.t
+      type data = t
+      let name = "Wp.CfgInfos.Generator"
+      let compile = compile
+    end)
+
+let collect kf ?(bhv=[]) ?(prop=[]) () =
+  Generator.get { kf ; bhv ; prop }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index a568567c1fc7cd519534b634a36ca1d9ffaa8a6c..355a3efcffd97d244a7f8262f5568638564ce9b3 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -26,10 +26,10 @@ type t
 
 module Cfg = Interpreted_automata
 
-val collect : Kernel_function.t -> Cfg.automaton ->
-  ?bhv:string list ->
-  ?prop:string list ->
-  unit -> t
+(** Memoized *)
+val collect :
+  Kernel_function.t -> ?bhv:string list -> ?prop:string list -> unit -> t
+
 val annots : t -> bool
 val doomed : t -> WpPropId.prop_id Bag.t
 val calls : t -> Kernel_function.Set.t