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 ed63e1f988aaf31a4c2be99a2aa44649e2b2c547..ecbe431cb85bed2372da6e904116aa2cd58f3361 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
@@ -7,7 +7,7 @@ int main(void) {
   int x;
   /*@ assert 0 == 0; */ x = 0;
   /*@ assert 0 != 1; */
-  /*@ assert 0xfffffffffffffff == 0xfffffffffffffff; */
+  /*@ assert 1152921504606846975 == 0xfffffffffffffff; */
 
   /* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index dc3fe0bba1cbcdb4b6fe2e0f1cfc4bb8be895ff3..2f8d4ef60a31a932823211867a42b6a45f2fca2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -593,14 +593,14 @@ int main(void)
     __gmpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
-  /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+  /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
   { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
     __gmpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
     __gmpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
     e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
                           (__mpz_struct const *)(e_acsl_8));
     if (! (e_acsl_9 == 0)) {
-      e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+      e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
     } __gmpz_clear((__mpz_struct *)(e_acsl_7));
     __gmpz_clear((__mpz_struct *)(e_acsl_8));
   }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index ea258f13f9db0799dff835eb95675557af7f4cd8..a5656a259232c0bebe4153ce01544d7d9c1073c1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -175,14 +175,14 @@ int main(void)
     mpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
-  /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+  /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
   { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
     mpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
     mpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
     e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
                        (__mpz_struct const *)(e_acsl_8));
     if (! (e_acsl_9 == 0)) {
-      e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+      e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
     } mpz_clear((__mpz_struct *)(e_acsl_7));
     mpz_clear((__mpz_struct *)(e_acsl_8));
   }
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4677d7dc5b5e4fdc06be8ab2adc74a1aaab5522a..71b84af223a3e677a25889776f16640d7a25ea72 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -230,14 +230,17 @@ end
 (* ************************************************************************** *)
 
 let constant_to_exp ?(loc=Location.unknown) = function
-  | CInt64(n, k, s) ->
-    (match k with
-    | IBool | IChar | IUChar | IUInt | IUShort | IULong
-    | ISChar | IShort | IInt | ILong ->
-      kinteger64_repr ?loc k n s
-    | ILongLong | IULongLong ->
-      mkString ?loc (Int64.to_string n))
-  | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> new_exp ?loc (Const c)
+  | CInt64(n, 
+	   (IBool | IChar | IUChar | IUInt | IUShort | IULong
+	       | ISChar | IShort | IInt | ILong as k), 
+	   s) ->
+    kinteger64_repr ?loc k n s
+  | CInt64(n, (ILongLong | IULongLong), _s) -> 
+    (* cannot use the string [s] if any since we do not know the base in which
+       it is written. Such a base is required by GMP. *)
+    mkString ?loc (Int64.to_string n)
+  | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> 
+    new_exp ?loc (Const c)
 
 let tlval_to_lval = function
   | TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
@@ -536,7 +539,8 @@ class e_acsl_visitor prj generate = object (self)
 	stmt 
 	Env.empty
     in
-    if Env.is_empty env then DoChildren
+    if Env.is_empty env then 
+      DoChildren
     else begin
       assert generate;
       let mk_block stmt =
@@ -548,7 +552,6 @@ class e_acsl_visitor prj generate = object (self)
 
   initializer Env.register_actions_queue self#get_filling_actions
 
-
 end
 
 let do_visit ?(prj=Project.current ()) generate =