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 617549275c19e82c32f93f4f0b6dcec43adcb14c..0dc7fb06cc0ec368a1e4b5025989f6d3029f2429 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -10,6 +10,8 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __literal_string
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index e8aef1cfbc24fb5af26b9f9ba7a71658d9b5d475..a36a786f4a782f06e8c54a75812777f4cf8c3050 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -34,8 +34,5 @@
   S___fc_real_data_0_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_stdout[0..1] ∈ [--..--]
-[value] using specification for function __store_block
-[value] using specification for function __full_init
-[value] using specification for function __literal_string
 [value] using specification for function printf
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
index ad8c7116d47d459bbf4dbfce893918b1314c40b0..efd924c556296cc37747d56a5a72f0bae13e0177 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
@@ -4,8 +4,8 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-  random_counter ∈ {0}
-  rand_max ∈ {32767}
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd924c556296cc37747d56a5a72f0bae13e0177
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -0,0 +1,34 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+  __fc_random_counter ∈ {0}
+  __fc_rand_max ∈ {32767}
+  __fc_heap_status ∈ [--..--]
+  __e_acsl_init ∈ [--..--]
+  __e_acsl_internal_heap ∈ [--..--]
+  __memory_size ∈ [--..--]
+  S ∈ {0}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
+  __e_acsl_literal_string_3 ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
+tests/bts/bts1837.i:19:[value] entering loop for the first time
+tests/bts/bts1837.i:21:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid_read
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/bts/bts1837.i:22:[value] Assertion got status valid.
+[value] using specification for function __valid
+[value] using specification for function __delete_block
+tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
+tests/bts/bts1837.i:11:[value] Assertion got status valid.
+tests/bts/bts1837.i:12:[value] Assertion got status valid.
+tests/bts/bts1837.i:13:[value] Assertion got status valid.
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 5860ba5a000e1b0424a4a411aa3fa9557fc65229..6a0ea2b012a1d4a08a71e107dad3576f61b140d2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -21,8 +21,8 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
 /*@
 model __mpz_struct { ℤ n };
 */
-int random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
-unsigned long const rand_max = (unsigned long)32767;
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
 /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
 
 /*@
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index f4eedb8b927580579e693e6e9967be45e9f84632..404c5700de4f4a269ff10aabb2d70bb723ea89fe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -1,4 +1,6 @@
 /* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -127,6 +129,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
 
 void __e_acsl_memory_init(void)
 {
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
   __store_block((void *)(& stdout),8UL);
   __full_init((void *)(& stdout));
   return;
@@ -134,8 +144,6 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
-  char *__e_acsl_literal_string_2;
-  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
   FILE *f2;
@@ -144,14 +152,6 @@ int main(void)
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
-  __e_acsl_literal_string = "foo";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
-  __full_init((void *)__e_acsl_literal_string);
-  __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "wb";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __full_init((void *)(& f2));
   f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 13b9fa9cf18134adad785b59484613d3bc98d365..b583971541f9682f7dc01cedcd3cb8d663331f08 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -1,4 +1,6 @@
 /* Generated by Frama-C */
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -134,6 +136,14 @@ FILE *__e_acsl_fopen(char const *filename, char const *mode)
 
 void __e_acsl_memory_init(void)
 {
+  __e_acsl_literal_string_2 = "wb";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
   __store_block((void *)(& stdout),8UL);
   __full_init((void *)(& stdout));
   return;
@@ -141,8 +151,6 @@ void __e_acsl_memory_init(void)
 
 int main(void)
 {
-  char *__e_acsl_literal_string_2;
-  char *__e_acsl_literal_string;
   int __retres;
   FILE *f;
   FILE *f2;
@@ -151,14 +159,6 @@ int main(void)
   __store_block((void *)(& f),8UL);
   __full_init((void *)(& f));
   f = stdout;
-  __e_acsl_literal_string = "foo";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
-  __full_init((void *)__e_acsl_literal_string);
-  __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "wb";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("wb"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __full_init((void *)(& f2));
   f2 = __e_acsl_fopen(__e_acsl_literal_string,__e_acsl_literal_string_2);
   /*@ assert f ≡ __fc_stdout; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index c99d74f71f1ced6c5b1f5e0db6edaa19c73c07c9..29505bbf90343e2880360f392908c4cf5e00487e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
index c99d74f71f1ced6c5b1f5e0db6edaa19c73c07c9..29505bbf90343e2880360f392908c4cf5e00487e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.res.oracle
@@ -20,6 +20,8 @@ FRAMAC_SHARE/libc/stdio.h:95:[e-acsl] warning: E-ACSL construct `logic function
   stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+  __e_acsl_literal_string ∈ {0}
+  __e_acsl_literal_string_2 ∈ {0}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
                [--..--]
                [0].[bits 80 to 95] ∈ UNINITIALIZED