diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
index e7d2df64f395d9814a589f493f994e7dc49839ba..04d1c97261bf1c50ddebd680e3f9f7458ddffaca 100644
--- a/devel_tools/docker/Makefile
+++ b/devel_tools/docker/Makefile
@@ -98,7 +98,7 @@ ocamlfind.1.8.1 \\\
 ocamlgraph.1.8.8 \\\
 ppx_deriving_yojson.3.6.1 \\\
 ppx_import.1.9.0 \\\
-why3.1.4.0 \\\
+why3.1.5.0 \\\
 yojson.1.7.0 \\\
 zarith.1.10 \\\
 zmq.5.1.3 \\\
diff --git a/nix/default.nix b/nix/default.nix
index 3c5b73797c7233d802bd5eed6bde49fb0c9bcc1f..d9f8349f5d7db3034a05fff70433d66e6ed7a9e5 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -11,7 +11,7 @@ let mydir = builtins.getEnv("PWD");
       [ "ocamlfind" "zarith" "ocamlgraph" "yojson" "zmq"
         "ppx_import" "ppx_deriving" "ppx_deriving_yojson"
         "coq=8.13.0" "alt-ergo=2.2.0"
-        "why3=1.4.0" "why3-coq=1.4.0"
+        "why3=1.5.0" "why3-coq=1.5.0"
         "menhir=20211012"
         "easy-format=1.3.2"
       ];
diff --git a/opam/opam b/opam/opam
index b7c3f147d041645e31f22f9a08626b5a440b6ff6..4c6a1fa77fe2003a2cc26bbf6cd9510e17119e2f 100644
--- a/opam/opam
+++ b/opam/opam
@@ -120,7 +120,7 @@ depends: [
   "ocaml" { >= "4.08.1" }
   "ocamlfind" # needed beyond build stage, used by -load-module
   "ocamlgraph" { >= "1.8.8" }
-  "why3" { >= "1.4.0" & < "1.5~" }
+  "why3" { >= "1.5.0" }
   "yojson" {>= "1.6.0"}
   "zarith" {>= "1.5"}
 ]
diff --git a/reference-configuration.md b/reference-configuration.md
index 230a167885f83de851a73c69ebce1375484b990c..df8c90259b25650348bcf916304d871158e1ef1b 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -15,7 +15,7 @@ support libraries (notably gtksourceview). lablgtk3 should be preferred.
 - ocamlgraph.1.8.8
 - ppx_deriving_yojson.3.6.1 (for mdr, optional)
 - ppx_import.1.9.1
-- why3.1.4.0
+- why3.1.5.0
 - yojson.1.7.0
 - zarith.1.12
 
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 44ab3d0f7f41c3a5b67289e40192f687657f0ffe..314769066fb4a6cd8edb0a31f0dd036445ba7c5f 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -39,13 +39,19 @@ let option_qual =
 let why3_failure msg =
   Pretty_utils.ksfprintf failwith msg
 
-module Env = WpContext.Index(struct
+type why3_conf = {
+  env : Why3.Env.env ;
+  libdir : string ;
+  datadir : string ;
+}
+
+module Conf = WpContext.Index(struct
     include Datatype.Unit
     type key = unit
-    type data = Why3.Env.env
+    type data = why3_conf
   end)
 
-let get_why3_env = Env.memoize
+let get_why3_conf = Conf.memoize
     begin fun () ->
       let config = Why3Provers.config () in
       let main = Why3.Whyconf.get_main config in
@@ -53,12 +59,14 @@ let get_why3_env = Env.memoize
         (WpContext.directory () :> string)::
         ((Wp_parameters.Share.get_dir ~mode:`Must_exist "why3") :> string)::
         (Why3.Whyconf.loadpath main) in
-      Why3.Env.create_env ld
+      let libdir = Why3.Whyconf.libdir main in
+      let datadir = Why3.Whyconf.datadir main in
+      { env = Why3.Env.create_env ld ; libdir ; datadir }
     end
 
 type context = {
   mutable th : Why3.Theory.theory_uc;
-  env: Why3.Env.env;
+  conf: why3_conf;
 }
 
 type convert = {
@@ -120,14 +128,14 @@ let fold_map map fold = function
 
 let empty_context name : context = {
   th = Why3.Theory.create_theory (Why3.Ident.id_fresh name);
-  env = get_why3_env ();
+  conf = get_why3_conf ();
 }
 
 let empty_cnv ?(polarity=`NoPolarity) (ctx:context) : convert = {
   th = ctx.th;
   subst = Lang.F.Tmap.empty;
   pool = Lang.F.pool ();
-  env = ctx.env;
+  env = ctx.conf.env;
   polarity;
   incomplete_symbols = Hashtbl.create 3;
   incomplete_types = Hashtbl.create 3;
@@ -779,7 +787,7 @@ class visitor (ctx:context) c =
         (if import then "import" else "")
         Why3.Pp.(print_list (Why3.Pp.constant_string ".") string) file
         thy name ;
-      let thy = Why3.Env.read_theory ctx.env file thy in
+      let thy = Why3.Env.read_theory ctx.conf.env file thy in
       let th = ctx.th in
       let th = Why3.Theory.open_scope th name in
       let th = Why3.Theory.use_export th thy in
@@ -1153,7 +1161,7 @@ type prover_call = {
   mutable killed : bool ;
 }
 
-let ping_prover_call p =
+let ping_prover_call ~libdir p =
   match Why3.Call_provers.query_call p.call with
   | NoUpdates
   | ProverStarted ->
@@ -1170,7 +1178,7 @@ let ping_prover_call p =
               Wp_parameters.debug ~dkey
                 "Hard Kill (late why3server timeout)" ;
               p.interrupted <- true ;
-              Why3.Call_provers.interrupt_call p.call ;
+              Why3.Call_provers.interrupt_call ~libdir p.call ;
             end
     in Task.Wait 100
   | InternalFailure exn ->
@@ -1205,7 +1213,8 @@ let ping_prover_call p =
       VCS.pp_result r;
     Task.Return (Task.Result r)
 
-let call_prover_task ~timeout ~steps prover call =
+let call_prover_task ~timeout ~steps ~conf prover call =
+  let libdir = conf.libdir in
   Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %d, steps %d@."
     Why3.Whyconf.print_prover prover
     (Why3.Opt.get_def (-1) timeout)
@@ -1220,9 +1229,9 @@ let call_prover_task ~timeout ~steps prover call =
   let ping = function
     | Task.Kill ->
       pcall.killed <- true ;
-      Why3.Call_provers.interrupt_call call ;
+      Why3.Call_provers.interrupt_call ~libdir call ;
       Task.Yield
-    | Task.Coin -> ping_prover_call pcall
+    | Task.Coin -> ping_prover_call ~libdir pcall
   in
   Task.async ping
 
@@ -1243,7 +1252,7 @@ let digest wpo drv prover task =
       end
   in Digest.file file |> Digest.to_hex
 
-let batch pconf driver ?script ~timeout ~steplimit prover task =
+let batch pconf driver ~conf ?script ~timeout ~steplimit prover task =
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
   let limit =
     let memlimit = Why3.Whyconf.memlimit (Why3.Whyconf.get_main (Why3Provers.config ())) in
@@ -1261,8 +1270,8 @@ let batch pconf driver ?script ~timeout ~steplimit prover task =
   let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
   let inplace = if script <> None then Some true else None in
   let call = Why3.Driver.prove_task_prepared ?old:script ?inplace
-      ~command ~limit driver task in
-  call_prover_task ~timeout ~steps prover call
+      ~command ~limit ~libdir:conf.libdir ~datadir:conf.datadir driver task in
+  call_prover_task ~conf ~timeout ~steps prover call
 
 (* -------------------------------------------------------------------------- *)
 (* --- Interactive Prover (Coq)                                           --- *)
@@ -1295,20 +1304,23 @@ let updatescript ~script driver task =
   let d_new = Digest.file script in
   if String.equal d_new d_old then Extlib.safe_remove backup
 
-let editor ~script ~merge wpo pconf driver prover task =
+let editor ~script ~merge ~conf wpo pconf driver prover task =
   Task.sync editor_mutex
     begin fun () ->
       Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
       Cache.clear_result ~digest:(digest wpo driver) prover task ;
       if merge then updatescript ~script driver task ;
       let command = editor_command pconf in
-      let call = Why3.Call_provers.call_editor ~command script in
-      call_prover_task ~timeout:None ~steps:None pconf.prover call
+      let call =
+        Why3.Call_provers.call_editor
+          ~command ~datadir:conf.datadir ~libdir:conf.libdir script
+      in
+      call_prover_task ~conf ~timeout:None ~steps:None pconf.prover call
     end
 
-let compile ~script ~timeout wpo pconf driver prover task =
+let compile ~script ~timeout ~conf wpo pconf driver prover task =
   let digest = digest wpo driver in
-  let runner = batch pconf driver ~script in
+  let runner = batch ~conf pconf driver ~script in
   Cache.get_result ~digest ~runner ~timeout ~steplimit:None prover task
 
 let prepare ~mode wpo driver task =
@@ -1329,33 +1341,34 @@ let prepare ~mode wpo driver task =
 let interactive ~mode wpo pconf driver prover task =
   let time = Wp_parameters.InteractiveTimeout.get () in
   let timeout = if time <= 0 then None else Some time in
+  let conf = get_why3_conf () in
   match prepare ~mode wpo driver task with
   | None -> Task.return VCS.unknown
   | Some (script, merge) ->
     match mode with
     | VCS.Batch ->
-      compile ~script ~timeout wpo pconf driver prover task
+      compile ~script ~timeout ~conf wpo pconf driver prover task
     | VCS.Update ->
       if merge then updatescript ~script driver task ;
-      compile ~script ~timeout wpo pconf driver prover task
+      compile ~script ~timeout ~conf wpo pconf driver prover task
     | VCS.Edit ->
       let open Task in
-      editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
-      compile ~script ~timeout wpo pconf driver prover task
+      editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+      compile ~script ~timeout ~conf wpo pconf driver prover task
     | VCS.Fix ->
       let open Task in
-      compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+      compile ~script ~timeout ~conf wpo pconf driver prover task >>= fun r ->
       if VCS.is_valid r then return r else
-        editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
-        compile ~script ~timeout wpo pconf driver prover task
+        editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+        compile ~script ~timeout ~conf wpo pconf driver prover task
     | VCS.FixUpdate ->
       let open Task in
       if merge then updatescript ~script driver task ;
-      compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+      compile ~script ~timeout ~conf wpo pconf driver prover task >>= fun r ->
       if VCS.is_valid r then return r else
         let merge = false in
-        editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
-        compile ~script ~timeout wpo pconf driver prover task
+        editor ~script ~merge ~conf wpo pconf driver prover task >>= fun _ ->
+        compile ~script ~timeout ~conf wpo pconf driver prover task
 
 (* -------------------------------------------------------------------------- *)
 (* --- Prove WPO                                                          --- *)
@@ -1373,8 +1386,8 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
     if Wp_parameters.Generate.get ()
     then Task.return VCS.no_result (* Only generate *)
     else
-      let env = WpContext.on_context context get_why3_env () in
-      let drv , pconf , task = prover_task env prover task in
+      let conf = WpContext.on_context context get_why3_conf () in
+      let drv , pconf , task = prover_task conf.env prover task in
       if is_trivial task then
         Task.return VCS.valid
       else
@@ -1383,7 +1396,7 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
       else
         Cache.get_result
           ~digest:(digest wpo drv)
-          ~runner:(batch pconf drv ?script:None)
+          ~runner:(batch ~conf pconf drv ?script:None)
           ~timeout ~steplimit prover task
   with exn ->
     if Wp_parameters.has_dkey dkey_api then
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 8df1b3908a149065d28db136450806405afc82dc..7e5c762776d40df8c7321adb2597fdb72328c1f7 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -57,14 +57,14 @@ case $WHY3VERSION in
         plugin_disable(wp,[why3 not found])
         ;;
       0.* | 1.[[0123]].*)
-        AC_MSG_RESULT([found $WHY3VERSION: requires 1.4.0+])
+        AC_MSG_RESULT([found $WHY3VERSION: requires 1.5.0+])
         plugin_disable(wp,[non-supported why3 $WHY3VERSION])
         ;;
-      1.4.*)
+      1.5.*)
         AC_MSG_RESULT([found $WHY3VERSION: ok])
         ;;
       *)
-        AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.4.0+)])
+        AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.5.0+)])
         ;;
 esac
 fi
diff --git a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
index e2ecb2158690c4c94a95668c87a9268fd4ee92e2..ad74ce62fd60dd44ff2ec66b030b29c1b9d017f1 100644
--- a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
+++ b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
@@ -1,60 +1,60 @@
 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.
 
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index b01d3e9c63ef85cdfcb16c2ae11da55dc0141dc7..efd2e9f9df793726354d9a57d5856a32742bedf2 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -57,7 +57,7 @@ end
        let m3 = set m2 (shift_sint32 a 3) (get m2 a2) in
        0 <= i1 ->
        0 <= i ->
-       region (base a) <= 0 ->
+       region (a.base) <= 0 ->
        i1 <= 9 ->
        i <= 9 ->
        linked t ->
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index 58865eff22dc2d0733b3c82c8270a883ca4ae487..2067e2fba853bee466f0b264d6e023006ef6e01b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -75,13 +75,13 @@ theory A_Occ
   
   (* use Chunk *)
   
-  Q_empty :
+  axiom Q_empty :
     forall mint:addr -> int, v:int, p:addr, f:int, t:int.
      t <= f -> is_sint32_chunk mint -> is_sint32 v -> L_occ mint v p f t = 0
   
   (* use Compound *)
   
