diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
index 3eb2e3333c056f94cff95093f58d988a7e756d11..0d5c159a5b4fa4d713226ab96db183c03a8b9e8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: function contract
-   EXECNOW: LOG gen_function_contract.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && ./gcc_test.sh function_contract
-   EXECNOW: LOG gen_function_contract2.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_test.sh function_contract2
+   EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && ./gcc_test.sh function_contract
+   EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && ./gcc_test.sh function_contract2
 */
 
 int X = 0, Y = 2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
index 4d72b51f8ba260f3426db19bb800d5d9baca0e25..6086959108b1a8e8029d56591f7aaa3c1ae226b6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
@@ -1,7 +1,7 @@
 /* run.config
    COMMENT: integer constant + a stmt after the assertion
-   EXECNOW: LOG gen_integer_constant.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_test.sh integer_constant
-   EXECNOW: LOG gen_integer_constant2.c @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
+   EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_test.sh integer_constant
+   EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
 */
 int main(void) {
   int x;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
index ae0498739bb2ffa1954faf8bc41c1227a2b0ff28..da412680b27e82b5338983d276994761738c674c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/localvar.c
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: allocation and de-allocation of local variables
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+   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_localvar.c BIN gen_localvar.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar.c > /dev/null && ./gcc_test.sh localvar
    EXECNOW: LOG gen_localvar2.c BIN gen_localvar2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/localvar.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_localvar2.c > /dev/null && ./gcc_test.sh localvar2
 */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index 8c14c1dc41cf2b1177733f8c6ee8b33f39a64634..c74dc7aff5c7cdb45a72b879eabcebdc6bd54c00 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: \valid
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+   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_valid.c BIN gen_valid.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid.c > /dev/null && ./gcc_test.sh valid
    EXECNOW: LOG gen_valid2.c BIN gen_valid2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid2.c > /dev/null && ./gcc_test.sh valid2
 */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
index c9e34945da5ac6fa3345ccde2aa878068290a82a..00b6add38033a7cc94f63fb5d6eac4844dd6b3af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_alias.c
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: \valid in presence of aliasing
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+   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_valid_alias.c BIN gen_valid_alias.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias.c > /dev/null && ./gcc_test.sh valid_alias
    EXECNOW: LOG gen_valid_alias2.c BIN gen_valid_alias2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_alias.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_alias2.c > /dev/null && ./gcc_test.sh valid_alias2
 */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
index 262ee31b7293e3421005f774a26708bf6a2e6eed..63c607d1e839e5271999726f482f2896fa753d69 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid_in_contract.c
@@ -1,6 +1,6 @@
 /* run.config
    COMMENT: function contract involving \valid
-   STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin _malloc:Frama_C_alloc_size -val-builtin _free:Frama_C_free -val-split-return-function _initialized:0 -slevel 2"
+   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_valid_in_contract.c BIN gen_valid_in_contract.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract.c > /dev/null && ./gcc_test.sh valid_in_contract
    EXECNOW: LOG gen_valid_in_contract2.c BIN gen_valid_in_contract2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/valid_in_contract.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_valid_in_contract2.c > /dev/null && ./gcc_test.sh valid_in_contract2
 */