diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index b90605ae71aa692f5ef7782a086a40be521abe88..0c1e1f185e9d0cfa37eb7e087a87b871f02fcf38 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -74,6 +74,7 @@
 /tests/e-acsl-reject/result/*.annot
 /tests/e-acsl-reject/result/*_DEP
 /tests/e-acsl-reject/result/*.log
+/tests/bts/result/*
 /tests/check/obj/*
 .frama-c
 tests/ptests_config
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 514602db126ff41d6ef2c7a9b011e080641ffbe4..81ebb9c4d0ac799a07c1f4fd450002faba4e3989 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -112,7 +112,7 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
 
 ifeq (@MAY_RUN_TESTS@,yes)
 
-PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime
+PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts
 E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config
 
 endif
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i b/src/plugins/e-acsl/tests/bts/bts1304.i
similarity index 62%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i
rename to src/plugins/e-acsl/tests/bts/bts1304.i
index b1266ba553f1861423348db1483ae36948a1bd91..ef6a48c1e39ee1d75ea0085bd0034f75c16dcc6f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i
+++ b/src/plugins/e-acsl/tests/bts/bts1304.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: argument of functions must be kept, so keep its parameter
-   EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
-   EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
+   EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
+   EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
 */
 
 struct msgA { int type; int a[2]; };
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i b/src/plugins/e-acsl/tests/bts/bts1307.i
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i
rename to src/plugins/e-acsl/tests/bts/bts1307.i
index b488258b842c99d3d89c2b919df46bc7da70fc24..12968768efdae58bf99a7ec7ca80b5d88d753330 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i
+++ b/src/plugins/e-acsl/tests/bts/bts1307.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: spec with floats and reals
-   EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
-   EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
+   EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
+   EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
 */
 
 /*@ requires \valid(Mtmax_in);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i b/src/plugins/e-acsl/tests/bts/bts1324.i
similarity index 61%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
rename to src/plugins/e-acsl/tests/bts/bts1324.i
index 05456f90c43ee56863c8059cd532c56b8e92b89e..1aa509718181d6e615f6eeb479d48d1822c7fe0b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
+++ b/src/plugins/e-acsl/tests/bts/bts1324.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: fixed bug with typing of universal quantification
-   EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
-   EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
+   EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
+   EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
 */
 
 /*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i b/src/plugins/e-acsl/tests/bts/bts1326.i
similarity index 62%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i
rename to src/plugins/e-acsl/tests/bts/bts1326.i
index 23de84e0965afb21c14c7cbae65ee4335e149c60..63412190fcabeaa061909b8c3911bbad7ff1b585 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i
+++ b/src/plugins/e-acsl/tests/bts/bts1326.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: complex term left-values
-   EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
-   EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
+   EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
+   EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
 */
 
 typedef int ArrayInt[5];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
similarity index 73%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c
rename to src/plugins/e-acsl/tests/bts/bts1390.c
index 2dbb1177cedbd38e7acbde704550b16664edddbf..0d203d313aff62eac7e75e677c925e2051eea79f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: bts #1390, issue with typing of quantified variables
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
-   EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
+   EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
+   EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
similarity index 58%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c
rename to src/plugins/e-acsl/tests/bts/bts1398.c
index 2fb52b52cc71798978b74bb879f8163246ffb7d7..c1480633d8262409de24a37362e6d53a37f16275 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: variadic function call
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
-   EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
+   EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
+   EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
 */
 
 #include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
similarity index 71%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c
rename to src/plugins/e-acsl/tests/bts/bts1399.c
index bccd7be8cae8aca2d4bca91326e95d0590c48af1..c246d7acc6b147307f5e093da9e1d0534dfd9d36 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/bts1399.c
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: complex fields and indexes + potential RTE in \initialized
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
-   EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
-   EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
+   EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
+   EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
 */
 
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c b/src/plugins/e-acsl/tests/bts/bts1478.c
similarity index 54%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
rename to src/plugins/e-acsl/tests/bts/bts1478.c
index 5270202b6e3bcccf26a1def51016a900a951c2d2..a5fadbe4dd5f0ea348e44748bb4aef1b2633dc40 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/bts1478.c
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
-   EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
-   EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
+   EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
+   EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
 */
 
 int global_i;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i b/src/plugins/e-acsl/tests/bts/bts1700.i