-  Q_is :
+  axiom Q_is :
     forall mint:addr -> int, v:int, p:addr, f:int, t:int.
      let x = (- 1) + t in
      let x1 = get mint (shift_sint32 p x) in
@@ -91,7 +91,7 @@ theory A_Occ
      is_sint32 v ->
      is_sint32 x1 -> (1 + L_occ mint v p f x) = L_occ mint v p f t
   
-  Q_isnt :
+  axiom Q_isnt :
     forall mint:addr -> int, v:int, p:addr, f:int, t:int.
      let x = (- 1) + t in
      let x1 = get mint (shift_sint32 p x) in
@@ -154,7 +154,7 @@ end
       forall t:addr -> int, a:addr, i:int, i1:int, i2:int, i3:int.
        i3 <= i1 ->
        i < i3 ->
-       region (base a) <= 0 ->
+       region (a.base) <= 0 ->
        is_sint32_chunk t ->
        is_uint32 i3 ->
        is_uint32 i1 ->
@@ -233,14 +233,14 @@ theory A_Occ1
   
   (* use Chunk1 *)
   
-  Q_empty1 :
+  axiom Q_empty1 :
     forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
      t <=' f ->
      is_sint32_chunk1 mint -> is_sint321 v -> L_occ1 mint v p f t = 0
   
   (* use Compound1 *)
   
-  Q_is1 :
+  axiom Q_is1 :
     forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
      let x = (- 1) +' t in
      let x1 = get1 mint (shift_sint321 p x) in
@@ -250,7 +250,7 @@ theory A_Occ1
      is_sint321 v ->
      is_sint321 x1 -> (1 +' L_occ1 mint v p f x) = L_occ1 mint v p f t
   
-  Q_isnt1 :
+  axiom Q_isnt1 :
     forall mint:addr1 -> int, v:int, p:addr1, f:int, t:int.
      let x = (- 1) +' t in
      let x1 = get1 mint (shift_sint321 p x) in
@@ -315,7 +315,7 @@ end
        let x = (- 1) +' i1 in
        not get1 t (shift_sint321 a x) = i2 ->
        i <' i1 ->
-       region1 (base1 a) <=' 0 ->
+       region1 (a.base1) <=' 0 ->
        i1 <=' 1000 ->
        is_sint32_chunk1 t ->
        is_uint321 i1 ->
@@ -392,14 +392,14 @@ theory A_Occ2
   
   (* use Chunk2 *)
   
-  Q_empty2 :
+  axiom Q_empty2 :
     forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
      t <='' f ->
      is_sint32_chunk2 mint -> is_sint322 v -> L_occ2 mint v p f t = 0
   
   (* use Compound2 *)
   
-  Q_is2 :
+  axiom Q_is2 :
     forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
      let x = (- 1) +'' t in
      let x1 = get2 mint (shift_sint322 p x) in
@@ -409,7 +409,7 @@ theory A_Occ2
      is_sint322 v ->
      is_sint322 x1 -> (1 +'' L_occ2 mint v p f x) = L_occ2 mint v p f t
   
-  Q_isnt2 :
+  axiom Q_isnt2 :
     forall mint:addr2 -> int, v:int, p:addr2, f:int, t:int.
      let x = (- 1) +'' t in
      let x1 = get2 mint (shift_sint322 p x) in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 982b66a1342f47f627b60d988b9cc4890a35b48a..4469b4881435e5e65c5c1203e12cd5c46261760d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -138,42 +138,42 @@ end
       forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
     
     predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
-      addr) (begin:int) (end1:int) =
+      addr) (begin1:int) (end1:int) =
       forall i:int.
-       begin <= i ->
+       begin1 <= i ->
        i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
     
     predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
-      (begin:int) (i:int) (j:int) (end1:int) =
+      (begin1:int) (i:int) (j:int) (end1:int) =
       ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
           get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
-         begin <= i) /\
+         begin1 <= i) /\
         i < j) /\
        j < end1) /\
       (forall i1:int.
         not i1 = i ->
         not j = i1 ->
-        begin <= i1 ->
+        begin1 <= i1 ->
         i1 < end1 ->
         get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
     
     inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
       | Q_refl :
-          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
            int, end1:int.
-           P_same_array mint mint1 a b begin end1 ->
-           P_same_elements mint mint1 a b begin end1
+           P_same_array mint mint1 a b begin1 end1 ->
+           P_same_elements mint mint1 a b begin1 end1
       | Q_swap :
-          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
            int, i:int, j:int, end1:int.
-           P_swap mint mint1 a b begin i j end1 ->
-           P_same_elements mint mint1 a b begin end1
+           P_swap mint mint1 a b begin1 i j end1 ->
+           P_same_elements mint mint1 a b begin1 end1
       | Q_trans :
           forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
-           addr, b:addr, c:addr, begin:int, end1:int.
-           P_same_elements mint mint1 b c begin end1 ->
-           P_same_elements mint1 mint2 a b begin end1 ->
-           P_same_elements mint mint2 a c begin end1
+           addr, b:addr, c:addr, begin1:int, end1:int.
+           P_same_elements mint mint1 b c begin1 end1 ->
+           P_same_elements mint1 mint2 a b begin1 end1 ->
+           P_same_elements mint mint2 a c begin1 end1
     
     goal wp_goal :
       forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
index 67a25621bb869debb0266cef37f13f481f8aa753..fa26e5047b49c275c7402b281b9632446b4fd3d9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle
@@ -22,13 +22,14 @@
     
     predicate P_RP int
     
-    P_RP_def : forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
+    axiom P_RP_def :
+      forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
     
     function L_F (i:int) : int = 2 * i
     
     function L_RF int : int
     
-    L_RF_def :
+    axiom L_RF_def :
       forall i:int. L_RF i = (if i <= 0 then 0 else L_F i + L_RF ((- 1) + i))
     
     goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index aa0c561557224e54f9a9f121b341bba3912c6f50..df29522c76ece81e57062b386000ae24c92c0429 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -89,13 +89,13 @@ theory Compound
     Init_S1_X1 (get init (shiftfield_F1_X_a p))
     (get init (shiftfield_F1_X_b p)) (get init (shiftfield_F1_X_c p))
   
-  Q_Load_S1_X_update_Mchar0 :
+  axiom Q_Load_S1_X_update_Mchar0 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
      addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
      separated p 3 q 1 ->
      Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
   
-  Q_Load_S1_X_eqmem_Mchar0 :
+  axiom Q_Load_S1_X_eqmem_Mchar0 :
     forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
      addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
      eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
@@ -104,21 +104,21 @@ theory Compound
      eqmem mchar mchar1 q n ->
      Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
   
-  Q_Load_S1_X_havoc_Mchar0 :
+  axiom Q_Load_S1_X_havoc_Mchar0 :
     forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
      addr -> int, n:int, p:addr, q:addr
      [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
      separated p 3 q n ->
-     Load_S1_X p (havoc mchar1 mchar q n) mint mint1
-     = Load_S1_X p mchar mint mint1
+     Load_S1_X p (havoc mchar1 mchar q n) mint mint1 =
+     Load_S1_X p mchar mint mint1
   
-  Q_Load_S1_X_update_Mint1 :
+  axiom Q_Load_S1_X_update_Mint1 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
      addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
      separated p 3 q 1 ->
      Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
   
-  Q_Load_S1_X_eqmem_Mint1 :
+  axiom Q_Load_S1_X_eqmem_Mint1 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
      -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
      eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
@@ -127,21 +127,21 @@ theory Compound
      eqmem mint1 mint2 q n ->
      Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
   
-  Q_Load_S1_X_havoc_Mint1 :
+  axiom Q_Load_S1_X_havoc_Mint1 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
      -> int, n:int, p:addr, q:addr
      [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
      separated p 3 q n ->
-     Load_S1_X p mchar (havoc mint2 mint1 q n) mint
-     = Load_S1_X p mchar mint1 mint
+     Load_S1_X p mchar (havoc mint2 mint1 q n) mint =
+     Load_S1_X p mchar mint1 mint
   
-  Q_Load_S1_X_update_Mint2 :
+  axiom Q_Load_S1_X_update_Mint2 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
      addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
      separated p 3 q 1 ->
      Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
   
-  Q_Load_S1_X_eqmem_Mint2 :
+  axiom Q_Load_S1_X_eqmem_Mint2 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
      -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
      eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
@@ -150,28 +150,28 @@ theory Compound
      eqmem mint1 mint2 q n ->
      Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
   
-  Q_Load_S1_X_havoc_Mint2 :
+  axiom Q_Load_S1_X_havoc_Mint2 :
     forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
      -> int, n:int, p:addr, q:addr
      [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
      separated p 3 q n ->
-     Load_S1_X p mchar mint (havoc mint2 mint1 q n)
-     = Load_S1_X p mchar mint mint1
+     Load_S1_X p mchar mint (havoc mint2 mint1 q n) =
+     Load_S1_X p mchar mint mint1
   
-  Q_Load_Init_S1_X_update_Init0 :
+  axiom Q_Load_Init_S1_X_update_Init0 :
     forall init:addr -> bool, p:addr, q:addr, v:bool
      [Load_Init_S1_X p (set init q v)].
      separated p 3 q 1 ->
      Load_Init_S1_X p (set init q v) = Load_Init_S1_X p init
   
-  Q_Load_Init_S1_X_eqmem_Init0 :
+  axiom Q_Load_Init_S1_X_eqmem_Init0 :
     forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
      [Load_Init_S1_X p init, eqmem init init1 q n| Load_Init_S1_X p init1,
      eqmem init init1 q n].
      included p 3 q n ->
      eqmem init init1 q n -> Load_Init_S1_X p init1 = Load_Init_S1_X p init
   
-  Q_Load_Init_S1_X_havoc_Init0 :
+  axiom Q_Load_Init_S1_X_havoc_Init0 :
     forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
      [Load_Init_S1_X p (havoc init1 init q n)].
      separated p 3 q n ->
@@ -236,7 +236,7 @@ end
       forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3:
        addr -> int, t4:addr -> int, a:addr.
        Load_Init_S1_X a t = x ->
-       region (base a) <= 0 ->
+       region (a.base) <= 0 ->
        is_sint16_chunk t3 ->
        is_sint32_chunk t4 ->
        is_sint8_chunk t2 ->
@@ -272,7 +272,7 @@ end
     goal wp_goal :
       forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
        addr -> int, a:addr, x:S1_X.
-       region (base a) <= 0 ->
+       region (a.base) <= 0 ->
        IsS1_X x ->
        is_sint16_chunk t3 ->
        is_sint32_chunk t4 ->
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index fe74a260b12b87a301e7cc4bbddfbdc4cc00bd2c..c8d3f169d3faade2e0c503923e59a7f7ccb141d4 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -59,19 +59,19 @@ theory Compound
   
   function shiftfield_F1_FD_pos (p:addr) : addr = shift p 0
   
-  Q_Load_S2_A_update_Mint0 :
+  axiom Q_Load_S2_A_update_Mint0 :
     forall mint:addr -> int, p:addr, q:addr, v:int
      [Load_S2_A p (set mint q v)].
      not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
   
-  Q_Load_S2_A_eqmem_Mint0 :
+  axiom Q_Load_S2_A_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
      eqmem mint mint1 q n].
      included p 1 q n ->
      eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
   
-  Q_Load_S2_A_havoc_Mint0 :
+  axiom Q_Load_S2_A_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p (havoc mint1 mint q n)].
      separated p 1 q n ->
@@ -104,8 +104,8 @@ end
        let a3 = Load_S2_A a t in
        let a4 = Load_S2_A a (set (havoc t1 t a 1) a2 i) in
        not x = i ->
-       region (base a1) <= 0 ->
-       region (base a) <= 0 ->
+       region (a1.base) <= 0 ->
+       region (a.base) <= 0 ->
        is_sint32 i -> IsS2_A a3 -> is_sint32 x -> IsS2_A a4 -> EqS2_A a4 a3
   end
 [wp] 1 goal generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 973a39e45fa5af1ba55ed02d29a1bfe1666b0a7a..25cdbf437dc4817a633ae894932889549b4a583c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -101,42 +101,42 @@ end
        P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node
     
     predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
-      addr) (begin:int) (end1:int) =
+      addr) (begin1:int) (end1:int) =
       forall i:int.
-       begin <= i ->
+       begin1 <= i ->
        i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
     
     predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
-      (begin:int) (i:int) (j:int) (end1:int) =
+      (begin1:int) (i:int) (j:int) (end1:int) =
       ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
           get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
-         begin <= i) /\
+         begin1 <= i) /\
         i < j) /\
        j < end1) /\
       (forall i1:int.
         not i1 = i ->
         not j = i1 ->
-        begin <= i1 ->
+        begin1 <= i1 ->
         i1 < end1 ->
         get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
     
     inductive P_same_elements (addr -> int) (addr -> int) addr addr int int =
       | Q_refl :
-          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
            int, end1:int.
-           P_same_array mint mint1 a b begin end1 ->
-           P_same_elements mint mint1 a b begin end1
+           P_same_array mint mint1 a b begin1 end1 ->
+           P_same_elements mint mint1 a b begin1 end1
       | Q_swap :
-          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:
+          forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin1:
            int, i:int, j:int, end1:int.
-           P_swap mint mint1 a b begin i j end1 ->
-           P_same_elements mint mint1 a b begin end1
+           P_swap mint mint1 a b begin1 i j end1 ->
+           P_same_elements mint mint1 a b begin1 end1
       | Q_trans :
           forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:
-           addr, b:addr, c:addr, begin:int, end1:int.
-           P_same_elements mint mint1 b c begin end1 ->
-           P_same_elements mint1 mint2 a b begin end1 ->
-           P_same_elements mint mint2 a c begin end1
+           addr, b:addr, c:addr, begin1:int, end1:int.
+           P_same_elements mint mint1 b c begin1 end1 ->
+           P_same_elements mint1 mint2 a b begin1 end1 ->
+           P_same_elements mint mint2 a c begin1 end1
     
     goal wp_goal :
       forall t:addr -> int, t1:addr -> int, a:addr, a1:addr, i:int, i1:int, i2:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 70fd22d935e3729b93f16fb6b817a9b65b97d11a..29f604c34eaf0c3f72c10cc6cee353d6b77e173e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/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] 1 goal generated
 ------------------------------------------------------------
