diff --git a/convert.ml b/convert.ml
index 6497fb4bb997df1ea43ee31e63a0f810096eb30f..cc94061e7d74df70f95da7669eae7ed4c184d945 100644
--- a/convert.ml
+++ b/convert.ml
@@ -2257,7 +2257,7 @@ and convert_statement env st does_remove_virtual =
     | Code_annot (l,annot) ->
       let env = Convert_env.set_loc env l in
       let cloc = Convert_env.get_loc env in
-      let c_annot = Convert_acsl.convert_code_annot env annot in
+      let env, c_annot = Convert_acsl.convert_code_annot env annot in
       CODE_ANNOT(c_annot,cloc), env
     | Return (l,Some e) ->
       let e = add_temporary (* env *) e in
@@ -2385,7 +2385,9 @@ and convert_statement env st does_remove_virtual =
       let env, aux, cond = convert_full_expr env cond does_remove_virtual in
       let body,env = convert_statement env body does_remove_virtual in
       let body = add_temps_update aux body in
-      let annot = List.map (Convert_acsl.convert_code_annot env) annot in
+      let env, annot =
+        Convert_env.env_map Convert_acsl.convert_code_annot env annot
+      in
       add_temps aux (WHILE(annot,cond,body,cloc)), env
     | DoWhile (loc, cond, body,annot) ->
       let env = Convert_env.set_loc env loc in
@@ -2393,7 +2395,9 @@ and convert_statement env st does_remove_virtual =
       let env, aux, cond = convert_full_expr env cond does_remove_virtual in
       let body, env = convert_statement env body does_remove_virtual in
       let body = add_temps_update aux body in
-      let annot = List.map (Convert_acsl.convert_code_annot env) annot in
+      let env, annot =
+        Convert_env.env_map Convert_acsl.convert_code_annot env annot
+      in
       add_temps aux (DOWHILE(annot, cond, body, cloc)), env
     | For(loc, init, cond, incr, body,annot) ->
       let env = Convert_env.set_loc env loc in
@@ -2408,7 +2412,9 @@ and convert_statement env st does_remove_virtual =
       let ienv, incr =
         convert_incr_statement ienv incr does_remove_virtual
       in
-      let annot = List.map (Convert_acsl.convert_code_annot ienv) annot in
+      let ienv, annot =
+        Convert_env.env_map Convert_acsl.convert_code_annot ienv annot
+      in
       let body, ienv = convert_statement ienv body does_remove_virtual in
       let body = add_temps_update aux body in
       let loop = FOR(annot,init,cond,incr,body,cloc) in
@@ -3519,8 +3525,9 @@ let add_arg_names l =
           l))
 
 let convert_contract env spec =
-  Convert_acsl.convert_function_contract env spec,
-  Convert_env.get_loc env
+  let loc = Convert_env.get_loc env in
+  let env, spec = Convert_acsl.convert_function_contract env spec in
+  env, (spec, loc)
 
 let constify_receiver kind args =
   match kind, args with
@@ -3565,7 +3572,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
       let signature = {result= return_type; parameter= args_sig; variadic } in
       let signature = Convert_env.signature_normalize env signature in
       let name = Mangling.mangle qname tkind (Some(kind,signature)) in
-      let spec = Option.map (convert_contract benv) spec in
+      let benv, spec = Convert_env.env_opt convert_contract benv spec in
       let extern_c = false in
       let spec =
         if has_further_definition
@@ -3731,7 +3738,7 @@ and convert_class_component (env, implicits, types, fields, others) meth =
        fields, others)
     | Class_annot(loc,annot) ->
       let env = Convert_env.set_loc env loc in
-      let annot = Convert_acsl.convert_annot env annot in
+      let env, annot = Convert_acsl.convert_annot env annot in
       (env,implicits,types,fields,GLOBANNOT [annot]:: others)
 
 and convert_class env name tkind kind inherits body has_virtual =
@@ -3899,7 +3906,7 @@ let rec convert_global env glob =
   match glob with
     | GlobalAnnotation(loc,annot) ->
       let env = Convert_env.set_loc env loc in
-      let annot = Convert_acsl.convert_annot env annot in
+      let env, annot = Convert_acsl.convert_annot env annot in
       Convert_env.add_c_global env (GLOBANNOT [annot])
     | Function (name, _, _, _, _, _, _, _, _, _, _, _, _)
         when do_not_translate name
@@ -3935,7 +3942,7 @@ let rec convert_global env glob =
           let signature = Convert_env.signature_normalize env signature in
           Mangling.mangle qualified_name tkind (Some (kind, signature))
       in
-      let spec = Option.map (convert_contract benv) spec in
+      let benv, spec = Convert_env.env_opt convert_contract benv spec in
       let implicit = false in
       let spec =
         if has_further_definition then spec
diff --git a/convert_acsl.ml b/convert_acsl.ml
index cd5be7310ec0336d671d1199690c1e56eccfb0b8..8e0f9dccc23bcd0249e4a623fd22d0104e6140cc 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -42,22 +42,24 @@ let convert_logic_label_opt = function
   | Some lab -> Some (convert_logic_label lab)
   | None -> None
 
-let convert_ikind = function
-  | IBool -> Cil_types.IBool
-  | IChar_u | IChar_s | IChar -> Cil_types.IChar
-  | IUChar -> Cil_types.IUChar
-  | ISChar -> Cil_types.ISChar
-  | IChar16 -> Cil.intKindForSize 2 true
-  | IChar32 -> Cil.intKindForSize 4 true
-  | IWChar_u | IWChar_s | IWChar -> Cil.theMachine.Cil.wcharKind
-  | IShort -> Cil_types.IShort
-  | IUShort -> Cil_types.IUShort
-  | IInt -> Cil_types.IInt
-  | IUInt -> Cil_types.IUInt
-  | ILong -> Cil_types.ILong
-  | IULong -> Cil_types.IULong
-  | ILongLong -> Cil_types.ILongLong
-  | IULongLong -> Cil_types.IULongLong
+let convert_ikind env = function
+  | IBool -> env, LTint Cil_types.IBool
+  | IChar_u | IChar_s | IChar -> env, LTint Cil_types.IChar
+  | IUChar -> env, LTint Cil_types.IUChar
+  | ISChar -> env, LTint Cil_types.ISChar
+  | IChar16 -> env, LTint (Cil.intKindForSize 2 true)
+  | IChar32 -> env, LTint (Cil.intKindForSize 4 true)
+  | IWChar_u | IWChar_s | IWChar ->
+    let env = Convert_env.memo_wchar env in
+    env, LTnamed ("wchar_t", [])
+  | IShort -> env, LTint Cil_types.IShort
+  | IUShort -> env, LTint Cil_types.IUShort
+  | IInt -> env, LTint Cil_types.IInt
+  | IUInt -> env, LTint Cil_types.IUInt
+  | ILong -> env, LTint Cil_types.ILong
+  | IULong -> env, LTint Cil_types.IULong
+  | ILongLong -> env, LTint Cil_types.ILongLong
+  | IULongLong -> env, LTint Cil_types.IULongLong
 
 let convert_fkind = function
   | FFloat -> Cil_types.FFloat
@@ -86,47 +88,47 @@ let convert_cst_array_size env = function
     Frama_Clang_option.fatal "Unexpected value as array dimension"
 
 let rec convert_logic_type env = function
-  | Lvoid -> LTvoid
-  | Lint ik -> LTint (convert_ikind ik)
-  | Lfloat fk -> LTfloat (convert_fkind fk)
+  | Lvoid -> env, LTvoid
+  | Lint ik -> convert_ikind env ik
+  | Lfloat fk -> env, LTfloat (convert_fkind fk)
   | Larray (t,dim) ->
-    let t = convert_logic_type env t in
+    let env, t = convert_logic_type env t in
     let dim =
       match dim with
       | Some dim -> convert_cst_array_size env dim
       | None -> ASnone
     in
-    LTarray(t,dim)
+    env, LTarray(t,dim)
   | Lpointer t | Lreference t ->
-    let t = convert_logic_type env t in
-    LTpointer t
+    let env, t = convert_logic_type env t in
+    env, LTpointer t
   | Lenum e ->
     let e, tk = Convert_env.typedef_normalize env e TStandard
-    in LTenum (Mangling.mangle e tk None)
+    in env, LTenum (Mangling.mangle e tk None)
   | Lstruct (s,t) ->
     let s,t = Convert_env.typedef_normalize env s t in
     let cname =
       if Convert_env.is_extern_c_aggregate env s t then s.decl_name
       else Mangling.mangle s t None
     in
