diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config index 5221e8c0f16237b724d4e1a878776e1b22e8ac88..d71d6024da0cf68a48b803c1cebd369561434d5f 100644 --- a/src/plugins/wp/tests/ptests_config +++ b/src/plugins/wp/tests/ptests_config @@ -1,8 +1,8 @@ DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare -DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip +DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare -qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip +qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip qualif_SUITES= why3 ce_SUITES= wp_ce