diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1b891377b39343d9974a7df34386339fd732533c..8ecd2a69feeb67993e6eca44ccf1ebb7c99bbf85 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1604,7 +1604,6 @@ struct
     let on_sub_nodes = do_filter filter in
     match F.p_expr p with
     | And ps -> p_all on_sub_nodes ps
-    | Or ps -> p_disj List.(filter (fun p -> p <> p_true) (map on_sub_nodes ps))
     | If(e,a,b) -> F.p_if e (on_sub_nodes a) (on_sub_nodes b)
     | _ when has_init filter p -> p_true
     | _ -> p