[wp] Filter proved properties

src/plugins/wp/cfgCalculus.ml

@@ -103,6 +103,7 @@ let is_active_mode ~mode (p: Property.t) =
     -> assert false (* n/a *)
 
 let is_selected_props (props : props) ?pi pid =
+  WpPropId.filter_status pid &&
   match props with
   | `All | `Names [] -> true
   | `Names ps -> WpPropId.select_by_name ps pid

src/plugins/wp/cfgGenerator.ml

@@ -31,7 +31,7 @@ module KFmap = Kernel_function.Map
 
 type task = {
   mutable lemmas: LogicUsage.logic_lemma list ;
-  mutable modes: CfgCalculus.mode KFmap.t ;
+  mutable modes: CfgCalculus.mode KFmap.t ; (** TODO: when New CFG is validated, use list *)
   mutable props: CfgCalculus.props ;
 }