diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
index 1ca2b8df2848a1e9b695428903b392deed3de0d2..a605bbdb95f10e6f31fb443915653495c2e7ae4a 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
@@ -26,6 +26,7 @@
 ***************************************************************************/
 
 #include "../../internals/e_acsl_malloc.h"
+#include "../../internals/e_acsl_private_assert.h"
 
 #include "e_acsl_bittree.h"
 
@@ -160,7 +161,7 @@ static bt_node * bt_get_leaf_from_block (bt_block * ptr) {
 	    == (ptr->ptr & curr->left->mask))
       curr = curr->left;
     else
-      vassert(0, "Unreachable", NULL);
+      private_assert(0, "Unreachable", NULL);
   }
   DASSERT(curr->is_leaf);
   DASSERT(curr->leaf == ptr);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index b48e6e1866f1bb6aac54c5056c2ddbd072897b93..e729c281313b6d416e029212f012a2cc90f31695 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -31,7 +31,7 @@
 #include "../../internals/e_acsl_private_assert.h"
 #include "../../instrumentation_model/e_acsl_temporal.h"
 #include "../../numerical_model/e_acsl_floating_point.h"
-#include "../internals/e_acsl_safe_locations.h""
+#include "../internals/e_acsl_safe_locations.h"
 #include "e_acsl_bittree.h"
 
 #include "../e_acsl_observation_model.h"
@@ -231,12 +231,12 @@ int eacsl_valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
   bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return
     size == 0
-    ||
+    || (
     blk != NULL && !blk->is_readonly
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
 #endif
-  ;
+    );
 }
 
 /* return whether the size bytes of ptr are readable */
@@ -244,12 +244,12 @@ int eacsl_valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base)
   bt_block * blk = lookup_allocated(ptr, size, ptr_base);
   return
     size == 0
-    ||
+    || (
     blk != NULL
 #ifdef E_ACSL_TEMPORAL
     && temporal_valid(ptr_base, addrof_base)
 #endif
-  ;
+    );
 }
 
 /* return the base address of the block containing ptr */
@@ -260,7 +260,7 @@ void* eacsl_base_addr(void* ptr) {
 }
 
 /* return the offset of `ptr` within its block */
-size_t offset(void* ptr) {
+size_t eacsl_offset(void* ptr) {
   bt_block * tmp = bt_find(ptr);
   private_assert(tmp != NULL, "\\offset of unallocated memory", NULL);
   return ((uintptr_t)ptr - tmp->ptr);
@@ -585,7 +585,7 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   /* Tracking safe locations */
   collect_safe_locations();
   int i;
-  for (i = 0; i < get_safe_location_count(); i++) {
+  for (i = 0; i < get_safe_locations_count(); i++) {
     memory_location * loc = get_safe_location(i);
     void *addr = (void*)loc->address;
     uintptr_t len = loc->length;
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c
new file mode 100644
index 0000000000000000000000000000000000000000..efdd82a5ee0f2c74f1cc055f005cb40cce853a5d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+  COMMENT: Compile RTL with bittree memory model
+  STDOPT:#"-e-acsl-full-mtracking"
+  MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model bittree
+ */
+int main() {
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c
new file mode 100644
index 0000000000000000000000000000000000000000..d9bf523c54916e4d2decf42fe5b3342b3415c9ba
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c
@@ -0,0 +1,8 @@
+/* run.config_ci, run.config_dev
+  COMMENT: Compile RTL with segment memory model
+  STDOPT:#"-e-acsl-full-mtracking"
+  MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model segment
+ */
+int main() {
+  return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.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/e-acsl-segment-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.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-bittree-model.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c
new file mode 100644
index 0000000000000000000000000000000000000000..8673c9a15aa2ccbb782ab75e2700cd10b95d9cf2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c
@@ -0,0 +1,16 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(& __retres),(size_t)4);
+  __e_acsl_full_init((void *)(& __retres));
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c
new file mode 100644
index 0000000000000000000000000000000000000000..8673c9a15aa2ccbb782ab75e2700cd10b95d9cf2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c
@@ -0,0 +1,16 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_store_block((void *)(& __retres),(size_t)4);
+  __e_acsl_full_init((void *)(& __retres));
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-bittree-model.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-bittree-model.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-segment-model.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-segment-model.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391