similarity index 59%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
rename to src/plugins/e-acsl/tests/bts/bts1700.i
index bcf7a9e9f42fdc2681324d8f9b3676feceb4c4d9..b76adfe91c3666dffe9b209e020a8e59835d8f2d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
+++ b/src/plugins/e-acsl/tests/bts/bts1700.i
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: pointer to an empty struct
-   EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
+   EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
 */
 
 struct toto {};
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i b/src/plugins/e-acsl/tests/bts/bts1717.i
similarity index 60%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i
rename to src/plugins/e-acsl/tests/bts/bts1717.i
index 5a7a6fed1571366aa2823f9c55ac3c51db837535..3164300f7513db10b5f25d0639b687a38bccb0f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i
+++ b/src/plugins/e-acsl/tests/bts/bts1717.i
@@ -1,8 +1,8 @@
 /* run.config
    COMMENT: bts #1717, issue with labels on memory-related statements
    STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
-   EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
-   EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
+   EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
+   EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
 */
 
 int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
similarity index 87%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
index 85cef0bc32432b6b63f4c57406e4a5e035b9c5dc..343190f2f5b574b50236b8e2a4ceadb1550e60c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -19,10 +19,10 @@
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 [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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
similarity index 87%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
index 85cef0bc32432b6b63f4c57406e4a5e035b9c5dc..343190f2f5b574b50236b8e2a4ceadb1550e60c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -19,10 +19,10 @@
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 [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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
similarity index 55%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
index e383dfcf607563d8df0128d208184cf33abfcc3d..838283a10e040746acee53e01273e1207ed3871e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
@@ -5,12 +5,12 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -24,21 +24,21 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
 [value] using specification for function __valid
 [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/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
 [value] using specification for function __valid_read
 [value] user error: type long double not implemented. Using double instead
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
+tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
similarity index 57%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
index 3105455c7cb3e19d815846de9f45766f9bf919e0..6edfe90528a7eed74c6d1ca1e8c9935b957ec1a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
@@ -5,12 +5,12 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -24,18 +24,18 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
 [value] using specification for function __valid
 [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/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
 [value] using specification for function __gmpz_init_set_si
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
 [value] using specification for function __gmpz_cmp
@@ -43,7 +43,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_init
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
 [value] using specification for function __gmpz_tdiv_q
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
@@ -54,16 +54,16 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
 [value] user error: type long double not implemented. Using double instead
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:19:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:20:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:21:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
index f9945f408bf1915df145ee1d8c3b3560da91683d..22f38a1f1f17bc57b72f89fdb3eaabe3873139cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1324.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __initialize
-tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
+tests/bts/bts1324.i:8:[value] entering loop for the first time
 [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/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:15:[value] entering loop for the first time
+tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:25:[value] Assertion got status valid.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
similarity index 79%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
index a40f3257ff69798155bffd4c083b25c6329ea780..2632721388e39a137fd080623f196f2cb7d1ac2f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1324.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -33,7 +33,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
+tests/bts/bts1324.i:8:[value] entering loop for the first time
 [value] using specification for function __gmpz_cmp
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
@@ -43,15 +43,15 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
 [value] using specification for function __gmpz_get_ui
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
-tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
-tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
+tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
+tests/bts/bts1324.i:15:[value] entering loop for the first time
+tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [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.
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:25:[value] Assertion got status valid.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
similarity index 83%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
index 9ccad28dc80feb2f8b185dd16b8443879ba6ecde..af73383a57f2ef56b37be39c85120145d8c62049 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1326.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -21,12 +21,12 @@
 [value] using specification for function __store_block
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
 [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.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
similarity index 88%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
index 2914d3321efb3dcfcdd0f43a14159fba92d2d15f..0e6763434b0084af7bdea79502cf2a220e0ea2a0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1326.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -21,7 +21,7 @@
 [value] using specification for function __store_block
 [value] using specification for function __initialize
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
 [value] using specification for function __gmpz_init_set_si
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
 [value] using specification for function __gmpz_init
@@ -33,7 +33,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition g
 [value] using specification for function __gmpz_cmp
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
 [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.
 [value] using specification for function __gmpz_tdiv_q
@@ -42,7 +42,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: preconditio
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
similarity index 64%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
index 18ba293c49a3f27ff2d35c58a544a84e92410b36..9a7fea6d52e7d00cbf366222993676c7e34d2f04 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1390.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -30,7 +30,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
+tests/bts/bts1390.c:15:[value] entering loop for the first time
 [value] using specification for function __gmpz_init_set_ui
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
 [value] using specification for function __gmpz_cmp
@@ -38,28 +38,28 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_get_ui
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
+tests/bts/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
 [value] using specification for function __gmpz_add
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
-tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
+tests/bts/bts1390.c:20:[value] entering loop for the first time
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
+tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] entering loop for the first time
 [value] using specification for function __offset
-tests/e-acsl-runtime/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
+tests/bts/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
 [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/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
similarity index 54%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
index 1e234aff2a324e1518c3f628816c6542aafa6687..a58c7cfbb9607044bd29139731e0a4293386ce24 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1390.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -21,23 +21,23 @@
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __literal_string
-tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
+tests/bts/bts1390.c:15:[value] entering loop for the first time
 [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/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[value] entering loop for the first time
+tests/bts/bts1390.c:20:[value] entering loop for the first time
 [value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
+tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] entering loop for the first time
 [value] using specification for function __offset
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
similarity index 97%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
index ab093acca16fb509030a5aa59e8c7ad9b82850cb..704fb9ba63ce5895925e3965a6c624fd464b3479 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1398.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
similarity index 97%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
index ab093acca16fb509030a5aa59e8c7ad9b82850cb..704fb9ba63ce5895925e3965a6c624fd464b3479 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1398.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
similarity index 86%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index dedc732a7e94ff5332e216bef6ee360890de3620..4ac929543e0e59cf7bd6d5b0273110f2d9d2d3cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -5,18 +5,18 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1399.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +39,7 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
 FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
+tests/bts/bts1399.c:24:[value] Assertion got status valid.
 [value] using specification for function __gmpz_init_set_ui
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
 [value] using specification for function __gmpz_init_set_si
@@ -49,7 +49,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_init
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
 [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.
 [value] using specification for function __gmpz_tdiv_q
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
similarity index 89%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index ca35a04cc9c4c329127c9acecf2d03e8c6c2e4bb..ba3129208337ae8709c8515d37cb01272f6c37ab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -5,16 +5,16 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1399.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
 FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
 FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
+tests/bts/bts1399.c:24:[value] Assertion got status valid.
 [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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
index 819a1984571441405e02d25f21d8592e3f2702b1..6e5736c4a8f37d9bf94e1680244a052957112759 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1478.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -22,16 +22,16 @@
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __valid
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
similarity index 77%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
index 646927eca204f29f389f8c2f13c1d6ad84bf625b..34b0792d50121ac0b11452b22282aaed18bfb45d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1478.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -22,9 +22,9 @@
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
 [value] using specification for function __gmpz_init_set_si
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
 [value] using specification for function __gmpz_cmp
@@ -36,9 +36,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
similarity index 78%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
index 825a120a9f8e3c82b7e1f80f0a8a16d71e7cd687..e7b7193eb2ffa89c19a636c8a0dce493be97590f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1700.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
   __memory_size ∈ [--..--]
 FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:150:[kernel] 0-sized location
 [value] using specification for function __store_block
-tests/e-acsl-runtime/bts1700.i:9:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+tests/bts/bts1700.i:9:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[value] Assertion got status unknown.
 [value] using specification for function __valid
 [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.
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1700.i:12:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+tests/bts/bts1700.i:12:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
similarity index 78%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
index 825a120a9f8e3c82b7e1f80f0a8a16d71e7cd687..e7b7193eb2ffa89c19a636c8a0dce493be97590f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1700.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
   __memory_size ∈ [--..--]
 FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:150:[kernel] 0-sized location
 [value] using specification for function __store_block
-tests/e-acsl-runtime/bts1700.i:9:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+tests/bts/bts1700.i:9:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[value] Assertion got status unknown.
 [value] using specification for function __valid
 [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.
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1700.i:12:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+tests/bts/bts1700.i:12:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[value] Assertion got status unknown.
 [value] using specification for function __initialized
 [value] using specification for function __delete_block
 [value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
similarity index 91%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
index a0a3562292b6e9e70035cb3f51533eb1236d7589..5aafc7dfe0f28d89c3187e175673487ab39f0340 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1717.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -20,7 +20,7 @@
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
+tests/bts/bts1717.i:13:[value] Assertion got status valid.
 [value] using specification for function __initialized
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
similarity index 91%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
index a0a3562292b6e9e70035cb3f51533eb1236d7589..5aafc7dfe0f28d89c3187e175673487ab39f0340 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
@@ -5,7 +5,7 @@
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
 [kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1717.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -20,7 +20,7 @@
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
-tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
+tests/bts/bts1717.i:13:[value] Assertion got status valid.
 [value] using specification for function __initialized
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..bcf70a16ce721877a1395b4bba98fa674a28f50c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/test_config
@@ -0,0 +1,2 @@
+OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress -no-results
+OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress -no-results