diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index 73d3ac2b865191eaf0bab61e438854128a8e74b8..859f194de03916e47a925e10562e093c634f096f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -17,25 +17,27 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
-  __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+  __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &__fc_fopen }}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
-               [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+               [0].__fc_inode ∈
+               {{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
                [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
-               [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+               [1].__fc_inode ∈
+               {{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
   S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
                               [--..--]
                               [0].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+                                 &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0] }}
                               {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
                               [--..--]
                               [1].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+                                 &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0] }}
                               [1].__fc_real_data_max_size ∈ [--..--]
   S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
@@ -43,12 +45,12 @@
                               [--..--]
                               [0].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+                                 &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0] }}
                               {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
                               [--..--]
                               [1].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+                                 &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0] }}
                               [1].__fc_real_data_max_size ∈ [--..--]
   S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index 73d3ac2b865191eaf0bab61e438854128a8e74b8..859f194de03916e47a925e10562e093c634f096f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -17,25 +17,27 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
-  __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+  __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
   __fc_fopen[0..511] ∈ {0}
-  _p__fc_fopen ∈ {{ &__fc_fopen }}
+  _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
-               [0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }}
+               [0].__fc_inode ∈
+               {{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
                [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
-               [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
+               [1].__fc_inode ∈
+               {{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
   S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
                               [--..--]
                               [0].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }}
+                                 &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0] }}
                               {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
                               [--..--]
                               [1].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }}
+                                 &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0] }}
                               [1].__fc_real_data_max_size ∈ [--..--]
   S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
@@ -43,12 +45,12 @@
                               [--..--]
                               [0].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }}
+                                 &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0] }}
                               {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
                               [--..--]
                               [1].__fc_real_data ∈
                               {{ NULL ;
-                                 &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }}
+                                 &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0] }}
                               [1].__fc_real_data_max_size ∈ [--..--]
   S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
   S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]