diff --git a/src/plugins/e-acsl/tests/bts/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
index 74cba86cdbefc49eb207bda3bdbe6f3178c5f15c..eddb97a0285f9f8dbc4a6e97d19a33cc13e87ada 100644
--- a/src/plugins/e-acsl/tests/bts/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,4 +1,5 @@
 /* run.config
+   STDOPT: +"-no-val-builtins-auto"
    COMMENT: bts #1390, issue with typing of quantified variables
 */
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index 5882e8efc73d9a9c67f89d6362cf1f4db5ae4578..077c0847b439ca7600c915855d19bbb51961a4d7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:12:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:17:[value] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/runtime/initialized.c b/src/plugins/e-acsl/tests/runtime/initialized.c
index e417de91b8297907deca843419b47d999659aea6..44ca8c15992c66ee15ab420d7ff51959af509fbc 100644
--- a/src/plugins/e-acsl/tests/runtime/initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/initialized.c
@@ -1,4 +1,5 @@
 /* run.config
+   STDOPT: +"-no-val-builtins-auto"
    COMMENT: Behaviours of the \initialized E-ACSL predicate
 */
 
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index 50a7e1ed59c4c398aae5f68c6db7b25898d1bacf..ed712a0a82450f97fbb6f5f00547118629087ca2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -11,6 +11,7 @@ int main(int argc, char const **argv)
   __e_acsl_full_init((void *)(& memptr));
   int res2 =
     posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
+  /*@ assert Value: initialisation: \initialized(memptr); */
   /*@ assert Value: mem_access: \valid_read(memptr); */
   char *p = *memptr;
   __e_acsl_store_block((void *)(& p),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index f882a082af8cccb127e761dd0ece87a71c12ff87..442101a5faaeba86557e6a5311d5a0cb708794c6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,16 +1,16 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/initialized.c:65:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:69:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:347:[value] warning: function realloc: precondition got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:362:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
-tests/runtime/initialized.c:74:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:76:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:75:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:77:[value] warning: assertion got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/initialized.c:84:[value] warning: assertion got status unknown.
 tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:93:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:96:[value] warning: assertion got status unknown.
-tests/runtime/initialized.c:107:[value] warning: out of bounds write. assert \valid(partsi + i);
-tests/runtime/initialized.c:105:[value] warning: out of bounds write. assert \valid(partsc + i);
+tests/runtime/initialized.c:86:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:94:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:97:[value] warning: assertion got status unknown.
+tests/runtime/initialized.c:108:[value] warning: out of bounds write. assert \valid(partsi + i);
+tests/runtime/initialized.c:106:[value] warning: out of bounds write. assert \valid(partsc + i);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index 1bc1d7077e2cc62f6a9e4f8a06ae6a068137c79d..e3f9a03de82668f9c4ab780cdf0690e909146dcb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -17,7 +17,8 @@ tests/runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_r
 tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
 tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
 FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:92:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly reading indeterminate data
+                                         invalid base: NULL
 FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
 tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
 tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
index 45502e59bd2649da8cceadcb7adbf008095b9a2d..4ba26f48cd6e370693ebb279c4e044607f5cbfb5 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -1,17 +1,5 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
+tests/runtime/memalign.c:14:[value] warning: accessing uninitialized left-value. assert \initialized(memptr);
 tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
-tests/runtime/memalign.c:15:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/memalign.c:16:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:17:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:334:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
-tests/runtime/memalign.c:19:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
-tests/runtime/memalign.c:23:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:26:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:29:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:32:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:33:[value] warning: assertion got status unknown.
-tests/runtime/memalign.c:34:[value] warning: assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
index 7924f9d3b38cbaa18ee77d39560560729b27ebf9..efd026311297e55d8fefb674326118e6ece88624 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
@@ -1,12 +1,2 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/runtime/offset.c:39:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/runtime/offset.c:40:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:41:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:43:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:44:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:49:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:51:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:53:[value] warning: assertion got status unknown.
-tests/runtime/offset.c:55:[value] warning: assertion got status unknown.