From 56614d6cc743b37ccd58add91f688c141a2d742e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 20 May 2020 10:13:58 +0200
Subject: [PATCH] [wp] Fixes an unsoundness in init filter
---
src/plugins/wp/Conditions.ml | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1b891377b39..8ecd2a69fee 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
--
GitLab