-    LTstruct cname
+    env, LTstruct cname
   | Lunion (u,t) ->
     let u, t = Convert_env.typedef_normalize env u t in
     let cname =
       if Convert_env.is_extern_c_aggregate env u t then u.decl_name
       else Mangling.mangle u t None
     in
-    LTunion cname
+    env, LTunion cname
   | LCnamed (n,extern_c) ->
       let name = if extern_c then n.decl_name
       else (* change only the template parameters in the qualification *)
         let n, tk = Convert_env.typedef_normalize env n TStandard
         in Mangling.mangle n tk None
       in
-      LTnamed (name,[])
+      env, LTnamed (name,[])
   | Lnamed({ prequalification = [QNamespace "Utf8_logic"];
              decl_name = "boolean"},_,[]) ->
-      LTnamed (Utf8_logic.boolean,[])
+      env, LTnamed (Utf8_logic.boolean,[])
   | Lnamed(t,extern_c,args) ->
     let name =
       if extern_c then t.decl_name
@@ -134,17 +136,19 @@ let rec convert_logic_type env = function
         let t, tk = Convert_env.typedef_normalize env t TStandard
         in Mangling.mangle t tk None
     in
-    let args = List.map (convert_logic_type env) args in
-    LTnamed(name,args)
-  | Lvariable s -> LTnamed(s.decl_name,[])
-  | Linteger -> LTinteger
-  | Lreal -> LTreal
+    let env, args = Convert_env.env_map convert_logic_type env args in
+    env, LTnamed(name,args)
+  | Lvariable s -> env, LTnamed(s.decl_name,[])
+  | Linteger -> env, LTinteger
+  | Lreal -> env, LTreal
   | Larrow(args,rt) ->
-    let args = List.map (convert_logic_type env) args in
-    let rt = convert_logic_type env rt in
-    LTarrow(args, rt)
+    let env, args = Convert_env.env_map convert_logic_type env args in
+    let env, rt = convert_logic_type env rt in
+    env, LTarrow(args, rt)
 
-let convert_logic_param env p = (convert_logic_type env p.la_type, p.la_name)
+let convert_logic_param env p =
+  let env, typ = convert_logic_type env p.la_type in
+  env, (typ, p.la_name)
 
 type bkind = Relation | Logic | Arithmetic
 
@@ -189,9 +193,9 @@ let convert_rel = function
   | Rneq -> Neq
 
 let convert_var_decl env v =
-  let typ = convert_logic_type env v.lv_type in
+  let env, typ = convert_logic_type env v.lv_type in
   let name = v.logic_var_def_lv_name.decl_name in
-  (typ, name)
+  env, (typ, name)
 
 let convert_reference env typ e =
   match typ with
@@ -210,142 +214,155 @@ let convert_logic_reference env typ e =
 let rec convert_logic_expr env e =
   let env = Convert_env.set_loc env e.loc in
   let lexpr_loc = Convert_env.get_loc env in
-  let anonymous =
-    { lexpr_loc; lexpr_node = convert_logic_expr_node env e.node }
+  let env, lexpr_node = convert_logic_expr_node env e.node in
+  let anonymous = { lexpr_loc; lexpr_node } in
+  let res =
+    List.fold_right
+      (fun s res -> { lexpr_loc; lexpr_node = PLnamed(s,res) })
+      e.names anonymous
   in
-  List.fold_right
-    (fun s res -> { lexpr_loc; lexpr_node = PLnamed(s,res) })
-    e.names anonymous
+  env, res
 and convert_logic_expr_node env = function
-  | TConst c -> PLconstant(convert_logic_constant c)
+  | TConst c -> env, PLconstant(convert_logic_constant c)
   | TLval lv -> convert_logic_lval env lv
-  | TSizeOf t -> PLsizeof(convert_logic_type env t)
+  | TSizeOf t ->
+    let env, typ = convert_logic_type env t in
+    env, PLsizeof typ
   | TSizeOfStr s ->
     let cs =
       { lexpr_loc = Convert_env.get_loc env;
         lexpr_node = PLconstant(StringConstant s) }
     in
-    PLsizeofE(cs)
+    env, PLsizeofE(cs)
   | TUnOp((UOPostInc|UOPostDec|UOPreInc|UOPreDec),_) ->
     Convert_env.fatal env "Side effect operation in ACSL++ expression"
   | TUnOp((UOCastNoEffect _ | UOCastDeref | UOCastToVoid | UOCastInteger _
           | UOCastDerefInit | UOCastEnum _ | UOCastFloat _ | UOCastC _),_) ->
     Convert_env.fatal env
       "Logic casts are not supposed to use TUnOp but TCastE"
-  | TUnOp(UOOpposite,e) -> PLunop(Uminus,convert_logic_expr env e)
-  | TUnOp(UOBitNegate,e) -> PLunop(Ubw_not,convert_logic_expr env e)
-  | TUnOp(UOLogicalNegate,e) -> PLnot (convert_logic_expr env e)
+  | TUnOp(UOOpposite,e) ->
+    let env, e = convert_logic_expr env e in
+    env, PLunop(Uminus,e)
+  | TUnOp(UOBitNegate,e) ->
+    let env, e = convert_logic_expr env e in
+    env, PLunop(Ubw_not,e)
+  | TUnOp(UOLogicalNegate,e) ->
+    let env, e = convert_logic_expr env e in
+    env, PLnot e
   | TBinOp(bo,e1,e2) when bo_kind bo = Arithmetic ->
     let cbo = convert_bop_arith bo in
-    let ce1 = convert_logic_expr env e1 in
-    let ce2 = convert_logic_expr env e2 in
-    PLbinop(ce1,cbo,ce2)
+    let env, ce1 = convert_logic_expr env e1 in
+    let env, ce2 = convert_logic_expr env e2 in
+    env, PLbinop(ce1,cbo,ce2)
   | TBinOp(bo,e1,e2) when bo_kind bo = Relation ->
     let cbo = convert_bop_relation bo in
-    let ce1 = convert_logic_expr env e1 in
-    let ce2 = convert_logic_expr env e2 in
-    PLrel(ce1,cbo,ce2)
+    let env, ce1 = convert_logic_expr env e1 in
+    let env, ce2 = convert_logic_expr env e2 in
+    env, PLrel(ce1,cbo,ce2)
   | TBinOp(BOLogicalAnd,e1,e2) ->
-    let ce1 = convert_logic_expr env e1 in
-    let ce2 = convert_logic_expr env e2 in
-    PLand(ce1,ce2)
+    let env, ce1 = convert_logic_expr env e1 in
+    let env, ce2 = convert_logic_expr env e2 in
+    env, PLand(ce1,ce2)
   | TBinOp(BOLogicalOr,e1,e2) ->
-    let ce1 = convert_logic_expr env e1 in
-    let ce2 = convert_logic_expr env e2 in
-    PLor(ce1,ce2)
+    let env, ce1 = convert_logic_expr env e1 in
+    let env, ce2 = convert_logic_expr env e2 in
+    env, PLor(ce1,ce2)
   | TBinOp _ -> Convert_env.fatal env "Unknown binary operator in logic"
   | TCastE(typ,e) ->
-    let ctyp = convert_logic_type env typ in
-    let ce = convert_logic_expr env e in
-    PLcast(ctyp,ce)
+    let env, ctyp = convert_logic_type env typ in
+    let env, ce = convert_logic_expr env e in
+    env, PLcast(ctyp,ce)
   | TAddrOf lv | TStartOf lv ->
-    let e = convert_logic_lval env lv in
+    let env, e = convert_logic_lval env lv in
     (* simplify memory accesses introduced by handling of references *)
     (match e with
-      | PLunop(Ustar,t) -> t.lexpr_node
+      | PLunop(Ustar,t) -> env, t.lexpr_node
       | _ ->
         let e = { lexpr_node = e; lexpr_loc = Convert_env.get_loc env } in
-        PLunop(Uamp,e))
+        env, PLunop(Uamp,e))
   | TFieldAccess (e,(TField(f,TNoOffset)|TModel(f,TNoOffset))) ->
-    let ce = convert_logic_expr env e in PLdot(ce,f)
+    let env, ce = convert_logic_expr env e in env, PLdot(ce,f)
   | TFieldAccess _ ->
     Convert_env.fatal env "Unexpected offset in field access"
-  | TFalse -> PLfalse
-  | TTrue -> PLtrue
+  | TFalse -> env, PLfalse
+  | TTrue -> env, PLtrue
   | TApp(f,l,args,extern_c) ->
     (* TODO: if f is an extern C (or built-in), do not mangle it *)
