Skip to content
Snippets Groups Projects
Commit 56614d6c authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Fixes an unsoundness in init filter

parent 5b939abb
No related branches found
No related tags found
No related merge requests found
...@@ -1604,7 +1604,6 @@ struct ...@@ -1604,7 +1604,6 @@ struct
let on_sub_nodes = do_filter filter in let on_sub_nodes = do_filter filter in
match F.p_expr p with match F.p_expr p with
| And ps -> p_all on_sub_nodes ps | 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) | If(e,a,b) -> F.p_if e (on_sub_nodes a) (on_sub_nodes b)
| _ when has_init filter p -> p_true | _ when has_init filter p -> p_true
| _ -> p | _ -> p
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment