diff --git a/src/plugins/wp/tests/wp_bts/bts_2471.i b/src/plugins/wp/tests/wp_bts/bts_2471.i index 2419c0debd8c56f0daafc2f0bdae517aadb72fff..a25c144dafc34fea9b4067ea4e9e953d1ff1505e 100644 --- a/src/plugins/wp/tests/wp_bts/bts_2471.i +++ b/src/plugins/wp/tests/wp_bts/bts_2471.i @@ -4,7 +4,6 @@ /* run.config_qualif OPT: -wp-timeout 1 - OPT: -wp-prover native:alt-ergo -wp-timeout 1 OPT: -wp-prover native:coq */ diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle index ffb3913bc3829c2336a99250827f72c490e1ca85..daef8736024e638253e9724c9732a577d90cb7df 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle @@ -1,12 +1,13 @@ -# frama-c -wp -wp-timeout 1 [...] +# frama-c -wp [...] [kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] Warning: native support for alt-ergo is deprecated, use why3 instead +[wp] Warning: native support for coq is deprecated, use tip instead [wp] 1 goal scheduled -[wp] [Alt-Ergo (native)] Goal typed_foo_assert_ko : Unsuccess +[wp] [Coq] Goal typed_foo_assert_ko : Default tactic +[wp] [Coq (native)] Goal typed_foo_assert_ko : Unsuccess [wp] Proved goals: 0 / 1 - Alt-Ergo (native): 0 (unsuccess: 1) + Coq (native): 0 (unsuccess: 1) ------------------------------------------------------------ Functions WP Alt-Ergo Total Success foo - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle deleted file mode 100644 index daef8736024e638253e9724c9732a577d90cb7df..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle +++ /dev/null @@ -1,14 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: native support for coq is deprecated, use tip instead -[wp] 1 goal scheduled -[wp] [Coq] Goal typed_foo_assert_ko : Default tactic -[wp] [Coq (native)] Goal typed_foo_assert_ko : Unsuccess -[wp] Proved goals: 0 / 1 - Coq (native): 0 (unsuccess: 1) ------------------------------------------------------------- - Functions WP Alt-Ergo Total Success - foo - - 1 0.0% -------------------------------------------------------------