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 68dc1319cde49b90405061a831cef2979123dab9..d1bac58fc498ae25867f0a51a83cbcea2f94f795 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 @@ -3,6 +3,7 @@ [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards +[wp] Warning: native support for alt-ergo is deprecated, use why3 instead [wp] 1 goal scheduled [wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess [wp] Proved goals: 0 / 1 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 index 6c44b75068c14cfa5ea543478657ca61008ceeef..c83a6e29b181ad4907472692dddfebddeafa80c3 100644 --- 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 @@ -3,6 +3,7 @@ [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' [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 diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json index 5d34a2aa148ec69a768c4de87205861440f6366d..174835a1aa1206e5e4fb046badfcc607c4caf659 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json @@ -1,14 +1,10 @@ -{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 1 }, - "wp:main": { "total": 1, "valid": 1, "rank": 1 } }, +{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 }, + "wp:main": { "total": 1, "valid": 1 } }, "wp:functions": { "Job": { "Job_ensures": { "why3:Alt-Ergo,2.0.0": - { "total": 1, "valid": 1, - "rank": 1 }, + { "total": 1, "valid": 1 }, "wp:main": { "total": 1, - "valid": 1, - "rank": 1 } }, + "valid": 1 } }, "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1, - "valid": 1, - "rank": 1 }, + "valid": 1 }, "wp:main": { "total": 1, - "valid": 1, - "rank": 1 } } } } } + "valid": 1 } } } } } diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle index 48f19a88154aac3ef6ba18614891f4c87c71fdaa..487049986e2a19d8714a9bad06ff32efabe7b552 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle @@ -14,5 +14,5 @@ [wp] Report out: 'tests/wp_typed/result_qualif/mvar.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -Job - 1 (1..12) 1 100% +Job - 1 1 100% -------------------------------------------------------------