diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index f2b7abc13875fb0113053421aace7c796df5eaf7..b21fa463f9fdd3b9aae169f4c37799a80600c8d0 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -84,9 +84,9 @@ let is_dead_annot ca =
   match ca.annot_content with
   | APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
       false && is_unrolled_completely spec
-  | AAssert([],p) ->
+  | AAssert([],p)
+  | AInvariant([],_,p) ->
       not p.tp_only_check && is_predicate false p.tp_statement
-  | AInvariant([],_,p) -> is_predicate false p.tp_statement
   | _ -> false
 
 let is_dead_code stmt =