diff --git a/src/plugins/e-acsl/mpz.ml b/src/plugins/e-acsl/mpz.ml
index c55a6d9d97eac5d915a112bff9c6b936f7c887f8..a9c5a530c7e294a30a38e9494ba4e9cd7e99ab87 100644
--- a/src/plugins/e-acsl/mpz.ml
+++ b/src/plugins/e-acsl/mpz.ml
@@ -21,7 +21,6 @@
 (**************************************************************************)
 
 open Cil_types
-open Cil_datatype
 
 let t_torig_ref =
   ref 
@@ -59,7 +58,7 @@ let get_set_suffix_and_arg e =
     | TPtr(TInt(IChar, _), _) ->
       "_str",
       (* decimal base for the number given as string *)
-      [ e; Cil.integer ~loc:Location.unknown 10 ]
+      [ e; Cil.integer ~loc:e.eloc 10 ]
     | _ -> assert false
 
 let generic_affect ~loc fname lv ev e =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 31bf99c6e3c06d655022d3376473c2eb80f44ac9..dd3522b065119046107539e380885e9204699653 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -34,7 +34,7 @@ share/e-acsl/e_acsl_gmp.h:91:[value] Function __gmpz_set: precondition got statu
 share/e-acsl/e_acsl_gmp.h:92:[value] Function __gmpz_set: precondition got status valid.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
 [value] using specification for function __gmpz_cmp
 share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 7315d054464478f314ff0e7c8fa14773e1435f44..243cae07889c7b734dd65b1c0c39461c610304c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -16,7 +16,7 @@
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __initialize
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
 [value] using specification for function __valid_read
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 95b2d0a49d8c1c78f46767ad43608ca07790e69b..633eebb1b80ea1119336d7b0cc1631e23f88073a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -18,10 +18,11 @@
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __literal_string
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
 [value] using specification for function __valid_read
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
 tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 7fbf952e57a40065010c8d89d213aa0a8247ab6b..121482b595467ab9284ea2b4d3d5a8c1d50ee839 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -33,7 +33,7 @@ share/e-acsl/e_acsl_gmp.h:91:[value] Function __gmpz_set: precondition got statu
 share/e-acsl/e_acsl_gmp.h:92:[value] Function __gmpz_set: precondition got status valid.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
 [value] using specification for function __gmpz_init_set_ui
 share/e-acsl/e_acsl_gmp.h:53:[value] Function __gmpz_init_set_ui: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: postcondition got status valid.
@@ -48,6 +48,7 @@ tests/e-acsl-runtime/bts1390.c:15:[kernel] warning: out of bounds read. assert \
 share/e-acsl/e_acsl_gmp.h:140:[value] Function __gmpz_add: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:141:[value] Function __gmpz_add: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got status valid.
+tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
 tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
 tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
 [value] using specification for function __delete_block
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 8a4630fea3664c55ad68f8f7241df242ca18e22b..28ec7679cbdc174267e55a8d372eca86bf04bb54 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -48,8 +48,9 @@ share/e-acsl/e_acsl_gmp.h:142:[value] Function __gmpz_add: precondition got stat
 tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_3 < 10;
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_4 < 10;
+tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_2 < 10;
 tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
 tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index a3216aea63e6aba61819b3003c8a9bf704254fb0..94d7fda7d4dbd69488a29c081cd376d6c95c9624 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -22,7 +22,8 @@ tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-:0:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
+tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
 tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index c7f6447d64adf8961aaf40fe55869dd80d2d1bd6..78d76d732ac3f051290d4b4d20fdfa3451af158b 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -581,9 +581,9 @@ and named_predicate_content_to_exp ?name kf env p =
   | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
   | Pat(p, LogicLabel(_, label)) when label = "Here" -> 
     named_predicate_to_exp kf env p
-  | Pat(p, label) -> 
+  | Pat(p', label) -> 
     (* convert [t'] to [e] in a separated local env *)
-    let e, env = named_predicate_to_exp kf (Env.push env) p in
+    let e, env = named_predicate_to_exp kf (Env.push env) p' in
     let e, env, is_string = at_to_exp env None label e in
     assert (not is_string);
     e, env
@@ -693,7 +693,10 @@ let predicate_to_exp kf p =
 
 let assumes_predicate bhv =
   List.fold_left
-    (fun acc p -> Logic_const.pand (acc, Logic_const.unamed p.ip_content))
+    (fun acc p -> 
+      Logic_const.pand
+	~loc:p.ip_loc
+	(acc, Logic_const.unamed ~loc:p.ip_loc p.ip_content))
     Logic_const.ptrue
     bhv.b_assumes