-    let fname = if extern_c then f.decl_name
+    let fname =
+      if extern_c then f.decl_name
       else
         let f, t = Convert_env.typedef_normalize env f TStandard
-        in Mangling.mangle f t None in
+        in Mangling.mangle f t None
+    in
     let labels = List.map (fun l -> convert_logic_label l.snd) l in
-    let args = List.map (convert_logic_expr env) args in
-    PLapp(fname,labels,args)
+    let env, args = Convert_env.env_map convert_logic_expr env args in
+    env, PLapp(fname,labels,args)
   | TLambda (vars,t) ->
-    let quants = List.map (convert_var_decl env) vars in
-    let e = convert_logic_expr env t in
-    PLlambda(quants,e)
+    let env, quants = Convert_env.env_map convert_var_decl env vars in
+    let env, e = convert_logic_expr env t in
+    env, PLlambda(quants,e)
   | TDataCons(name,args) ->
     let name, t = Convert_env.typedef_normalize env name TStandard in
     let name = Mangling.mangle name t None in
-    let args = List.map (convert_logic_expr env) args in
-    PLapp(name,[],args)
+    let env, args = Convert_env.env_map convert_logic_expr env args in
+    env, PLapp(name,[],args)
   | TIf(cond,etrue,efalse) ->
-    let ccond = convert_logic_expr env cond in
-    let cetrue = convert_logic_expr env etrue in
-    let cefalse = convert_logic_expr env efalse in
-    PLif(ccond,cetrue,cefalse)
+    let env, ccond = convert_logic_expr env cond in
+    let env, cetrue = convert_logic_expr env etrue in
+    let env, cefalse = convert_logic_expr env efalse in
+    env, PLif(ccond,cetrue,cefalse)
   | TAt(t,l) ->
-    let t = convert_logic_expr env t in
+    let env, t = convert_logic_expr env t in
     let l = convert_logic_label l in
