diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 5944017b75c270cceee4140b80ec2a5b5dac58d5..235d65c7ff4c65c04321a4e3c40880d776321437 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -374,3 +374,12 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
 let get_loop_contract kf stmt = LoopContract.get (kf,stmt)
 
 (* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts                                                    --- *)
+(* -------------------------------------------------------------------------- *)
+
+let clear () =
+  CallContract.clear () ;
+  LoopContract.clear () ;
+  CodeAssertions.clear ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 302d1b08ba7ee314cb4a7e91ad8689df81d1cb6d..5fe25bdd1086ad413a27dc427f3471e291fd09f0 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -93,3 +93,9 @@ val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
 val get_call_contract : kernel_function -> call_contract
 
 (* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts                                                    --- *)
+(* -------------------------------------------------------------------------- *)
+
+val clear : unit -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index d781ebb00f4c64b4c1586b8248b80bf059cfb7f9..c6872377e710fb0303155c75518e1a28ffaa9d6d 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -213,6 +213,8 @@ struct
              end
              (List.rev modes)
         ) task.modes ;
+      CfgAnnot.clear () ;
+      CfgInfos.clear () ;
       !collection
     end
 
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 852fe68b4e34285724c7bd2010f779bee72f0f3a..013e77df4fcbf19dc2dd0f6e393d248f52552cf6 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -252,5 +252,6 @@ module Generator = WpContext.StaticGenerator(Key)
     end)
 
 let get kf ?(bhv=[]) ?(prop=[]) () = Generator.get { kf ; bhv ; prop }
+let clear () = Generator.clear ()
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index b94ab3471ef763f76563d0a9fa8e7ce4e00a0c42..b5420e9ffe881adf46dde218730c36932d234894 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -30,6 +30,8 @@ module Cfg = Interpreted_automata
 val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
   unit -> t
 
+val clear : unit -> unit
+
 val cfg : t -> Cfg.automaton option
 val annots : t -> bool
 val doomed : t -> WpPropId.prop_id Bag.t