diff --git a/src/plugins/wp/Footprint.ml b/src/plugins/wp/Footprint.ml
index a05d0d02ad71ef611b02cd661930c1f72b044c42..0198e11baab73ddf075ac879d968a21867a0e00a 100644
--- a/src/plugins/wp/Footprint.ml
+++ b/src/plugins/wp/Footprint.ml
@@ -31,7 +31,8 @@ let iter f e =
   Queue.add e q ;
   while not (Queue.is_empty q) do
     let e = Queue.pop q in
-    f e ; F.lc_iter (fun e -> Queue.push e q) e
+    if F.lc_closed e then f e ;
+    F.lc_iter (fun e -> Queue.push e q) e
   done
 
 let once f e =
@@ -42,7 +43,8 @@ let once f e =
   Queue.add e q ;
   while not (Queue.is_empty q) do
     let e = Queue.pop q in
-    f e ; F.lc_iter (fun e -> if once m e then Queue.push e q) e
+    if F.lc_closed e then f e ;
+    F.lc_iter (fun e -> if once m e then Queue.push e q) e
   done
 
 (* -------------------------------------------------------------------------- *)
@@ -151,3 +153,5 @@ let lookup ~occur ~inside =
       ) inside ;
     raise Not_found
   with Found e -> e
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Footprint.mli b/src/plugins/wp/Footprint.mli
index 868824c83bf007b4a8db215e4e4ae77519e76d87..9e2e9a739a4c629dd7af9e0d3ef293b7de53281d 100644
--- a/src/plugins/wp/Footprint.mli
+++ b/src/plugins/wp/Footprint.mli
@@ -49,3 +49,5 @@ val locate : select:term -> inside:term -> occurrence
 
 (** Retrieve back the [k]-th occurrence of a footprint inside a term. *)
 val lookup : occur:occurrence -> inside:term -> term
+
+(* -------------------------------------------------------------------------- *)