-    PLat(t,l)
+    env, PLat(t,l)
   | TBase_addr(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLbase_addr(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLbase_addr(l,t)
   | TOffset(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLoffset(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLoffset(l,t)
   | TBlock_length(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLblock_length(l,t)
-  | TNull -> PLnull
+    let env, t = convert_logic_expr env t in
+    env, PLblock_length(l,t)
+  | TNull -> env, PLnull
   | TLogic_coerce(_,t) ->
     (* should be transparent at the parsed logic tree level. *)
-    (convert_logic_expr env t).lexpr_node
+    let env, e = convert_logic_expr env t in
+    env, e.lexpr_node
   | TUpdate(obj,off,t) ->
-    let obj = convert_logic_expr env obj in
-    let path = path_of_offset env off in
-    let value = convert_logic_expr env t in
-    PLupdate(obj,path,PLupdateTerm value)
-  | TEmpty_set -> PLempty
+    let env, obj = convert_logic_expr env obj in
+    let env, path = path_of_offset env off in
+    let env, value = convert_logic_expr env t in
+    env, PLupdate(obj,path,PLupdateTerm value)
+  | TEmpty_set -> env, PLempty
   | TUnion l ->
-    let l = List.map (convert_logic_expr env) l in
-    PLunion l
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, PLunion l
   | TInter l ->
-    let l = List.map (convert_logic_expr env) l in
-    PLinter l
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, PLinter l
   | TComprehension (t,quants,pred) ->
-    let quants = List.map (convert_var_decl env) quants in
-    let t = convert_logic_expr env t in
-    let pred = Option.map (convert_pred_named env) pred in
-    PLcomprehension (t,quants,pred)
+    let env, quants = Convert_env.env_map convert_var_decl env quants in
+    let env, t = convert_logic_expr env t in
+    let env, pred = Convert_env.env_opt convert_pred_named env pred in
+    env, PLcomprehension (t,quants,pred)
   | TRange(l,h) ->
-    let l = Option.map (convert_logic_expr env) l in
-    let h = Option.map (convert_logic_expr env) h in
-    PLrange(l,h)
+    let env, l = Convert_env.env_opt convert_logic_expr env l in
+    let env, h = Convert_env.env_opt convert_logic_expr env h in
+    env, PLrange(l,h)
   | TLet(info,t) ->
-    let body = convert_inner_body env info in
+    let env, body = convert_inner_body env info in
     let name = info.li_name.decl_name in
-    let rest = convert_logic_expr env t in
-    PLlet(name,body,rest)
+    let env, rest = convert_logic_expr env t in
+    env, PLlet(name,body,rest)
   | TCoerce _ | TCoerceE _ ->
     Frama_Clang_option.not_yet_implemented "coercions"
 
 and convert_logic_lval env lv =
-  let base = convert_logic_lhost env lv.base_support in
+  let env, base = convert_logic_lhost env lv.base_support in
   convert_logic_offset env base lv.offset
 
 and convert_logic_lhost env = function
@@ -356,22 +373,22 @@ and convert_logic_lhost env = function
           Convert_env.get_global_var env v.logic_var_lv_name
         in
         let var = PLvar (convert_var env is_extern_c v) in
-        convert_reference env typ var
+        env, convert_reference env typ var
       | LVCLocal ->
         let var = PLvar v.logic_var_lv_name.decl_name in
         let typ = Convert_env.get_local_var env v.logic_var_lv_name.decl_name in
-        convert_reference env typ var
+        env, convert_reference env typ var
       | _ ->
-        PLvar v.logic_var_lv_name.decl_name
+        env, PLvar v.logic_var_lv_name.decl_name
     )
   | TCFun(n,s) ->
     let n, t = Convert_env.typedef_normalize env n TStandard
-    in PLvar (Mangling.mangle n t (Some (FKFunction,s)))
-  | TResult typ -> convert_logic_reference env typ PLresult
-  | TMem t -> let t = convert_logic_expr env t in PLunop(Ustar,t)
+    in env, PLvar (Mangling.mangle n t (Some (FKFunction,s)))
+  | TResult typ -> env, convert_logic_reference env typ PLresult
+  | TMem t -> let env, t = convert_logic_expr env t in env, PLunop(Ustar,t)
 
 and convert_logic_offset env base = function
-  | TNoOffset -> base
+  | TNoOffset -> env, base
   | TField(s,o) | TModel(s,o) ->
     let e = { lexpr_loc = Convert_env.get_loc env; lexpr_node = base } in
     let base = PLdot(e,s) in
@@ -391,144 +408,144 @@ and convert_logic_offset env base = function
       "casts to derived classes are not supported for the moment"
   | TIndex(t,o) ->
     let e = { lexpr_loc = Convert_env.get_loc env; lexpr_node = base } in
-    let i = convert_logic_expr env t in
+    let env, i = convert_logic_expr env t in
     let base = PLarrget(e,i) in
     convert_logic_offset env base o
 
 and path_of_offset env = function
-  | TNoOffset -> []
+  | TNoOffset -> env, []
   | TField(s,o) | TModel(s,o) ->
-    let path = path_of_offset env o in
-    PLpathField s :: path
+    let env, path = path_of_offset env o in
+    env, PLpathField s :: path
   | TBase(b,t,o) ->
-    let path = path_of_offset env o in
+    let env, path = path_of_offset env o in
     let b, t = Convert_env.typedef_normalize env b t in
-    PLpathField ("_frama_c_" ^ Mangling.mangle b t None) :: path
+    env, PLpathField ("_frama_c_" ^ Mangling.mangle b t None) :: path
   | TVirtualBase(b,t,o) ->
-    let path = path_of_offset env o in
+    let env, path = path_of_offset env o in
     let b, t = Convert_env.typedef_normalize env b t in
-    PLpathField ("_frama_c_" ^ Mangling.mangle b t None) :: path
+    env, PLpathField ("_frama_c_" ^ Mangling.mangle b t None) :: path
   | TDerived(_ (* d *),_ (* td *),_ (* b *),_ (* tb *),_ (* o *)) ->
     Convert_env.fatal env
       "casts to derived classes are not supported for the moment"
   | TIndex(t,o) ->
-    let i = convert_logic_expr env t in
-    let path = path_of_offset env o in
-    PLpathIndex(i) :: path
+    let env, i = convert_logic_expr env t in
+    let env, path = path_of_offset env o in
+    env, PLpathIndex(i) :: path
 
 and convert_pred_named env p =
   let env = Convert_env.set_loc env p.pred_loc in
   let pred_loc = Convert_env.get_loc env in
-  let cp = convert_pred env p.pred_content in
+  let env, cp = convert_pred env p.pred_content in
   let cp =
     List.fold_right
       (fun s acc -> PLnamed(s,{ lexpr_node = acc; lexpr_loc = pred_loc }))
       p.pred_name cp
   in
-  { lexpr_node = cp; lexpr_loc = pred_loc }
+  env, { lexpr_node = cp; lexpr_loc = pred_loc }
 
 and convert_pred env = function
-  | Pfalse -> PLfalse
-  | Ptrue -> PLtrue
+  | Pfalse -> env, PLfalse
+  | Ptrue -> env, PLtrue
   | PApp(p,labs,args,is_extern_c) ->
     let pname = if is_extern_c then p.decl_name
     else
       let p, t = Convert_env.typedef_normalize env p TStandard in
       Mangling.mangle p t None
     in let clabs = List.map (fun l -> convert_logic_label l.snd) labs in
-    let cargs = List.map (convert_logic_expr env) args in
-    PLapp(pname,clabs,cargs)
+    let env, cargs = Convert_env.env_map convert_logic_expr env args in
+    env, PLapp(pname,clabs,cargs)
   | Pseparated l ->
-    let l = List.map (convert_logic_expr env) l in
-    PLseparated l
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, PLseparated l
   | Prel(rel,t1,t2) ->
     let rel = convert_rel rel in
-    let t1 = convert_logic_expr env t1 in
-    let t2 = convert_logic_expr env t2 in
-    PLrel(t1,rel,t2)
+    let env, t1 = convert_logic_expr env t1 in
+    let env, t2 = convert_logic_expr env t2 in
+    env, PLrel(t1,rel,t2)
   | Pand(p1,p2) ->
-    let p1 = convert_pred_named env p1 in
-    let p2 = convert_pred_named env p2 in
-    PLand(p1,p2)
+    let env, p1 = convert_pred_named env p1 in
+    let env, p2 = convert_pred_named env p2 in
+    env, PLand(p1,p2)
   | Por(p1,p2) ->
-    let p1 = convert_pred_named env p1 in
-    let p2 = convert_pred_named env p2 in
-    PLor(p1,p2)
+    let env, p1 = convert_pred_named env p1 in
+    let env, p2 = convert_pred_named env p2 in
+    env, PLor(p1,p2)
   | Pxor(p1,p2) ->
-    let p1 = convert_pred_named env p1 in
-    let p2 = convert_pred_named env p2 in
-    PLxor(p1,p2)
+    let env, p1 = convert_pred_named env p1 in
+    let env, p2 = convert_pred_named env p2 in
+    env, PLxor(p1,p2)
   | Pimplies(p1,p2) ->
-    let p1 = convert_pred_named env p1 in
-    let p2 = convert_pred_named env p2 in
-    PLimplies(p1,p2)
+    let env, p1 = convert_pred_named env p1 in
+    let env, p2 = convert_pred_named env p2 in
+    env, PLimplies(p1,p2)
   | Piff(p1,p2) ->
-    let p1 = convert_pred_named env p1 in
-    let p2 = convert_pred_named env p2 in
-    PLiff(p1,p2)
+    let env, p1 = convert_pred_named env p1 in
+    let env, p2 = convert_pred_named env p2 in
+    env, PLiff(p1,p2)
   | Pnot p ->
-    let p = convert_pred_named env p in
-    PLnot p
+    let env, p = convert_pred_named env p in
+    env, PLnot p
   | Pif(cond,ptrue,pfalse) ->
-    let cond = convert_logic_expr env cond in
-    let ptrue = convert_pred_named env ptrue in
-    let pfalse = convert_pred_named env pfalse in
-    PLif(cond,ptrue,pfalse)
+    let env, cond = convert_logic_expr env cond in
+    let env, ptrue = convert_pred_named env ptrue in
+    let env, pfalse = convert_pred_named env pfalse in
+    env, PLif(cond,ptrue,pfalse)
   | Plet(li,p) ->
-    let body = convert_inner_body env li in
-    let p = convert_pred_named env p in
-    PLlet(li.li_name.decl_name,body,p)
+    let env, body = convert_inner_body env li in
+    let env, p = convert_pred_named env p in
+    env, PLlet(li.li_name.decl_name,body,p)
   | Pforall (x,p) ->
-    let quants = List.map (convert_var_decl env) x in
-    let p = convert_pred_named env p in
-    PLforall(quants,p)
+    let env, quants = Convert_env.env_map convert_var_decl env x in
+    let env, p = convert_pred_named env p in
+    env, PLforall(quants,p)
   | Pexists(x,p) ->
-    let quants = List.map (convert_var_decl env) x in
-    let p = convert_pred_named env p in
-    PLexists(quants,p)
+    let env, quants = Convert_env.env_map convert_var_decl env x in
+    let env, p = convert_pred_named env p in
+    env, PLexists(quants,p)
   | Pat(l,p) ->
     let l = convert_logic_label l in
-    let p = convert_pred_named env p in
-    PLat(p,l)
+    let env, p = convert_pred_named env p in
+    env, PLat(p,l)
   | Pvalid_function(t) ->
-    let t = convert_logic_expr env t in
-    PLvalid_function(t)
+    let env, t = convert_logic_expr env t in
+    env, PLvalid_function(t)
   | Pvalid_read(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLvalid_read(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLvalid_read(l,t)
   | Pvalid(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLvalid(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLvalid(l,t)
   | Pinitialized(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLinitialized(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLinitialized(l,t)
   | Pallocable(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLallocable(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLallocable(l,t)
   | Pfreeable(l,t) ->
     let l = convert_logic_label_opt l in
-    let t = convert_logic_expr env t in
-    PLfreeable(l,t)
+    let env, t = convert_logic_expr env t in
+    env, PLfreeable(l,t)
   | Pfresh(Some l1, Some l2,t1,t2) ->
     let l1 = convert_logic_label l1 in
     let l2 = convert_logic_label l2 in
-    let t1 = convert_logic_expr env t1 in
-    let t2 = convert_logic_expr env t2 in
-    PLfresh (Some(l1,l2),t1,t2)
+    let env, t1 = convert_logic_expr env t1 in
+    let env, t2 = convert_logic_expr env t2 in
+    env, PLfresh (Some(l1,l2),t1,t2)
   | Pfresh(None,None,t1,t2) ->
-    let t1 = convert_logic_expr env t1 in
-    let t2 = convert_logic_expr env t2 in
-    PLfresh (None,t1,t2)
+    let env, t1 = convert_logic_expr env t1 in
+    let env, t2 = convert_logic_expr env t2 in
+    env, PLfresh (None,t1,t2)
   | Pfresh(_,_,_,_) -> Frama_Clang_option.fatal
       "zero or two labels needed in fresh construct"
   | Psubtype _ -> Frama_Clang_option.not_yet_implemented "subtyping relation"
 
 and convert_inner_body env li =
-  let body =
+  let env, body =
     match li.fun_body with
       | LBnone -> Convert_env.fatal env "local binding without body"
       | LBreads _ -> Convert_env.fatal env "local binding with read clause"
@@ -537,14 +554,15 @@ and convert_inner_body env li =
       | LBpred p -> convert_pred_named env p
   in
   match li.profile with
-    | [] -> body
+    | [] -> env, body
     | prms ->
-      let convert_arg_decl a =
-        let typ = convert_logic_type env a.la_type in
+      let convert_arg_decl env a =
+        let env, typ = convert_logic_type env a.la_type in
         let v = a.la_name in
-        typ, v
+        env, (typ, v)
       in
-      let prms = List.map convert_arg_decl prms in
+      let env, prms = Convert_env.env_map convert_arg_decl env prms in
+      env,
       { lexpr_node = PLlambda(prms,body); lexpr_loc = Convert_env.get_loc env }
 
 let convert_logic_ctor env ctor =
@@ -558,39 +576,50 @@ let convert_logic_ctor env ctor =
         = Convert_env.typedef_normalize env ctor.ctor_name TStandard in
       Mangling.mangle ctor_name t None
   in
-  let prms = List.map (convert_logic_type env) ctor.ctor_params in
-  (name,prms)
+  let env, prms =
+    Convert_env.env_map convert_logic_type env ctor.ctor_params
+  in
+  env, (name,prms)
 
 let convert_logic_type_def env = function
-  | LTsum ctors -> TDsum (List.map (convert_logic_ctor env) ctors)
-  | LTsyn t -> TDsyn (convert_logic_type env t)
+  | LTsum ctors ->
+    let env, ctors = Convert_env.env_map convert_logic_ctor env ctors in
+    env, TDsum ctors
+  | LTsyn t ->
+    let env, t = convert_logic_type env t in env, TDsyn t
 
 let convert_extended env e =
-  (e.ext_name, List.map (convert_pred_named env) e.predicates)
+  let env, preds = Convert_env.env_map convert_pred_named env e.predicates in
+  env, (e.ext_name, preds)
 
 let convert_allocation env = function
   | Intermediate_format.FreeAlloc(f,a) ->
-    Logic_ptree.FreeAlloc
-      (List.map (convert_logic_expr env) f, List.map (convert_logic_expr env) a)
-  | Intermediate_format.FreeAllocAny -> Logic_ptree.FreeAllocAny
+    let env, f = Convert_env.env_map convert_logic_expr env f in
+    let env, a = Convert_env.env_map convert_logic_expr env a in
+    env, Logic_ptree.FreeAlloc (f,a)
+  | Intermediate_format.FreeAllocAny -> env, Logic_ptree.FreeAllocAny
 
 let convert_deps env = function
   | Intermediate_format.From l ->
-      Logic_ptree.From (List.map (convert_logic_expr env) l)
-  | Intermediate_format.FromAny -> Logic_ptree.FromAny
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, Logic_ptree.From l
+  | Intermediate_format.FromAny -> env, Logic_ptree.FromAny
 
 let convert_from env f =
-  convert_logic_expr env f.floc, convert_deps env f.vars
+  let env, w = convert_logic_expr env f.floc in
+  let env, r = convert_deps env f.vars in
+  env, (w,r)
 
 let convert_assigns env = function
-  | Intermediate_format.WritesAny -> Logic_ptree.WritesAny
+  | Intermediate_format.WritesAny -> env, Logic_ptree.WritesAny
   | Intermediate_format.Writes l ->
-      Logic_ptree.Writes (List.map (convert_from env) l)
+    let env, l = Convert_env.env_map convert_from env l in
+    env, Logic_ptree.Writes l
 
 let convert_pred_tp env ?(kind=Cil_types.Assert) p =
   (* TODO: support check and admit in ACSL++. *)
-  let tp_statement = convert_pred_named env p in
-  { tp_kind = kind; tp_statement }
+  let env, tp_statement = convert_pred_named env p in
+  env, { tp_kind = kind; tp_statement }
 
 let convert_termination_kind = function
   | Intermediate_format.Normal -> Cil_types.Normal
@@ -600,26 +629,35 @@ let convert_termination_kind = function
   | Intermediate_format.Returns -> Cil_types.Returns
 
 let convert_post_cond env p =
-  convert_termination_kind p.tkind, convert_pred_tp env p.pred
+  let kind = convert_termination_kind p.tkind in
+  let env, p = convert_pred_tp env p.pred in
+  env, (kind, p)
 
 let convert_behavior env bhv =
   let b_name = bhv.beh_name in
-  let b_requires = List.map (convert_pred_tp env) bhv.requires in
-  let b_assumes = List.map (convert_pred_named env) bhv.assumes in
-  let b_post_cond = List.map (convert_post_cond env) bhv.post_cond in
-  let b_assigns = convert_assigns env bhv.assignements in
-  let b_allocation = convert_allocation env bhv.alloc in
-  let b_extended = List.map (convert_extended env) bhv.extended in
-  { b_name; b_requires; b_assumes; b_post_cond;
-    b_assigns; b_allocation; b_extended }
-
-let convert_variant env v = convert_logic_expr env v.vbody, v.vname
+  let env_map = Convert_env.env_map in
+  (* optional arguments do not mix well with higher-order funcs *)
+  let convert_pred_tp env p = convert_pred_tp env p in
+  let env, b_requires = env_map convert_pred_tp env bhv.requires in
+  let env, b_assumes = env_map convert_pred_named env bhv.assumes in
+  let env, b_post_cond = env_map convert_post_cond env bhv.post_cond in
+  let env, b_assigns = convert_assigns env bhv.assignements in
+  let env, b_allocation = convert_allocation env bhv.alloc in
+  let env, b_extended = env_map convert_extended env bhv.extended in
+  env, { b_name; b_requires; b_assumes; b_post_cond;
+         b_assigns; b_allocation; b_extended }
+
+let convert_variant env v =
+  let env, body = convert_logic_expr env v.vbody in
+  env, (body, v.vname)
 
 let convert_function_contract env contract =
-  let spec_behavior = List.map (convert_behavior env) contract.behavior in
-  let spec_variant = Option.map (convert_variant env) contract.variant in
-  let spec_terminates =
-    Option.map (convert_pred_named env) contract.terminates
+  let env_map = Convert_env.env_map in
+  let env_opt = Convert_env.env_opt in
+  let env, spec_behavior = env_map convert_behavior env contract.behavior in
+  let env, spec_variant = env_opt convert_variant env contract.variant in
+  let env, spec_terminates =
+    env_opt convert_pred_named env contract.terminates
   in
   let spec_complete_behaviors =
     List.map (fun c -> c.behaviors) contract.complete_behaviors
@@ -627,8 +665,9 @@ let convert_function_contract env contract =
   let spec_disjoint_behaviors =
     List.map (fun c -> c.behaviors) contract.disjoint_behaviors
   in
-  { spec_behavior; spec_variant; spec_terminates; spec_complete_behaviors;
-    spec_disjoint_behaviors }
+  env,
+  { spec_behavior; spec_variant; spec_terminates;
+    spec_complete_behaviors; spec_disjoint_behaviors }
 
 let convert_inv_kind = function
   | InvariantAsAssertion -> false
@@ -636,46 +675,65 @@ let convert_inv_kind = function
 
 let convert_loop_pragma env = function
   | Intermediate_format.Unroll_specs l ->
-    Logic_ptree.Unroll_specs (List.map (convert_logic_expr env) l)
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, Logic_ptree.Unroll_specs l
   | Intermediate_format.Widen_hints l ->
-    Logic_ptree.Unroll_specs (List.map(convert_logic_expr env) l)
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, Logic_ptree.Widen_hints l
   | Intermediate_format.Widen_variables l ->
-    Logic_ptree.Widen_variables (List.map (convert_logic_expr env) l)
+    let env, l = Convert_env.env_map convert_logic_expr env l in
+    env, Logic_ptree.Widen_variables l
 
 let convert_slice_pragma env = function
   | Intermediate_format.SPexpr e ->
-      Logic_ptree.SPexpr (convert_logic_expr env e)
-  | Intermediate_format.SPctrl -> Logic_ptree.SPctrl
-  | Intermediate_format.SPstmt -> Logic_ptree.SPstmt
+    let env, e = convert_logic_expr env e in
+      env, Logic_ptree.SPexpr e
+  | Intermediate_format.SPctrl -> env, Logic_ptree.SPctrl
+  | Intermediate_format.SPstmt -> env, Logic_ptree.SPstmt
 
 let convert_impact_pragma env = function
   | Intermediate_format.IPexpr e ->
-      Logic_ptree.IPexpr (convert_logic_expr env e)
-  | Intermediate_format.IPstmt -> Logic_ptree.IPstmt
+    let env, e = convert_logic_expr env e in
+    env, Logic_ptree.IPexpr e
+  | Intermediate_format.IPstmt -> env, Logic_ptree.IPstmt
 
 let convert_pragma env = function
   | Intermediate_format.Loop_pragma p ->
-      Logic_ptree.Loop_pragma (convert_loop_pragma env p)
+    let env, p = convert_loop_pragma env p in
+    env, Logic_ptree.Loop_pragma p
   | Intermediate_format.Slice_pragma p ->
-      Logic_ptree.Slice_pragma (convert_slice_pragma env p)
+    let env, p = convert_slice_pragma env p in
+    env, Logic_ptree.Slice_pragma p
   | Intermediate_format.Impact_pragma p ->
-      Logic_ptree.Impact_pragma (convert_impact_pragma env p)
+    let env, p = convert_impact_pragma env p in
+    env, Logic_ptree.Impact_pragma p
 
 let convert_code_annot env = function
   | Intermediate_format.Assert(bhvs,pred) ->
-    AAssert(bhvs, convert_pred_tp env pred)
-  | StmtSpec(bhvs,spec) -> AStmtSpec(bhvs,convert_function_contract env spec)
+    let env, pred = convert_pred_tp env pred in
+    env, AAssert(bhvs, pred)
+  | StmtSpec(bhvs,spec) ->
+    let env, spec = convert_function_contract env spec in
+    env, AStmtSpec(bhvs, spec)
   | Invariant(bhvs,kind,inv) ->
     let kind = convert_inv_kind kind in
-    let inv = convert_pred_tp env inv in
-    AInvariant(bhvs,kind,inv)
-  | Variant v -> AVariant (convert_variant env v)
-  | Assigns (bhvs,a) -> AAssigns(bhvs,convert_assigns env a)
-  | Allocation(bhvs,a) -> AAllocation(bhvs,convert_allocation env a)
-  | Pragma p -> APragma (convert_pragma env p)
+    let env, inv = convert_pred_tp env inv in
+    env, AInvariant(bhvs,kind,inv)
+  | Variant v ->
+    let env, v = convert_variant env v in
+    env, AVariant v
+  | Assigns (bhvs,a) ->
+    let env, a = convert_assigns env a in
+    env, AAssigns(bhvs, a)
+  | Allocation(bhvs,a) ->
+    let env, a = convert_allocation env a in
+    env, AAllocation(bhvs,a)
+  | Pragma p ->
+    let env, p = convert_pragma env p in
+    env, APragma p
 
 let rec convert_annot env annot =
-  let annot, env =
+  let env, annot =
     match annot with
       | Dfun_or_pred (loc,info) ->
         let env = Convert_env.set_loc env loc in
@@ -692,77 +750,81 @@ let rec convert_annot env annot =
             Mangling.mangle info_name t None
         in
         let labels = List.map convert_logic_label info.arg_labels in
-        let rt = Option.map (convert_logic_type env) info.returned_type in
-        let params = List.map (convert_logic_param env) info.profile in
+        let env, rt =
+          Convert_env.env_opt convert_logic_type env info.returned_type
+        in
+        let env, params =
+          Convert_env.env_map convert_logic_param env info.profile
+        in
         (match info.fun_body,rt with
           | LBnone, None ->
-            LDpredicate_reads(name,labels,info.tparams,params,None)
+            env, LDpredicate_reads(name,labels,info.tparams,params,None)
           | LBnone, Some rt ->
-            LDlogic_reads(name,labels,info.tparams,rt,params,None)
+            env, LDlogic_reads(name,labels,info.tparams,rt,params,None)
           | LBreads l, None ->
-            let reads = List.map (convert_logic_expr env) l in
-            LDpredicate_reads(name,labels,info.tparams,params,Some reads)
+            let env, reads = Convert_env.env_map convert_logic_expr env l in
+            env, LDpredicate_reads(name,labels,info.tparams,params,Some reads)
           | LBreads l, Some rt ->
-            let reads = List.map (convert_logic_expr env) l in
-            LDlogic_reads(name,labels,info.tparams,rt,params,Some reads)
+            let env, reads = Convert_env.env_map convert_logic_expr env l in
+            env, LDlogic_reads(name,labels,info.tparams,rt,params,Some reads)
           | LBterm _, None ->
             Convert_env.fatal env "predicate definition with a term as body"
           | LBterm body, Some rt ->
-            let body = convert_logic_expr env body in
-            LDlogic_def(name,labels,info.tparams,rt,params,body)
+            let env, body = convert_logic_expr env body in
+            env, LDlogic_def(name,labels,info.tparams,rt,params,body)
           | LBpred _, Some _ ->
             Convert_env.fatal env
               "logic function definition with a predicate as body"
           | LBpred body, None ->
-            let body = convert_pred_named env body in
-            LDpredicate_def(name,labels,info.tparams,params,body)
+            let env, body = convert_pred_named env body in
+            env, LDpredicate_def(name,labels,info.tparams,params,body)
           | LBinductive _, Some _ ->
             Convert_env.fatal env
               "logic function definition with inductive body"
           | LBinductive body, None ->
-            let inductive_case ind =
+            let inductive_case env ind =
               let labs = List.map convert_logic_label ind.labels in
-              let def = convert_pred_named env ind.def in
-              (ind.def_name,labs,ind.arguments,def)
+              let env, def = convert_pred_named env ind.def in
+              env, (ind.def_name,labs,ind.arguments,def)
             in
-            let body = List.map inductive_case body in
-            LDinductive_def(name,labels,info.tparams,params,body)
-        ), env
+            let env, body = Convert_env.env_map inductive_case env body in
+            env, LDinductive_def(name,labels,info.tparams,params,body)
+        )
       | Dvolatile(loc,mem,read,write) ->
         let env = Convert_env.set_loc env loc in
-        let mem = List.map (convert_logic_expr env) mem in
+        let env, mem = Convert_env.env_map convert_logic_expr env mem in
         (* NB: should we have the real type of the arguments of the functions?*)
         let mangle name signature =
           let name, t = Convert_env.typedef_normalize env name TStandard in
           Mangling.mangle name t signature in
-        let read = Option.map (Fun.flip mangle None)
-                   read in
-        let write = Option.map (Fun.flip mangle None)
-                    write in
-        LDvolatile(mem,(read,write)), env
+        let read = Option.map (Fun.flip mangle None) read in
+        let write = Option.map (Fun.flip mangle None) write in
+        env, LDvolatile(mem,(read,write))
       | Daxiomatic(loc,s,annots) ->
         let env = Convert_env.set_loc env loc in
-        let annots = List.map (convert_annot env) annots in
-        LDaxiomatic(s,annots), env
+        let env, annots = Convert_env.env_map convert_annot env annots in
+        env, LDaxiomatic(s,annots)
       | Dtype(loc,lt_info) ->
         let env = Convert_env.set_loc env loc in
         let name =
           if lt_info.logic_type_info_is_extern_c then
             lt_info.type_name.decl_name
           else
-            let info_name, t = Convert_env.typedef_normalize
-                  env lt_info.type_name TStandard in
+            let info_name, t =
+              Convert_env.typedef_normalize env lt_info.type_name TStandard
+            in
             Mangling.mangle info_name t None
         in
-        let def = Option.map (convert_logic_type_def env)
-                    lt_info.definition in
-        LDtype(name, lt_info.params, def), env
+        let env, def =
+          Convert_env.env_opt convert_logic_type_def env lt_info.definition
+        in
+        env, LDtype(name, lt_info.params, def)
       | Dlemma(loc,name,is_axiom,labs,params,body) ->
         let env = Convert_env.set_loc env loc in
         let labs = List.map convert_logic_label labs in
         let kind = if is_axiom then Cil_types.Admit else Assert in
-        let body = convert_pred_tp env ~kind body in
-        LDlemma(name,labs,params,body), env
+        let env, body = convert_pred_tp env ~kind body in
+        env, LDlemma(name,labs,params,body)
       | Dinvariant(loc,body) ->
         let env = Convert_env.set_loc env loc in
         let name =
@@ -773,43 +835,45 @@ let rec convert_annot env annot =
                   env body.li_name TStandard in
             Mangling.mangle body_name t None
         in
-        let body =
+        let env, body =
           match body.fun_body with
             | LBpred p ->
               convert_pred_named env p
             | _ ->
               Convert_env.fatal env "unexpected body for a global invariant"
         in
-        LDinvariant(name, body), env
+        env, LDinvariant(name, body)
       | Dtype_annot (loc, body) ->
         let env = Convert_env.set_loc env loc in
         let inv_name =
           if body.li_extern_c then
             body.li_name.decl_name
           else
-            let body_name, t = Convert_env.typedef_normalize
-                  env body.li_name TStandard in
+            let body_name, t =
+              Convert_env.typedef_normalize env body.li_name TStandard
+            in
             Mangling.mangle body_name t None
         in
-        let this_type, this_name =
+        let env, (this_type, this_name) =
           match body.profile with
-            | [ { la_type = t; la_name = s } ] -> convert_logic_type env t, s
+            | [ { la_type = t; la_name = s } ] ->
+              let env, t = convert_logic_type env t in env, (t, s)
             | _ ->
               Convert_env.fatal env
                 "unexpected number of parameters \
                  in definition of type invariant"
         in
-        let inv =
+        let env, inv =
           match body.fun_body with
             | LBpred p -> convert_pred_named env p
             | _ -> Convert_env.fatal env "unexpected body for a type invariant"
         in
-        LDtype_annot { inv_name; this_type; this_name; inv }, env
+        env, LDtype_annot { inv_name; this_type; this_name; inv }
       | Dmodel_annot(loc,model) ->
         let env = Convert_env.set_loc env loc in
         let model_name = model.Intermediate_format.model_name in
-        let model_type = convert_logic_type env model.field_type in
-        let model_for_type = convert_logic_type env model.base_type in
-        LDmodel_annot { model_for_type; model_type; model_name }, env
+        let env, model_type = convert_logic_type env model.field_type in
+        let env, model_for_type = convert_logic_type env model.base_type in
+        env, LDmodel_annot { model_for_type; model_type; model_name }
   in
-  { decl_node = annot; decl_loc = Convert_env.get_loc env; }
+  env, { decl_node = annot; decl_loc = Convert_env.get_loc env; }
diff --git a/convert_acsl.mli b/convert_acsl.mli
index 9f6abe0ce6251a985e212a5b1a99f2ecaff67d94..55a5faa6f43de5dc0785bbd31cd0f3ec2f022034 100644
--- a/convert_acsl.mli
+++ b/convert_acsl.mli
@@ -24,11 +24,14 @@
 
 val convert_function_contract:
   Convert_env.env ->
-  Intermediate_format.function_contract -> Logic_ptree.spec
+  Intermediate_format.function_contract ->
+  Convert_env.env * Logic_ptree.spec
 
 val convert_code_annot:
   Convert_env.env ->
-  Intermediate_format.code_annotation -> Logic_ptree.code_annot
+  Intermediate_format.code_annotation ->
+  Convert_env.env * Logic_ptree.code_annot
 
 val convert_annot:
-  Convert_env.env -> Intermediate_format.global_annotation -> Logic_ptree.decl
+  Convert_env.env -> Intermediate_format.global_annotation ->
+  Convert_env.env * Logic_ptree.decl
diff --git a/convert_env.ml b/convert_env.ml
index f076bd323ae0b043a4932131c465ea0fbc28a6a3..5adbb515f34916e97195b4d2c99ac0bd25803d18 100644
--- a/convert_env.ml
+++ b/convert_env.ml
@@ -813,3 +813,7 @@ let env_map f env l =
   let do_one (env, acc) x = let env, y = f env x in env,y::acc in
   let env, res = List.fold_left do_one (env,[]) l in
   env, List.rev res
+
+let env_opt f env = function
+  | Some x -> let env, y = f env x in env, Some y
+  | None -> env, None
diff --git a/convert_env.mli b/convert_env.mli
index 9a45ebf1d7461b5517bfba95a17f17b223f5b717..9ab4dbe64b996f6ed92a47043c6de01120e2e3c3 100644
--- a/convert_env.mli
+++ b/convert_env.mli
@@ -325,3 +325,8 @@ val add_closure_info: env -> capture list -> env
     and returns the final environment together with the list of results
 *)
 val env_map: (env -> 'a -> (env * 'b)) -> env -> 'a list -> (env * 'b list)
+
+(** [env_opt f env opt] applies [f] if [opt] has a value, and [None], without
+    changing the environment otherwise.
+*)
+val env_opt: (env -> 'a -> (env * 'b)) -> env -> 'a option -> (env * 'b option)
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index bd686d917ffc2377d51e19504eead59e959b28e1..19fb1e1cbe1998b55f08f890b09b414245f70890 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -24,6 +24,7 @@ struct _frama_c_rtti_name_info_node {
    struct _frama_c_vmt *pvmt ;
 };
 typedef unsigned int size_t;
+typedef long wchar_t;
 struct __fc_div_t {
    int quot ;
    int rem ;
@@ -39,7 +40,6 @@ struct __fc_lldiv_t {
    long long rem ;
 };
 typedef struct __fc_lldiv_t lldiv_t;
-typedef long wchar_t;
 typedef size_t size_t;
 struct T;
 struct T {
@@ -272,14 +272,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -289,64 +289,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -355,11 +355,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -369,14 +369,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -401,20 +402,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ requires valid_nptr: \valid_read(nptr);
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 8b2058baa39ac3767c9065984c5cb8e5c3005e90..e5a02cc7a2908bfd6771dba682ccb08c547c2569 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -2,6 +2,7 @@
 Now output intermediate result
 /* Generated by Frama-C */
 typedef unsigned int size_t;
+typedef long wchar_t;
 struct __fc_div_t {
    int quot ;
    int rem ;
@@ -17,7 +18,6 @@ struct __fc_lldiv_t {
    long long rem ;
 };
 typedef struct __fc_lldiv_t lldiv_t;
-typedef long wchar_t;
 void *malloc(size_t size);
 
 void free(void *p);
@@ -241,14 +241,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -258,64 +258,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -324,11 +324,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -338,14 +338,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -370,20 +371,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ requires valid_nptr: \valid_read(nptr);
diff --git a/tests/specs/oracle/wchar_t.res.oracle b/tests/specs/oracle/wchar_t.res.oracle
index 130fd3148ea1772077349e0f70e5eb40da8610f4..adecf2ef1d13c9e6a4e6a89bad75e9724ddce9d6 100644
--- a/tests/specs/oracle/wchar_t.res.oracle
+++ b/tests/specs/oracle/wchar_t.res.oracle
@@ -2,9 +2,10 @@
 Now output intermediate result
 /* Generated by Frama-C */
 typedef long wchar_t;
-/*@ predicate is_normal_char(long c) = 0 â‰¤ c â‰¤ 255;
+/*@ predicate is_normal_char(wchar_t c) = 0 â‰¤ c â‰¤ 255;
  */
-/*@ predicate wchar_buff{L}(long *p, â„¤ l) = \at(*(p + l) â‰¡ (long)0,L);
+/*@
+predicate wchar_buff{L}(wchar_t *p, â„¤ l) = \at(*(p + l) â‰¡ (wchar_t)0,L);
  */
 int freq[256];
 /*@ requires is_normal_char(c); */
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index 116484a4efbe6cb54b5bdc4035ce7350c687bda6..158a5df03761a6ff0b7954894a01b69076d5f119 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -65,6 +65,7 @@ struct pair<int*,int*> {
    int *first ;
    int *second ;
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -678,14 +679,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -695,64 +696,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -761,11 +762,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -775,14 +776,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -807,20 +809,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
diff --git a/tests/stl/oracle/stl_bool.res.oracle b/tests/stl/oracle/stl_bool.res.oracle
index 750ea7a998b32d7be0fa12af092d4b466308d8c2..64160356e0812d94b5e81bacf6e238028255655d 100644
--- a/tests/stl/oracle/stl_bool.res.oracle
+++ b/tests/stl/oracle/stl_bool.res.oracle
@@ -43,6 +43,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -326,14 +327,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -343,64 +344,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -409,11 +410,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -423,14 +424,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -455,20 +457,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index 4a90e39711dae24bd20e6fd3fab7c3baff873174..b4e115ee3fe5c3a9089c493a64fd112ee27c4314 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -50,6 +50,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -486,14 +487,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -503,64 +504,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -569,11 +570,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -583,14 +584,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -615,20 +617,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index 0f3b7fc03505686f69a3d7e875060ff73d3b8d60..ce15968f67d2aae01758ccfa8669393a2e63a55a 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -67,6 +67,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -492,14 +493,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -509,64 +510,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -575,11 +576,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -589,14 +590,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -621,20 +623,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index e03d5d8e5d00e07cf2aec3598e315a4beea078aa..d8f78952a309b6652709d2a13bb0a7476a70f0a2 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -54,6 +54,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -115,7 +116,6 @@ struct __fc_lldiv_t {
    long long rem ;
 };
 typedef struct __fc_lldiv_t lldiv_t;
-typedef long wchar_t;
 struct Aircraft {
    int m_id ;
    int m_flyCount ;
@@ -461,14 +461,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -478,64 +478,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -544,11 +544,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -558,14 +558,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -590,20 +591,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
 
 */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index a46d588217d4921a93749653bd2029a34e6f0f19..014225c031ca311a59e353244ead192a7c143f53 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -52,6 +52,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -112,7 +113,6 @@ struct __fc_lldiv_t {
    long long rem ;
 };
 typedef struct __fc_lldiv_t lldiv_t;
-typedef long wchar_t;
 struct Aircraft {
    int m_id ;
    int m_flyCount ;
@@ -442,14 +442,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -459,64 +459,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -525,11 +525,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -539,14 +539,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -571,20 +572,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
 
 */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 37ece5b303d3a0f03e26700b2a7aba6e4b530cb3..1f306e3324fc334c905324e1371b9cce0e110314 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -53,6 +53,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -113,7 +114,6 @@ struct __fc_lldiv_t {
    long long rem ;
 };
 typedef struct __fc_lldiv_t lldiv_t;
-typedef long wchar_t;
 struct Aircraft {
    int m_id ;
    int m_flyCount ;
@@ -443,14 +443,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -460,64 +460,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -526,11 +526,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -540,14 +540,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -572,20 +573,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
 
 */
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index f47a3978400b2b09fa04f35a6693615cf4fc6725..0cc69025abd99f5982d62e82d18cb47af089b151 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -41,6 +41,7 @@ struct integral_constant<bool,1>;
 struct integral_constant<bool,1> {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -103,7 +104,6 @@ struct tm {
    int tm_yday ;
    int tm_isdst ;
 };
-typedef long wchar_t;
 typedef char char_type;
 typedef wchar_t char_type;
 struct __shared_ref_base;
@@ -405,14 +405,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -422,64 +422,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -488,11 +488,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -502,14 +502,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -534,20 +535,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
@@ -2218,7 +2219,7 @@ wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle);
 wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
 
 /*@ axiomatic wformat_length {
-      logic â„¤ wformat_length{L}(long *format) ;
+      logic â„¤ wformat_length{L}(wchar_t *format) ;
       
       }
 
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index 32844fea1e0495bce92c9ec67e770ef9132f377b..e61c0e41eb1039a215debe66e27075a51d81b161 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -33,6 +33,7 @@ struct _frama_c_rtti_name_info_node {
 };
 typedef unsigned int size_t;
 typedef size_t size_t;
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -262,14 +263,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -279,64 +280,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -345,11 +346,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -359,14 +360,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -391,20 +393,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 95faad0de16d86e2147be464c15c06285ab3bd87..51284e7d35e254fa9ef3c3d5af18d304f0d3ef1a 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -372,6 +372,7 @@ struct piecewise_construct_t;
 struct piecewise_construct_t {
    
 };
+typedef long wchar_t;
 struct exception;
 struct bad_exception;
 struct nested_exception;
@@ -985,14 +986,14 @@ axiomatic StrChr {
  */
 /*@
 axiomatic WMemChr {
-  logic ð”¹ wmemchr{L}(long *s, long c, â„¤ n) 
+  logic ð”¹ wmemchr{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
-  logic â„¤ wmemchr_off{L}(long *s, long c, â„¤ n) 
+  logic â„¤ wmemchr_off{L}(wchar_t *s, wchar_t c, â„¤ n) 
     reads *(s + (0 .. n - 1));
   
   axiom wmemchr_def{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ long c;
     âˆ€ â„¤ n;
       wmemchr(s, c, n) â‰¢ (0 â‰¢ 0) â‡”
@@ -1002,64 +1003,64 @@ axiomatic WMemChr {
  */
 /*@
 axiomatic WcsLen {
-  logic â„¤ wcslen{L}(long *s) 
+  logic â„¤ wcslen{L}(wchar_t *s) 
     reads *(s + (0 ..));
   
   axiom wcslen_pos_or_null{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ â„¤ i;
-      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (long)0) âˆ§
-      *(s + i) â‰¡ (long)0 â‡’ wcslen(s) â‰¡ i;
+      0 â‰¤ i âˆ§ (âˆ€ â„¤ j; 0 â‰¤ j < i â‡’ *(s + j) â‰¢ (wchar_t)0) âˆ§
+      *(s + i) â‰¡ (wchar_t)0 â‡’ wcslen(s) â‰¡ i;
   
   axiom wcslen_neg{L}:
-    âˆ€ long *s;
-      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (long)0) â‡’ wcslen(s) < 0;
+    âˆ€ wchar_t *s;
+      (âˆ€ â„¤ i; 0 â‰¤ i â‡’ *(s + i) â‰¢ (wchar_t)0) â‡’ wcslen(s) < 0;
   
   axiom wcslen_before_null{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (long)0;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i < wcslen(s) â‡’ *(s + i) â‰¢ (wchar_t)0;
   
   axiom wcslen_at_null{L}:
-    âˆ€ long *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (long)0;
+    âˆ€ wchar_t *s; 0 â‰¤ wcslen(s) â‡’ *(s + wcslen(s)) â‰¡ (wchar_t)0;
   
   axiom wcslen_not_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (long)0 â‡’ i < wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¢ (wchar_t)0 â‡’ i < wcslen(s);
   
   axiom wcslen_zero{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
-      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (long)0 â‡’ i â‰¡ wcslen(s);
+      0 â‰¤ i â‰¤ wcslen(s) âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ i â‰¡ wcslen(s);
   
   axiom wcslen_sup{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i; 0 â‰¤ i â‰¤ wcslen(s) â‡’ wcslen(s + i) â‰¡ wcslen(s) - i;
   
   axiom wcslen_create{L}:
-    âˆ€ long *s;
-    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
+    âˆ€ wchar_t *s;
+    âˆ€ int i; 0 â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’ 0 â‰¤ wcslen(s) â‰¤ i;
   
   axiom wcslen_create_shift{L}:
-    âˆ€ long *s;
+    âˆ€ wchar_t *s;
     âˆ€ int i;
     âˆ€ int k;
-      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (long)0 â‡’
+      0 â‰¤ k â‰¤ i âˆ§ *(s + i) â‰¡ (wchar_t)0 â‡’
       0 â‰¤ wcslen(s + k) â‰¤ i - k;
   
   }
  */
 /*@
 axiomatic WcsCmp {
-  logic â„¤ wcscmp{L}(long *s1, long *s2) 
+  logic â„¤ wcscmp{L}(wchar_t *s1, wchar_t *s2) 
     reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2)));
   
   axiom wcscmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
       wcscmp(s1, s2) â‰¡ 0 â‡”
       wcslen(s1) â‰¡ wcslen(s2) âˆ§
       (âˆ€ â„¤ i; 0 â‰¤ i â‰¤ wcslen(s1) â‡’ *(s1 + i) â‰¡ *(s2 + i));
@@ -1068,11 +1069,11 @@ axiomatic WcsCmp {
  */
 /*@
 axiomatic WcsNCmp {
-  logic â„¤ wcsncmp{L}(long *s1, long *s2, â„¤ n) 
+  logic â„¤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, â„¤ n) 
     reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1));
   
   axiom wcsncmp_zero{L}:
-    âˆ€ long *s1, long *s2;
+    âˆ€ wchar_t *s1, wchar_t *s2;
     âˆ€ â„¤ n;
       wcsncmp(s1, s2, n) â‰¡ 0 â‡”
       (wcslen(s1) < n âˆ§ wcscmp(s1, s2) â‰¡ 0) âˆ¨
@@ -1082,14 +1083,15 @@ axiomatic WcsNCmp {
  */
 /*@
 axiomatic WcsChr {
-  logic ð”¹ wcschr{L}(long *wcs, â„¤ wc) 
+  logic ð”¹ wcschr{L}(wchar_t *wcs, â„¤ wc) 
     reads *(wcs + (0 .. wcslen(wcs)));
   
   axiom wcschr_def{L}:
-    âˆ€ long *wcs;
+    âˆ€ wchar_t *wcs;
     âˆ€ â„¤ wc;
       wcschr(wcs, wc) â‰¢ (0 â‰¢ 0) â‡”
-      (âˆƒ â„¤ i; 0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (long)((int)wc));
+      (âˆƒ â„¤ i;
+         0 â‰¤ i â‰¤ wcslen(wcs) âˆ§ *(wcs + i) â‰¡ (wchar_t)((int)wc));
   
   }
  */
@@ -1114,20 +1116,20 @@ predicate valid_read_nstring{L}(char *s, â„¤ n) =
 predicate valid_string_or_null{L}(char *s) = s â‰¡ \null âˆ¨ valid_string(s);
  */
 /*@
-predicate valid_wstring{L}(long *s) =
+predicate valid_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_wstring{L}(long *s) =
+predicate valid_read_wstring{L}(wchar_t *s) =
   0 â‰¤ wcslen(s) âˆ§ \valid_read(s + (0 .. wcslen(s)));
  */
 /*@
-predicate valid_read_nwstring{L}(long *s, â„¤ n) =
+predicate valid_read_nwstring{L}(wchar_t *s, â„¤ n) =
   (\valid_read(s + (0 .. n - 1)) âˆ§ \initialized(s + (0 .. n - 1))) âˆ¨
   valid_read_wstring(s);
  */
 /*@
-predicate valid_wstring_or_null{L}(long *s) =
+predicate valid_wstring_or_null{L}(wchar_t *s) =
   s â‰¡ \null âˆ¨ valid_wstring(s);
  */
 /*@ ghost int __fc_heap_status; */