@@ -162,7 +162,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] 1 goal generated
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index fc2bd44fdd5bf6ac2dc4cfe36213ff7ff1950c6a..bdae904b176d5799a42a2c3f84f8b6190c311e27 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/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
 ----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index ff97bc71c534b5b33638bfe120f1c0de928f8e66..16921421e1bdbcb0a10f13b41d0179b4f67afae7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/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
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index 324a789c9b982c3478ddd70178df49f3c1c4adc5..268995c9ffb2bf6b68baaf179a0d0a43b0f371ee 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -103,61 +103,61 @@ theory Compound
     (Array_uint32 (shiftfield_F1_S_a p) 5 mint)
     (Array_sint64 (shiftfield_F1_S_b p) 5 mint2)
   
-  Q_Array_uint32_access :
+  axiom Q_Array_uint32_access :
     forall mint:addr -> int, i:int, n:int, p:addr
      [get (Array_uint32 p n mint) i].
      0 <= i ->
      i < n -> get (Array_uint32 p n mint) i = get mint (shift_uint32 p i)
   
-  Q_Array_uint32_update_Mint0 :
+  axiom Q_Array_uint32_update_Mint0 :
     forall mint:addr -> int, n:int, p:addr, q:addr, v:int
      [Array_uint32 p n (set mint q v)].
      not q = p -> Array_uint32 p n (set mint q v) = Array_uint32 p n mint
   
-  Q_Array_uint32_eqmem_Mint0 :
+  axiom Q_Array_uint32_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
      [Array_uint32 p n mint, eqmem mint mint1 q n1| Array_uint32 p n mint1,
      eqmem mint mint1 q n1].
      included p 1 q n1 ->
      eqmem mint mint1 q n1 -> Array_uint32 p n mint1 = Array_uint32 p n mint
   
-  Q_Array_uint32_havoc_Mint0 :
+  axiom Q_Array_uint32_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
      [Array_uint32 p n (havoc mint1 mint q n1)].
      separated p 1 q n1 ->
      Array_uint32 p n (havoc mint1 mint q n1) = Array_uint32 p n mint
   
-  Q_Array_sint64_access :
+  axiom Q_Array_sint64_access :
     forall mint:addr -> int, i:int, n:int, p:addr
      [get (Array_sint64 p n mint) i].
      0 <= i ->
      i < n -> get (Array_sint64 p n mint) i = get mint (shift_sint64 p i)
   
-  Q_Array_sint64_update_Mint0 :
+  axiom Q_Array_sint64_update_Mint0 :
     forall mint:addr -> int, n:int, p:addr, q:addr, v:int
      [Array_sint64 p n (set mint q v)].
      not q = p -> Array_sint64 p n (set mint q v) = Array_sint64 p n mint
   
-  Q_Array_sint64_eqmem_Mint0 :
+  axiom Q_Array_sint64_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
      [Array_sint64 p n mint, eqmem mint mint1 q n1| Array_sint64 p n mint1,
      eqmem mint mint1 q n1].
      included p 1 q n1 ->
      eqmem mint mint1 q n1 -> Array_sint64 p n mint1 = Array_sint64 p n mint
   
-  Q_Array_sint64_havoc_Mint0 :
+  axiom Q_Array_sint64_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
      [Array_sint64 p n (havoc mint1 mint q n1)].
      separated p 1 q n1 ->
      Array_sint64 p n (havoc mint1 mint q n1) = Array_sint64 p n mint
   
