diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/test_config b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
index 61e3a7b0e535945b6e22a3d5dca55d4ce3685bd4..475ef57bff28b613c9cf0d4fe829db396cdac650 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
@@ -1 +1,2 @@
-OPT: -e-acsl-check
+COMMENT: -e-acsl-check set by default
+STDOPT:
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 807e22c92039fbaeb416dfe8ea2dfdf33d53fa88..3e7ab96b05caa50cafe33637a07645fb55f6b9c1 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 @@
-OPT: -e-acsl-project p -then-on p -print -val
+STDOPT: +"-e-acsl-project p" +"-then-on p" +"-print" +"-val"
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index f15e29fb6c1ebbbc5f3e8e703237d95314501e31..899f3ec34cf0566d9dc7f083308f3ec0377b63ba 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,2 +1,3 @@
 CMD: FRAMAC_SHARE=./share @frama-c@ -cpp-command="gcc -C -E -I. -I${FRAMAC_SHARE}"
+OPT: -e-acsl-check
 FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|[a-zA-Z/\\]\+frama_c_project_p_[a-z0-9]*|PROJECT_FILE|"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a5df3eccacdf65740837c448cb981a0de431efb4..03c5f2bfb2fb19e48dd2340ceeb4e1bcfe06e19e 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -51,10 +51,10 @@ let mk_if e p =
   let msg =
     let b = Buffer.create 97 in
     let fmt = Format.formatter_of_buffer b in
-    let no_uni = Parameters.UseUnicode.get () in
-    Parameters.UseUnicode.off ();
+    let no_uni = Parameters.Unicode.get () in
+    Parameters.Unicode.off ();
     Format.fprintf fmt "%a@?" Cil.d_predicate_named p;
-    Parameters.UseUnicode.set no_uni;
+    Parameters.Unicode.set no_uni;
     Buffer.contents b
   in
   let s = mk_call "e_acsl_fail" [ mkString unknown_loc msg ] in
@@ -262,6 +262,15 @@ let rec term_to_exp t = match t.term_node with
     let e2 = term_to_exp t2 in
     assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
     let name = name_of_mpz_arith_bop bop in
+(*    (* guarding divisions and modulos *)
+    (match bop with
+    | Div | Mod ->
+      let e =
+	if Mpz.e_got_t e2 then
+	  New_vars.push_and_mpz_init (fun _ e -> mk_call "mpz_cmp"
+      New_block.push (mk_if e2 t2
+	(mkStmt ~valid_sid:true (If(e2, , mlBlock [], unknown_loc))
+    | _ -> assert false);*)
     New_vars.push_and_mpz_init (fun _ e -> mk_call name [ e; e1; e2 ])
   | TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
     (* comparison operators *)