diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index 3e7ab96b05caa50cafe33637a07645fb55f6b9c1..28f202ce09a3f221389ba0aa941202dd89dec9e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1 +1 @@
-STDOPT: +"-e-acsl-project p" +"-then-on p" +"-print" +"-val"
+STDOPT: +"-e-acsl-project p" +"-then-on p" +"-check" +"-print" +"-val"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a556874d14df91475efc95f7501023dbf7975af2..3c5e837604e9d4ba6477a9a8c21c3eaf935c4cfd 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -329,7 +329,7 @@ let convert_behaviors only_behaviors env behaviors =
   in
   Env.close_block_option pre_env, 
   Env.close_block_option post_env,
-  Env.merge_function_vars ~from:pre_env post_env
+  Env.merge_function_vars ~from:post_env pre_env
 
 let convert_spec only_behaviors env spec =
   if spec.spec_variant <> None then Misc.not_yet "variant clause";
@@ -350,10 +350,10 @@ let convert_annotation env annot =
       if l <> [] then Misc.not_yet "assertions applied only on some behaviors";
       convert_named_predicate env p, None
     | AStmtSpec(only_behaviors, spec) -> 
-      let pre_block, post_block, post_env = 
+      let pre_block, post_block, new_env = 
 	convert_spec only_behaviors env spec 
       in
-      let env = Env.merge_function_vars ~from:post_env env in
+      let env = Env.merge_function_vars ~from:new_env env in
       let env = match pre_block with
 	| None -> env
 	| Some b -> Env.add_stmt env (mkStmt ~valid_sid:true (Block b))