[wp] (qualif) tests oracles related to Why3 VC format

src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle

 File "spec_memory.why", line 24, characters 4-56:
-Verification condition check_valid_rd.
+Goal check_valid_rd.
 Prover result is: Valid.
 
 File "spec_memory.why", line 27, characters 4-56:
-Verification condition check_valid.
+Goal check_valid.
 Prover result is: Valid.
 
 File "spec_memory.why", line 30, characters 4-62:
-Verification condition invalid_spec.
+Goal invalid_spec.
 Prover result is: Valid.
 
 File "spec_memory.why", line 34, characters 4-76:
-Verification condition invalid_null_spec.
+Goal invalid_null_spec.
 Prover result is: Valid.
 
 File "spec_memory.why", line 38, characters 4-51:
-Verification condition invalid_null.
+Goal invalid_null.
 Prover result is: Valid.
 
 File "spec_memory.why", line 42, characters 4-79:
-Verification condition invalid_empty.
+Goal invalid_empty.
 Prover result is: Valid.
 
 File "spec_memory.why", line 46, characters 4-59:
-Verification condition valid_rd_null.
+Goal valid_rd_null.
 Prover result is: Valid.
 
 File "spec_memory.why", line 49, characters 4-59:
-Verification condition valid_rw_null.
+Goal valid_rw_null.
 Prover result is: Valid.
 
 File "spec_memory.why", line 52, characters 4-34:
-Verification condition valid_obj_null.
+Goal valid_obj_null.
 Prover result is: Valid.
 
 File "spec_memory.why", line 56, characters 4-77:
-Verification condition INC_P.
+Goal INC_P.
 Prover result is: Valid.
 
 File "spec_memory.why", line 60, characters 4-169:
-Verification condition INC_A.
+Goal INC_A.
 Prover result is: Valid.
 
 File "spec_memory.why", line 67, characters 4-63:
-Verification condition INC_1.
+Goal INC_1.
 Prover result is: Valid.
 
 File "spec_memory.why", line 71, characters 4-64:
-Verification condition INC_2.
+Goal INC_2.
 Prover result is: Valid.
 
 File "spec_memory.why", line 75, characters 4-161:
-Verification condition INC_3.
+Goal INC_3.
 Prover result is: Valid.
 
 File "spec_memory.why", line 82, characters 4-178:
-Verification condition INC_4.
+Goal INC_4.
 Prover result is: Valid.
 

src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle

@@ -2,5 +2,5 @@
 WP Requirements for Qualif Tests (3)
 ----------------------------------------------------------
 1. The Alt-Ergo theorem prover, version 2.2.0
-2. The Why3 platform, version 1.4.0
+2. The Why3 platform, version 1.5.0
 ----------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle

@@ -74,7 +74,7 @@ end
     goal wp_goal :
       forall t:addr -> int, i:int, a:addr.
        let x = get t (shift_sint32 a i) in
-       region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+       region (a.base) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
   end
 [wp] [Alt-Ergo] Goal typed_f_ensures : Unsuccess
 [wp] Proved goals:    0 / 1
@@ -154,7 +154,7 @@ end
     goal wp_goal :
       forall t:addr1 -> int, i:int, a:addr1.
        let x = get1 t (shift_sint321 a i) in
-       region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
+       region1 (a.base1) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
   end
 [wp] [Alt-Ergo] Goal typed_ref_f_ensures : Unsuccess
 [wp] Proved goals:    0 / 1