diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
index 0e413258b368b1aaa925b7579b4943988e11f432..9b1baa7ad970fe5d9085f12e0c179b27a69b01b7 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
@@ -39,7 +39,8 @@
  * otherwise.
  */
 int separated2(void * ptr1, size_t size1, void * ptr2, size_t size2) {
-  DASSERT(valid_read(ptr1, size1, base_addr(ptr1), NULL) && valid_read(ptr2, size2, base_addr(ptr2), NULL));
+  DASSERT(eacsl_valid_read(ptr1, size1, eacsl_base_addr(ptr1), NULL)
+          && eacsl_valid_read(ptr2, size2, eacsl_base_addr(ptr2), NULL));
 
   // Cast pointers to char* to be able to do pointer arithmetic without
   // triggering undefined behavior
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
new file mode 100644
index 0000000000000000000000000000000000000000..8d050c12439f462c3148f4f3dcde4456249f974c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+  COMMENT: Compile RTL with debug and debug verbose informations
+  STDOPT:#"-e-acsl-debug 1"
+  MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose
+ */
+int main() {
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c
new file mode 100644
index 0000000000000000000000000000000000000000..5884b0f6c6078320062404a8fcf96f5158f24dc4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c
@@ -0,0 +1,11 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391