diff --git a/src/plugins/wp/tests/wp_bts/issue_143.i b/src/plugins/wp/tests/wp_bts/issue_143.i
deleted file mode 100644
index 575b826675ace4d42d0cd6edde246da14a06e800..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/issue_143.i
+++ /dev/null
@@ -1,22 +0,0 @@
-/* run.config
- DONTRUN:
-*/
-/* run.config_qualif
- CMD: chmod a-x %{dep:../../inexistant-prover} && @frama-c@ @WP_OPTIONS@ @PTEST_OPTIONS@
- OPT: -wp
- OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo %{dep:../../inexistant-prover} -wp-coqc %{dep:../../inexistant-prover}
- OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo %{dep:../../inexistant-prover}
- OPT: -wp -wp-prover "native:coq" -wp-coqc %{dep:../../inexistant-prover}
-*/
-
-/*@
- axiomatic A {
- lemma ok_because_inconsistent: \forall integer x; x > 0 ==> x < 0 ==> x == 0 ;
- }
-*/
-
-/*@
- axiomatic B {
- lemma ok_because_consistent: \forall integer x; x > 0 ==> x*x > 0 ;
- }
-*/
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
deleted file mode 100644
index 216f5e76554bf4fbb5c0759d37fa55c9afc616a2..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_141.res.oracle
+++ /dev/null
@@ -1,10 +0,0 @@
-# frama-c -wp -wp-rte -wp-steps 50 [...]
-[kernel] Parsing issue_141.i (no preprocessing)
-[wp] Running WP plugin...
-[rte] annotating function f
-[rte] annotating function main
-[wp] issue_141.i:18: Warning:
- calculus failed on strategy
- for 'main', behavior 'default!', all properties, both assigns or not because
- unsupported strange loop(s). (abort)
-[wp] No proof obligations
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 8d031ef0aec0346a1b754a010c2e9c610ff308a1..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 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%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
deleted file mode 100644
index ae88c968f4f93ede1636f0bfdd4f27dd1e5ab0ab..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
deleted file mode 100644
index dbc3692bd3d94259a85fbabd4eb7eac19af49ccf..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
deleted file mode 100644
index ae88c968f4f93ede1636f0bfdd4f27dd1e5ab0ab..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
deleted file mode 100644
index 75ee8bc5187fa26bf0bdd9a4993ea52715eeacef..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ /dev/null
@@ -1,17 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
-[wp] 2 goals scheduled
-[wp] [Coq (native)] Goal typed_lemma_ok_because_consistent : Failed
- Command '../../inexistant-prover' not found
-[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
-[wp] [Coq (native)] Goal typed_lemma_ok_because_inconsistent : Failed
- Command '../../inexistant-prover' not found
-[wp] Proved goals: 0 / 2
- Coq (native): 0 (failed: 2)
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - - 1 0.0%
- Axiomatic B - - 1 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
deleted file mode 100644
index 193391696738af597851faf822d15c08a2f2dbfa..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_f1_loop_assigns : Valid
-[wp] [Qed] Goal typed_f1_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f1_assigns : Valid
-[wp] [Qed] Goal typed_f2_loop_assigns : Valid
-[wp] [Qed] Goal typed_f2_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f2_assigns : Valid
-[wp] Proved goals: 6 / 6
- Qed: 6
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f1 3 - 3 100%
- f2 3 - 3 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
deleted file mode 100644
index 348854ab2a2864bf3bbde78b21b9acd64b020743..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ /dev/null
@@ -1,153 +0,0 @@
-# frama-c -wp -wp-rte [...]
-[kernel] Parsing frama_c_hashtbl_solved.c (with preprocessing)
-[wp] Running WP plugin...
-[rte] annotating function add
-[rte] annotating function eq_string
-[rte] annotating function hash
-[rte] annotating function init
-[rte] annotating function mem_binding
-[rte] annotating function size
-[wp] Goal typed_eq_string_complete_eq_not_eq : trivial
-[wp] Goal typed_eq_string_disjoint_eq_not_eq : trivial
-[wp] Goal typed_eq_string_loop_invariant_preserved : not tried
-[wp] Goal typed_eq_string_loop_invariant_established : not tried
-[wp] Goal typed_eq_string_loop_invariant_2_preserved : not tried
-[wp] Goal typed_eq_string_loop_invariant_2_established : not tried
-[wp] Goal typed_eq_string_assert_rte_mem_access : not tried
-[wp] Goal typed_eq_string_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_eq_string_assert_rte_signed_overflow : not tried
-[wp] Goal typed_eq_string_loop_assigns : trivial
-[wp] Goal typed_eq_string_assigns_part1 : not tried
-[wp] Goal typed_eq_string_assigns_part2 : not tried
-[wp] Goal typed_eq_string_assigns_part3 : not tried
-[wp] Goal typed_eq_string_assigns_part4 : not tried
-[wp] Goal typed_eq_string_loop_variant_decrease : not tried
-[wp] Goal typed_eq_string_loop_variant_positive : not tried
-[wp] Goal typed_eq_string_eq_ensures : not tried
-[wp] Goal typed_eq_string_not_eq_ensures : not tried
-[wp] Goal typed_hash_ensures_left_unproved : not tried
-[wp] Goal typed_hash_loop_invariant_preserved : not tried
-[wp] Goal typed_hash_loop_invariant_established : not tried
-[wp] Goal typed_hash_assert_rte_mem_access : not tried
-[wp] Goal typed_hash_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_hash_assert_rte_signed_overflow : not tried
-[wp] Goal typed_hash_loop_assigns : trivial
-[wp] Goal typed_hash_assigns_part1 : not tried
-[wp] Goal typed_hash_assigns_part2 : not tried
-[wp] Goal typed_hash_loop_variant_decrease : not tried
-[wp] Goal typed_hash_loop_variant_positive : not tried
-[wp] Goal typed_size_ensures : not tried
-[wp] Goal typed_size_assert_rte_mem_access : not tried
-[wp] Goal typed_size_assigns : not tried
-[wp] Goal typed_init_ensures : not tried
-[wp] Goal typed_init_ensures_2 : not tried
-[wp] Goal typed_init_assert_rte_mem_access : not tried
-[wp] Goal typed_init_loop_invariant_preserved : not tried
-[wp] Goal typed_init_loop_invariant_established : not tried
-[wp] Goal typed_init_loop_invariant_2_preserved : not tried
-[wp] Goal typed_init_loop_invariant_2_established : not tried
-[wp] Goal typed_init_assert_rte_index_bound : not tried
-[wp] Goal typed_init_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_init_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_init_assert_rte_signed_overflow : not tried
-[wp] Goal typed_init_loop_assigns_part1 : trivial
-[wp] Goal typed_init_loop_assigns_part2 : not tried
-[wp] Goal typed_init_assigns_part1 : not tried
-[wp] Goal typed_init_assigns_part2 : not tried
-[wp] Goal typed_init_assigns_part3 : not tried
-[wp] Goal typed_init_loop_variant_decrease : not tried
-[wp] Goal typed_init_loop_variant_positive : not tried
-[wp] Goal typed_add_complete_full_nominal : not tried
-[wp] Goal typed_add_disjoint_full_nominal : not tried
-[wp] Goal typed_add_assert_rte_index_bound : not tried
-[wp] Goal typed_add_assert_rte_mem_access : not tried
-[wp] Goal typed_add_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_3 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_4 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_5 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_3 : not tried
-[wp] Goal typed_add_assert_rte_index_bound_6 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_4 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_5 : not tried
-[wp] Goal typed_add_assert_rte_signed_overflow : not tried
-[wp] Goal typed_add_assert_rte_mem_access_6 : not tried
-[wp] Goal typed_add_assert_rte_mem_access_7 : not tried
-[wp] Goal typed_add_assert_rte_signed_overflow_2 : not tried
-[wp] Goal typed_add_assigns_exit : trivial
-[wp] Goal typed_add_assigns_normal_part1 : trivial
-[wp] Goal typed_add_assigns_normal_part2 : not tried
-[wp] Goal typed_add_assigns_normal_part3 : not tried
-[wp] Goal typed_add_assigns_normal_part4 : not tried
-[wp] Goal typed_add_assigns_normal_part5 : not tried
-[wp] Goal typed_add_assigns_normal_part6 : not tried
-[wp] Goal typed_add_assigns_normal_part7 : not tried
-[wp] Goal typed_add_assigns_normal_part8 : not tried
-[wp] Goal typed_add_assigns_normal_part9 : not tried
-[wp] Goal typed_add_call_hash_requires : not tried
-[wp] Goal typed_add_nominal_ensures : not tried
-[wp] Goal typed_add_nominal_ensures_2 : not tried
-[wp] Goal typed_add_nominal_ensures_3 : not tried
-[wp] Goal typed_add_nominal_ensures_4 : not tried
-[wp] Goal typed_add_nominal_ensures_5 : not tried
-[wp] Goal typed_add_nominal_assigns_exit : trivial
-[wp] Goal typed_add_nominal_assigns_normal_part1 : trivial
-[wp] Goal typed_add_nominal_assigns_normal_part2 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part3 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part4 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part5 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part6 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part7 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part8 : not tried
-[wp] Goal typed_add_nominal_assigns_normal_part9 : not tried
-[wp] Goal typed_add_full_ensures : not tried
-[wp] Goal typed_add_full_assigns_exit : trivial
-[wp] Goal typed_add_full_assigns_normal_part1 : trivial
-[wp] Goal typed_add_full_assigns_normal_part2 : not tried
-[wp] Goal typed_add_full_assigns_normal_part3 : not tried
-[wp] Goal typed_add_full_assigns_normal_part4 : not tried
-[wp] Goal typed_add_full_assigns_normal_part5 : not tried
-[wp] Goal typed_add_full_assigns_normal_part6 : not tried
-[wp] Goal typed_add_full_assigns_normal_part7 : not tried
-[wp] Goal typed_add_full_assigns_normal_part8 : not tried
-[wp] Goal typed_add_full_assigns_normal_part9 : not tried
-[wp] Goal typed_mem_binding_complete_found_not_found : not tried
-[wp] Goal typed_mem_binding_disjoint_found_not_found : not tried
-[wp] Goal typed_mem_binding_loop_invariant_preserved : not tried
-[wp] Goal typed_mem_binding_loop_invariant_established : not tried
-[wp] Goal typed_mem_binding_loop_invariant_2_preserved : not tried
-[wp] Goal typed_mem_binding_loop_invariant_2_established : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_2 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_3 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_4 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_5 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_6 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access_2 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_7 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_8 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_9 : not tried
-[wp] Goal typed_mem_binding_assert_rte_index_bound_10 : not tried
-[wp] Goal typed_mem_binding_assert_rte_mem_access_3 : not tried
-[wp] Goal typed_mem_binding_assert_rte_signed_overflow : not tried
-[wp] Goal typed_mem_binding_loop_assigns_part1 : trivial
-[wp] Goal typed_mem_binding_loop_assigns_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part1 : trivial
-[wp] Goal typed_mem_binding_assigns_exit_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part3 : not tried
-[wp] Goal typed_mem_binding_assigns_exit_part4 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part1 : trivial
-[wp] Goal typed_mem_binding_assigns_normal_part2 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part3 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part4 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part5 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part6 : not tried
-[wp] Goal typed_mem_binding_assigns_normal_part7 : not tried
-[wp] Goal typed_mem_binding_loop_variant_decrease : not tried
-[wp] Goal typed_mem_binding_loop_variant_positive : not tried
-[wp] Goal typed_mem_binding_call_hash_requires : not tried
-[wp] Goal typed_mem_binding_call_eq_string_requires : not tried
-[wp] Goal typed_mem_binding_call_eq_string_requires_2 : not tried
-[wp] Goal typed_mem_binding_found_ensures : not tried
-[wp] Goal typed_mem_binding_not_found_ensures : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle
deleted file mode 100644
index f8fa052d8e0a246603ecc91666f450bda1525dd7..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle/loop-statement.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing loop-statement.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] Goal typed_lemma_Lb : not tried
-[wp] Goal typed_loop_statement_requires_Scond : not tried
-[wp] Goal typed_loop_statement_ensures_Sbody : not tried
-[wp] Goal typed_loop_statement_assigns : trivial
-[wp] Goal typed_loop_statement_requires_Rinv : not tried
-[wp] Goal typed_loop_statement_ensures_Scond : not tried
-[wp] Goal typed_loop_statement_ensures_Sloop : not tried
-[wp] Goal typed_loop_statement_loop_invariant_Iloop_preserved : not tried
-[wp] Goal typed_loop_statement_loop_invariant_Iloop_established : not tried
-[wp] Goal typed_loop_statement_loop_assigns_part1 : trivial
-[wp] Goal typed_loop_statement_loop_assigns_part2 : not tried
-[wp] Goal typed_loop_statement_assigns_2_exit_part1 : trivial
-[wp] Goal typed_loop_statement_assigns_2_exit_part2 : not tried
-[wp] Goal typed_loop_statement_assigns_2_normal_part1 : trivial
-[wp] Goal typed_loop_statement_assigns_2_normal_part2 : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
deleted file mode 100644
index c99172a223bc3449ae605c420826261c541b5494..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ /dev/null
@@ -1,181 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing frama_c_hashtbl_solved.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 102 goals scheduled
-[wp] [Qed] Goal typed_eq_string_complete_eq_not_eq : Valid
-[wp] [Qed] Goal typed_eq_string_disjoint_eq_not_eq : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_eq_string_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_eq_string_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_eq_string_loop_assigns : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part1 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part2 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part3 : Valid
-[wp] [Qed] Goal typed_eq_string_assigns_part4 : Valid
-[wp] [Qed] Goal typed_eq_string_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_eq_string_loop_variant_positive : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_eq_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_not_eq_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_hash_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_hash_loop_invariant_established : Valid
-[wp] [Qed] Goal typed_hash_loop_assigns : Valid
-[wp] [Qed] Goal typed_hash_assigns_part1 : Valid
-[wp] [Qed] Goal typed_hash_assigns_part2 : Valid
-[wp] [Qed] Goal typed_hash_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_hash_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_size_ensures : Valid
-[wp] [Qed] Goal typed_size_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_init_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_init_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_init_assigns_part1 : Valid
-[wp] [Qed] Goal typed_init_assigns_part2 : Valid
-[wp] [Script] Goal typed_init_assigns_part3 : Valid
-[wp] [Qed] Goal typed_init_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_init_loop_variant_positive : Valid
-[wp] [Alt-Ergo] Goal typed_add_complete_full_nominal : Valid
-[wp] [Alt-Ergo] Goal typed_add_disjoint_full_nominal : Valid
-[wp] [Qed] Goal typed_add_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_assigns_normal_part9 : Valid
-[wp] [Qed] Goal typed_add_call_hash_requires : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_3 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_4 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_ensures_5 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_nominal_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_nominal_assigns_normal_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_ensures : Valid
-[wp] [Qed] Goal typed_add_full_assigns_exit : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part7 : Valid
-[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part8 : Valid
-[wp] [Qed] Goal typed_add_full_assigns_normal_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_complete_found_not_found : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_disjoint_found_not_found : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_established : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_2_preserved : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_invariant_2_established : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_exit_part4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part1 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part5 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part6 : Valid
-[wp] [Qed] Goal typed_mem_binding_assigns_normal_part7 : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_variant_decrease : Valid
-[wp] [Qed] Goal typed_mem_binding_loop_variant_positive : Valid
-[wp] [Qed] Goal typed_mem_binding_call_hash_requires : Valid
-[wp] [Qed] Goal typed_mem_binding_call_eq_string_requires : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_call_eq_string_requires_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_found_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_not_found_ensures : Valid
-[wp] Proved goals: 102 / 102
- Qed: 69
- Script: 1
- Alt-Ergo: 32
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- eq_string 11 4 15 100%
- hash 6 1 7 100%
- size 2 - 2 100%
- init 8 4 13 100%
- add 24 15 39 100%
- mem_binding 18 8 26 100%
-------------------------------------------------------------
-[wp] Running WP plugin...
-[rte] annotating function add
-[rte] annotating function eq_string
-[rte] annotating function hash
-[rte] annotating function init
-[rte] annotating function mem_binding
-[rte] annotating function size
-[wp] 41 goals scheduled
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_eq_string_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_hash_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_hash_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_hash_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_size_assert_rte_mem_access : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_init_assert_rte_index_bound : Valid
-[wp] [Qed] Goal typed_init_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_index_bound_3 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_4 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_2 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_mem_access_3 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_4 : Valid
-[wp] [Qed] Goal typed_add_assert_rte_mem_access_5 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_6 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_mem_access_7 : Valid
-[wp] [Alt-Ergo] Goal typed_add_assert_rte_signed_overflow_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_3 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_4 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_5 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_2 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_7 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_8 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_9 : Valid
-[wp] [Qed] Goal typed_mem_binding_assert_rte_index_bound_10 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_mem_access_3 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_assert_rte_signed_overflow : Valid
-[wp] Proved goals: 41 / 41
- Qed: 16
- Alt-Ergo: 25
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- eq_string 11 7 18 100%
- hash 7 3 10 100%
- size 2 1 3 100%
- init 10 7 18 100%
- add 30 24 54 100%
- mem_binding 25 15 40 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
deleted file mode 100644
index 940355bf8dd007765944c8173ebf5315bc89a1c0..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
+++ /dev/null
@@ -1,30 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing loop-statement.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 15 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_Lb : Unsuccess
-[wp] [Qed] Goal typed_loop_statement_requires_Scond : Valid
-[wp] [Qed] Goal typed_loop_statement_ensures_Sbody : Valid
-[wp] [Qed] Goal typed_loop_statement_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_loop_statement_requires_Rinv : Valid
-[wp] [Qed] Goal typed_loop_statement_ensures_Scond : Valid
-[wp] [Qed] Goal typed_loop_statement_ensures_Sloop : Valid
-[wp] [Alt-Ergo] Goal typed_loop_statement_loop_invariant_Iloop_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_loop_statement_loop_invariant_Iloop_established : Valid
-[wp] [Qed] Goal typed_loop_statement_loop_assigns_part1 : Valid
-[wp] [Qed] Goal typed_loop_statement_loop_assigns_part2 : Valid
-[wp] [Qed] Goal typed_loop_statement_assigns_2_exit_part1 : Valid
-[wp] [Qed] Goal typed_loop_statement_assigns_2_exit_part2 : Valid
-[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part1 : Valid
-[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part2 : Valid
-[wp] Proved goals: 14 / 15
- Qed: 11
- Alt-Ergo: 3 (unsuccess: 1)
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic Ploop - - 1 0.0%
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- loop_statement 11 3 14 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
deleted file mode 100644
index 290bc031ca0df2a69b143f3c8fe368053428895d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_hoare/oracle/alias_assigns_hypotheses.res.oracle
+++ /dev/null
@@ -1,254 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing alias_assigns_hypotheses.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function comprehension_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 85) in 'comprehension_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 86) in 'comprehension_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 84) in 'comprehension_alias':
-Effect at line 88
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function field_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 54) in 'field_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 55) in 'field_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 53) in 'field_alias':
-Effect at line 57
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function field_range_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 66) in 'field_range_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 67) in 'field_range_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 65) in 'field_range_alias':
-Effect at line 69
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 25) in 'formal_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 26) in 'formal_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 24) in 'formal_alias':
-Effect at line 28
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_alias_array
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 40) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 41) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 42) in 'formal_alias_array':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (1/2):
-Effect at line 44
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 39) in 'formal_alias_array' (2/2):
-Effect at line 45
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function formal_no_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 33) in 'formal_no_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 32) in 'formal_no_alias':
-Effect at line 35
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function global_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 10) in 'global_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 11) in 'global_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 9) in 'global_alias':
-Effect at line 13
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function global_no_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 18) in 'global_no_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 17) in 'global_no_alias':
-Effect at line 20
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function set_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 74) in 'set_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 75) in 'set_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 73) in 'set_alias':
-Effect at line 77
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function union_alias
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 95) in 'union_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file alias_assigns_hypotheses.i, line 96) in 'union_alias':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file alias_assigns_hypotheses.i, line 94) in 'union_alias':
-Effect at line 98
-Prove: true.
-
-------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'global_alias':
- /*@
- behavior typed:
- requires \separated(g_alias,\union(&g_alias,global+(..)));
- */
- void global_alias(void);
-[wp] Warning: Memory model hypotheses for function 'global_no_alias':
- /*@ behavior typed: requires \separated(g_alias,&g_alias); */
- void global_no_alias(void);
-[wp] Warning: Memory model hypotheses for function 'formal_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),f_alias);
- requires \separated(f_alias,global+(..));
- */
- void formal_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'formal_alias_array':
- /*@
- behavior typed:
- requires \separated(global+(..),alias_array+(..));
- requires \separated(&(*alias_array)[0 .. 1],global+(..));
- */
- void formal_alias_array(int (*alias_array)[2]);
-[wp] Warning: Memory model hypotheses for function 'field_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),x);
- requires \separated(&x->x,global+(..));
- */
- void field_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'field_range_alias':
- /*@
- behavior typed:
- requires \separated(global+(..),x+(..));
- requires \separated(&(x + (0 .. 3))->x,global+(..));
- */
- void field_range_alias(struct X *x);
-[wp] Warning: Memory model hypotheses for function 'set_alias':
- /*@
- behavior typed:
- requires \separated(\union(global+(..),&g_alias),f_alias);
- requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
- */
- void set_alias(int *f_alias);
-[wp] Warning: Memory model hypotheses for function 'comprehension_alias':
- /*@
- behavior typed:
- requires \separated({alias | int *alias; alias ≡ \at(g_alias,Pre)},
- \union(&g_alias,global+(..)));
- */
- void comprehension_alias(void);
-[wp] Warning: Memory model hypotheses for function 'union_alias':
- /*@
- behavior typed:
- requires \separated(\union(global+(..),&g_alias),f_alias);
- requires \separated({g_alias, f_alias},\union(&g_alias,global+(..)));
- */
- void union_alias(int *f_alias);