-  Q_Load_S1_S_update_Mint0 :
+  axiom Q_Load_S1_S_update_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
      addr, v:int [Load_S1_S p (set mint q v) mint1 mint2].
      separated p 11 q 1 ->
      Load_S1_S p (set mint q v) mint1 mint2 = Load_S1_S p mint mint1 mint2
   
-  Q_Load_S1_S_eqmem_Mint0 :
+  axiom Q_Load_S1_S_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr [Load_S1_S p mint mint2 mint3,
      eqmem mint mint1 q n| Load_S1_S p mint1 mint2 mint3,
@@ -166,21 +166,21 @@ theory Compound
      eqmem mint mint1 q n ->
      Load_S1_S p mint1 mint2 mint3 = Load_S1_S p mint mint2 mint3
   
-  Q_Load_S1_S_havoc_Mint0 :
+  axiom Q_Load_S1_S_havoc_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr
      [Load_S1_S p (havoc mint1 mint q n) mint2 mint3].
      separated p 11 q n ->
-     Load_S1_S p (havoc mint1 mint q n) mint2 mint3
-     = Load_S1_S p mint mint2 mint3
+     Load_S1_S p (havoc mint1 mint q n) mint2 mint3 =
+     Load_S1_S p mint mint2 mint3
   
-  Q_Load_S1_S_update_Mint1 :
+  axiom Q_Load_S1_S_update_Mint1 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
      addr, v:int [Load_S1_S p mint2 (set mint1 q v) mint].
      separated p 11 q 1 ->
      Load_S1_S p mint2 (set mint1 q v) mint = Load_S1_S p mint2 mint1 mint
   
-  Q_Load_S1_S_eqmem_Mint1 :
+  axiom Q_Load_S1_S_eqmem_Mint1 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr [Load_S1_S p mint3 mint1 mint,
      eqmem mint1 mint2 q n| Load_S1_S p mint3 mint2 mint,
@@ -189,21 +189,21 @@ theory Compound
      eqmem mint1 mint2 q n ->
      Load_S1_S p mint3 mint2 mint = Load_S1_S p mint3 mint1 mint
   
-  Q_Load_S1_S_havoc_Mint1 :
+  axiom Q_Load_S1_S_havoc_Mint1 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr
      [Load_S1_S p mint3 (havoc mint2 mint1 q n) mint].
      separated p 11 q n ->
-     Load_S1_S p mint3 (havoc mint2 mint1 q n) mint
-     = Load_S1_S p mint3 mint1 mint
+     Load_S1_S p mint3 (havoc mint2 mint1 q n) mint =
+     Load_S1_S p mint3 mint1 mint
   
-  Q_Load_S1_S_update_Mint2 :
+  axiom Q_Load_S1_S_update_Mint2 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, p:addr, q:
      addr, v:int [Load_S1_S p mint1 mint (set mint2 q v)].
      separated p 11 q 1 ->
      Load_S1_S p mint1 mint (set mint2 q v) = Load_S1_S p mint1 mint mint2
   
-  Q_Load_S1_S_eqmem_Mint2 :
+  axiom Q_Load_S1_S_eqmem_Mint2 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr [Load_S1_S p mint1 mint mint2,
      eqmem mint2 mint3 q n| Load_S1_S p mint1 mint mint3,
@@ -212,13 +212,13 @@ theory Compound
      eqmem mint2 mint3 q n ->
      Load_S1_S p mint1 mint mint3 = Load_S1_S p mint1 mint mint2
   
-  Q_Load_S1_S_havoc_Mint2 :
+  axiom Q_Load_S1_S_havoc_Mint2 :
     forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, mint3:addr
      -> int, n:int, p:addr, q:addr
      [Load_S1_S p mint1 mint (havoc mint3 mint2 q n)].
      separated p 11 q n ->
-     Load_S1_S p mint1 mint (havoc mint3 mint2 q n)
-     = Load_S1_S p mint1 mint mint2
+     Load_S1_S p mint1 mint (havoc mint3 mint2 q n) =
+     Load_S1_S p mint1 mint mint2
 end
 [wp:print-generated] 
   theory WP
@@ -246,7 +246,7 @@ end
       forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, i:int.
        let a1 = Load_S1_S a t t2 t1 in
        let a2 = Load_S1_S a t (set t2 (shiftfield_F1_S_f a) i) t1 in
-       region (base a) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
+       region (a.base) <= 0 -> IsS1_S a1 -> IsS1_S a2 -> EqS1_S a2 a1
   end
 [wp] 1 goal generated
 ------------------------------------------------------------