diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
index 4f72855791d3a54ddfbcff322451890de1db1df6..f0324f6405dc1d5800fb571a2439291f4085ee97 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
@@ -1,5 +1,5 @@
 /* run.config
-   COMMENT: linear search (example of the SAC'13 article)
+   COMMENT: linear search (example from the SAC'13 article)
    EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && ./gcc_runtime.sh linear_search
    EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_runtime.sh linear_search2
 */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 45a24b77ddd2a9497c732e87c4c2a77d92f49865..6b59fc96e3cc0306e04073eddbe39a644a1e4818 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -98,18 +98,18 @@ struct list *f(struct list *l)
   struct list *__retres;
   __store_block((void *)(& __retres),4U);
   __store_block((void *)(& l),4U);
-  if (l == (void *)0) {
+  if (l == (struct list *)0) {
     __full_init((void *)(& __retres));
     __retres = l;
     goto return_label;
   }
-  if (l->next == (void *)0) {
+  if (l->next == (struct list *)0) {
     __full_init((void *)(& __retres));
     __retres = l;
     goto return_label;
   }
   __full_init((void *)(& __retres));
-  __retres = (struct list *)((void *)0);
+  __retres = (struct list *)0;
   return_label:
     __delete_block((void *)(& l));
     __delete_block((void *)(& __retres));
@@ -187,7 +187,7 @@ struct list *__e_acsl_f(struct list *l)
 int main(void)
 {
   int __retres;
-  __e_acsl_f((struct list *)((void *)0));
+  __e_acsl_f((struct list *)0);
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 45a24b77ddd2a9497c732e87c4c2a77d92f49865..6b59fc96e3cc0306e04073eddbe39a644a1e4818 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -98,18 +98,18 @@ struct list *f(struct list *l)
   struct list *__retres;
   __store_block((void *)(& __retres),4U);
   __store_block((void *)(& l),4U);
-  if (l == (void *)0) {
+  if (l == (struct list *)0) {
     __full_init((void *)(& __retres));
     __retres = l;
     goto return_label;
   }
-  if (l->next == (void *)0) {
+  if (l->next == (struct list *)0) {
     __full_init((void *)(& __retres));
     __retres = l;
     goto return_label;
   }
   __full_init((void *)(& __retres));
-  __retres = (struct list *)((void *)0);
+  __retres = (struct list *)0;
   return_label:
     __delete_block((void *)(& l));
     __delete_block((void *)(& __retres));
@@ -187,7 +187,7 @@ struct list *__e_acsl_f(struct list *l)
 int main(void)
 {
   int __retres;
-  __e_acsl_f((struct list *)((void *)0));
+  __e_acsl_f((struct list *)0);
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
index 6000f8fb4f899bf620bb4f89242728132df66cf9..b3277552b8568313cd90bbacdd895d355437ac44 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
@@ -25,8 +25,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index ed5739d6aa150d63e00ac048663cba8e03ba4464..d769c2b730b67d277d3595ff63aea6e6b9574135 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -47,8 +47,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.