diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 3b9f31eb7b51e88e461c82e32c794744c4a691f1..6ec351f314db9a34aec63b1fb8b6388b9070943d 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -243,6 +243,8 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
       in
       let guard = stmts_block guard_blk in
       (* increment the loop counter [x++] *)
+      (* TODO: should check that it does not overflow in the case of the type
+         of the loop variable is __declared__ too small. *)
       let tlv_one = t_plus_one tlv in
       (* previous typing ensures that [x++] fits type [ty] *)
       Typing.type_term ~use_gmp_opt:false ~ctx:ctx_one tlv_one;
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/gmp/quantif.i
index c6e7b2d842ec255cef193f8c3b9a3a1738ca2232..e7870dc4f325228ceca1bf2a370c3e1d7db6f967 100644
--- a/src/plugins/e-acsl/tests/gmp/quantif.i
+++ b/src/plugins/e-acsl/tests/gmp/quantif.i
@@ -28,6 +28,7 @@ int main(void) {
   { // Gitlab issue #42
     int buf[10];
     /*@ assert \forall integer i; 0 <= i < 10 ==> \valid(buf+i); */
+    /*@ assert \forall char i; 0 <= i < 10 ==> \valid(buf+i); */
   }
 
   return 0;
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 3ad11c0c70e4e830db5ebd964effc6525b8e6060..ca61314a6aee253d4e46f5d03e5df4275c6ba217 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -567,7 +567,7 @@ let rec type_predicate p =
             | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmp i)
             | Ctype ty ->
               (match Cil.unrollType ty with
-              | TInt(ik, _) -> C_type ik
+              | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
               | ty ->
                 Options.fatal "unexpected type %a for quantified variable %a"
                   Printer.pp_typ ty