From 2cc4f5a7c6c0b32a85c2a3c04ba4f40c2b15c844 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Feb 2021 15:01:41 +0100
Subject: [PATCH] [wp] Filter no_wp
---
src/plugins/wp/cfgCalculus.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index d2e8be2e49f..5ff18776dae 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -106,7 +106,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
let is_selected_props (props : props) ?pi pid =
WpPropId.filter_status pid &&
match props with
- | `All | `Names [] -> true
+ | `All | `Names [] -> WpPropId.select_default pid
| `Names ps -> WpPropId.select_by_name ps pid
| `PropId p ->
Property.equal p @@ match pi with
--
GitLab