diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index 537ed90a85f324808f4a39e3ab7a498352902d8f..7420d943c8ce4f52b8cfc76abc5938d0b721523c 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -77,12 +77,13 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
   match p.pred_content with
   | Pfalse -> Cil.zero ~loc, adata, env
   | Ptrue -> Cil.one ~loc, adata, env
-  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
-  | Papp (li, [], args) ->
+  | Papp (li, [], args)
+  | Papp (li, [BuiltinLabel Here], args) ->
     let e, adata, env =
       Logic_functions.app_to_exp ~adata ~loc kf env li args in
     let adata = Assert.register_pred ~loc env p e adata in
     e, adata, env
+  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
   | Pdangling _ -> Env.not_yet env "\\dangling"
   | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
   | Pvalid_function _ -> Env.not_yet env "\\valid_function"
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 456a28bc9882b25a38b8be0b9d4130f628135fea..f14cd58df0001529de1008176894ea5e70adce9e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -765,7 +765,8 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
   | Tapp(li, _, _)
     when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
     assert false
-  | Tapp(li, [], args) ->
+  | Tapp(li, [], args)
+  | Tapp(li, [BuiltinLabel Here], args) ->
     let e, adata, env =
       Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
     let adata = Assert.register_term ~loc t e adata in
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index ead203551b4cf464f28044f412691cf8f18bae15..a3e010fc6f607b715aa78855b37b91d5012227ff 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -37,8 +37,8 @@ int glob = 5;
 /*@ logic double f2(double x) = (double)(1/x); */ /* handle in MR !226 */
 
 // To test not_yet:
-/*@ predicate p_notyet{L}(integer x) = x > 0; */
-/*@ logic integer f_notyet{L}(integer x) = x; */
+/*@ predicate p_here{L}(integer x) = x > 0; */
+/*@ logic integer f_here{L}(integer x) = x; */
 
 // Test sums inside functions
 /*@ logic integer f_sum (integer x) = \sum(1,x,\lambda integer y; 1); */
@@ -83,6 +83,6 @@ int main(void) {
   /*@ assert over(1., 2.) == 0.5; */;
 
   // not yet supported
-  /* /\*@ assert p_notyet(27); *\/ ; */
-  /* /\*@ assert f_notyet(27) == 27; *\/ ; */
+  /*@ assert p_here(27); */;
+  /*@ assert f_here(27) == 27; */;
 }
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index ca9e702ccf90ad1eae903661f7a1d6954148d184..c173eeb0c636c88c751bdf35ad302ec72cea7082 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -83,10 +83,14 @@ int glob = 5;
  */
 double __gen_e_acsl_f2(double x);
 
-/*@ predicate p_notyet{L}(integer x) = x > 0;
+/*@ predicate p_here{L}(integer x) = x > 0;
  */
-/*@ logic integer f_notyet{L}(integer x) = x;
+int __gen_e_acsl_p_here(int x);
+
+/*@ logic integer f_here{L}(integer x) = x;
  */
+int __gen_e_acsl_f_here(int x);
+
 /*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
  */
 int __gen_e_acsl_f_sum(int x);
@@ -434,6 +438,41 @@ int main(void)
     __gmpq_clear(__gen_e_acsl__11);
   }
   /*@ assert over(1., 2.) == 0.5; */ ;
+  {
+    int __gen_e_acsl_p_here_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_16 =
+      {.values = (void *)0};
+    __gen_e_acsl_p_here_2 = __gen_e_acsl_p_here(27);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"p_here(27)",
+                                 0,__gen_e_acsl_p_here_2);
+    __gen_e_acsl_assert_data_16.blocking = 1;
+    __gen_e_acsl_assert_data_16.kind = "Assertion";
+    __gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
+    __gen_e_acsl_assert_data_16.file = "functions.c";
+    __gen_e_acsl_assert_data_16.fct = "main";
+    __gen_e_acsl_assert_data_16.line = 86;
+    __e_acsl_assert(__gen_e_acsl_p_here_2,& __gen_e_acsl_assert_data_16);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
+  }
+  /*@ assert p_here(27); */ ;
+  {
+    int __gen_e_acsl_f_here_2;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_17 =
+      {.values = (void *)0};
+    __gen_e_acsl_f_here_2 = __gen_e_acsl_f_here(27);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,"f_here(27)",
+                                 0,__gen_e_acsl_f_here_2);
+    __gen_e_acsl_assert_data_17.blocking = 1;
+    __gen_e_acsl_assert_data_17.kind = "Assertion";
+    __gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
+    __gen_e_acsl_assert_data_17.file = "functions.c";
+    __gen_e_acsl_assert_data_17.fct = "main";
+    __gen_e_acsl_assert_data_17.line = 87;
+    __e_acsl_assert(__gen_e_acsl_f_here_2 == 27,
+                    & __gen_e_acsl_assert_data_17);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_17);
+  }
+  /*@ assert f_here(27) == 27; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
@@ -638,6 +677,21 @@ double __gen_e_acsl_f2(double x)
   return __gen_e_acsl__9;
 }
 
+/*@ assigns \result;
+    assigns \result \from x; */
+int __gen_e_acsl_p_here(int x)
+{
+  int __retres = x > 0;
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from x; */
+int __gen_e_acsl_f_here(int x)
+{
+  return x;
+}
+
 /*@ assigns \result;
     assigns \result \from x; */
 int __gen_e_acsl_f_sum(int x)