diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml index ef586c7c564d4828314f461de419d5cf8650cac9..d886bdacd26e6ed444a456a45810ae25a261c159 100644 --- a/src/plugins/wp/cfgCalculus.ml +++ b/src/plugins/wp/cfgCalculus.ml @@ -85,8 +85,7 @@ let is_active_mode ~mode ~goal (p: Property.t) = | IPCodeAnnot { ica_ca } -> is_selected_ca mode ~goal ica_ca | IPPredicate { ip_kind } -> begin match ip_kind with - | PKRequires bhv | PKAssumes bhv -> - Cil.is_default_behavior bhv || is_selected_bhv mode bhv + | PKRequires _ | PKAssumes _ -> true | PKEnsures(bhv,_) -> is_selected_bhv mode bhv | PKTerminates -> is_default_bhv mode end