diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 1f303b5fc343639808b8f3106b1012cc0f412b86..c5ac01b0f158f382b900f32769ef89b3555a2842 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -48,40 +48,11 @@ let compute_ip cc ip =
         | _ -> ()
       in iter cc ip ;
       cc#compute
-
-  | IPBehavior {ib_kf; ib_bhv} ->
-      let model = cc#model in
-      let bhv = [ib_bhv.Cil_types.b_name] in
-      let assigns = WpAnnot.WithAssigns in
-      List.iter cc#add_strategy
-        (WpAnnot.get_function_strategies ~model ~assigns ~bhv ib_kf) ;
-      cc#compute
-  | IPComplete _
-  | IPDisjoint _
-  | IPCodeAnnot _
-  | IPAllocation _
-  | IPAssigns _
-  | IPDecrease _
-  | IPPredicate _
-    ->
-      let model = cc#model in
-      let assigns = WpAnnot.WithAssigns in
+  | _ ->
       List.iter cc#add_strategy
-        (WpAnnot.get_id_prop_strategies ~model ~assigns ip) ;
+        (WpAnnot.get_property_strategies ~model:cc#model ip) ;
       cc#compute
 
-  | IPFrom _
-  | IPAxiom _
-  | IPReachable _
-  | IPPropertyInstance _
-  | IPOther _
-  | IPTypeInvariant _
-  | IPGlobalInvariant _
-  | IPExtended _
-    ->
-      Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
-      Bag.empty
-
 (* -------------------------------------------------------------------------- *)
 (* --- Annotations Entry Point                                            --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index d8d221d9cbd5209bb9adca1d4105cd6ddfe3715d..8165aea5076ac48e23384369df8e525d7c8fae32 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1386,29 +1386,13 @@ struct
 
       end !groups
 
-  let lemma = L.lemma
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- WPO Computer                                                       --- *)
-(* -------------------------------------------------------------------------- *)
-
-module KFmap = Kernel_function.Map
-
-module Computer(M : Sigs.Compiler) =
-struct
-
-  module VCG = VC(M)
-  module WP = Calculus.Cfg(VCG)
-
-  let compile_lemma l = ignore (VCG.lemma l)
+  let lemma l = ignore (L.lemma l)
 
   let prove_lemma collection l =
     if l.lem_kind <> `Axiom then
       begin
         let id = WpPropId.mk_lemma_id l in
-        let def = VCG.lemma l in
+        let def = L.lemma l in
         let model = WpContext.get_model () in
         let vca = {
           Wpo.VC_Lemma.depends = l.lem_depends ;
@@ -1435,6 +1419,20 @@ struct
         collection := Bag.append !collection wpo ;
       end
 
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- WPO Computer                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+module KFmap = Kernel_function.Map
+
+module Computer(M : Sigs.Compiler) =
+struct
+
+  module VCG = VC(M)
+  module WP = Calculus.Cfg(VCG)
+
   let prove_strategy collection model kf strategy =
     let cfg = WpStrategy.cfg_of_strategy strategy in
     let bhv = WpStrategy.get_bhv strategy in
@@ -1469,14 +1467,14 @@ struct
           Lang.F.release () ;
           WpContext.on_context (model,WpContext.Global)
             begin fun () ->
-              LogicUsage.iter_lemmas compile_lemma ;
-              Bag.iter (prove_lemma collection) lemmas ;
+              LogicUsage.iter_lemmas VCG.lemma ;
+              Bag.iter (VCG.prove_lemma collection) lemmas ;
             end () ;
           KFmap.iter
             (fun kf strategies ->
                WpContext.on_context (model,WpContext.Kf kf)
                  begin fun () ->
-                   LogicUsage.iter_lemmas compile_lemma ;
+                   LogicUsage.iter_lemmas VCG.lemma ;
                    Bag.iter (prove_strategy collection model kf) strategies ;
                  end ()
             ) annots ;
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 9b3af468c5b5b4f651a947f82a0059ee56f37241..1e0f4006807ef333e08be1f81b91c615d293974a 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1344,3 +1344,35 @@ let get_function_strategies ~model
     ?(assigns=WithAssigns) ?(bhv=[]) ?(prop=[]) kf =
   let prop = match prop with [] -> AllProps | _ -> NamedProp prop in
   get_strategies assigns kf model bhv None prop
+
+let get_property_strategies ~model ip =
+  let open Property in
+  match ip with
+  | IPBehavior {ib_kf; ib_bhv} ->
+      let bhv = [ib_bhv.Cil_types.b_name] in
+      let assigns = WithAssigns in
+      get_function_strategies ~model ~assigns ~bhv ib_kf
+  | IPComplete _
+  | IPDisjoint _
+  | IPCodeAnnot _
+  | IPAllocation _
+  | IPAssigns _
+  | IPDecrease _
+  | IPPredicate _
+    ->
+      let assigns = WithAssigns in
+      get_id_prop_strategies ~model ~assigns ip
+
+  | IPAxiomatic _
+  | IPLemma _
+  | IPFrom _
+  | IPAxiom _
+  | IPReachable _
+  | IPPropertyInstance _
+  | IPOther _
+  | IPTypeInvariant _
+  | IPGlobalInvariant _
+  | IPExtended _
+    ->
+      Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
+      []
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 8155d57820cd0551626b2db6c2e9d8e8cebc1c74..835a1e968812e50d5ce4db1956ac1d1b5f6f628e 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -34,10 +34,6 @@ open Cil_types
 
 type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
 
-val get_id_prop_strategies :
-  model:WpContext.model ->
-  ?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
-
 val get_call_pre_strategies :
   model:WpContext.model ->
   stmt -> WpStrategy.strategy list
@@ -49,4 +45,7 @@ val get_function_strategies :
   ?prop:string list ->
   Kernel_function.t -> WpStrategy.strategy list
 
+val get_property_strategies :
+  model:WpContext.model -> Property.t -> WpStrategy.strategy list
+
 (*----------------------------------------------------------------------------*)