diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 4a1e5e711d7024edf490b74237e69ea1eec76c58..d3cb04b390b2186a1ea41901c4da623ced7967df 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-  E-ACSL       [2020-06-19] Add support to create GMP rational from GMP
+                integer. (frama-c/e-acsl#120)
 -* E-ACSL       [2020-06-18] Fix support of VLA memory tracking.
                 (frama-c/e-acsl#119)
 
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
index 625d41ea3e4a89d66a369913c8b75db81ec1c4bd..39946e50b149fcb452fdd858f0dfba24b28ac6c7 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
@@ -154,6 +154,12 @@ extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
 extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid_read(z_orig);
+  @ requires \valid(q);
+  @ assigns *q \from *z_orig; */
+extern void __gmpq_set_z(mpq_t q, const mpz_t z_orig)
+  __attribute__((FC_BUILTIN));
+
 /*@ allocates q;
   @ ensures \valid(q);
   @ ensures \initialized(q);
@@ -173,6 +179,12 @@ extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
 extern void __gmpz_set_si(mpz_t z, signed long int n)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid_read(q_orig);
+  @ requires \valid(z);
+  @ assigns *z \from *q_orig; */
+extern void __gmpz_set_q(mpz_t z, const mpq_t q_orig)
+  __attribute__((FC_BUILTIN));
+
 /*************/
 /* Finalizer */
 /*************/
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index fa5d75b572de2c4bbe5e6c241f7322690496f328..9d2590f9bb43d97691287382eb237c27bc06868c 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -262,16 +262,21 @@ let coerce ~arith_operand ~ctx ~op ty =
   then { ty; op; cast = Some ctx }
   else { ty; op; cast = None }
 
-let number_ty_of_typ ty = match Cil.unrollType ty with
-  | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
-  | TFloat(fk, _) -> C_float fk
-  | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
-  | TNamed _ -> assert false
+let number_ty_of_typ ~post ty =
+  (* Consider GMP types only in a post typing phase *)
+  if post && Gmp_types.Z.is_t ty then Gmpz
+  else if post && Gmp_types.Q.is_t ty then Rational
+  else
+    match Cil.unrollType ty with
+    | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
+    | TFloat(fk, _) -> C_float fk
+    | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
+    | TNamed _ -> assert false
 
 let ty_of_logic_ty ?term lty =
   let get_ty = function
     | Linteger -> Gmpz
-    | Ctype ty -> number_ty_of_typ ty
+    | Ctype ty -> number_ty_of_typ ~post:false ty
     | Lreal -> Real
     | Larrow _ -> Nan
     | Ltype _ -> Error.not_yet "user-defined logic type"
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 8002d23e4a2fa3339d2d30334e2e6fb0b95814b8..7a7fd0f80d5df014274881863363855978cb820c 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -79,8 +79,12 @@ val typ_of_number_ty: number_ty -> typ
     for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].
     @raise Not_a_number in case of [Nan]. *)
 
-val number_ty_of_typ: typ -> number_ty
-(** Reverse of [typ_of_number_ty] *)
+val number_ty_of_typ: post:bool -> typ -> number_ty
+(** Reverse of [typ_of_number_ty]
+    [number_ty_of_typ ~post ty] return the {!number_ty} corresponding to a
+    C type. [post] indicates if the type is before or after the typing phase.
+    The GMP types will be recognized only in a post-typing phase.
+*)
 
 val join: number_ty -> number_ty -> number_ty
 (** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 89ea82b0bdf32a031d9fe4c25795decb950b0e39..b35afd1163cd65d1ab4ff68e9c93e18a94fa0323 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -42,38 +42,49 @@ exception Longlong of ikind
 
 let get_set_suffix_and_arg res_ty e =
   let ty = Cil.typeOf e in
-  if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
-  else
-    let args_uisi e =
-      if Gmp_types.Z.is_t res_ty then [ e ]
-      else begin
-        assert (Gmp_types.Q.is_t res_ty);
-        [ e; Cil.one ~loc:e.eloc ]
-      end
-    in
-    match Cil.unrollType ty with
-    | TInt(IChar, _) ->
-      (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
-       else "_si"),
-      args_uisi e
-    | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
-      "_ui", args_uisi e
-    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", args_uisi e
-    | TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
-    | TPtr(TInt(IChar, _), _) ->
-      "_str",
-      (* decimal base for the number given as string *)
-      [ e; Cil.integer ~loc:e.eloc 10 ]
-    | TFloat((FDouble | FFloat), _) ->
-      (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
-         Hence, calling [set_d] for both of them is sound.
-         HOWEVER: the machdep MUST NOT be vulnerable to double rounding
-         [TODO] check the statement above *)
-      "_d", [ e ]
-    | TFloat(FLongDouble, _) ->
-      Error.not_yet "creating gmp from long double"
-    | _ ->
-      assert false
+  let exp_number_ty = Typing.number_ty_of_typ ~post:true ty in
+  let res_number_ty = Typing.number_ty_of_typ ~post:true res_ty in
+  let args_uisi e =
+    if Gmp_types.Z.is_t res_ty then [ e ]
+    else begin
+      assert (Gmp_types.Q.is_t res_ty);
+      [ e; Cil.one ~loc:e.eloc ]
+    end
+  in
+  match (exp_number_ty, res_number_ty) with
+  | Typing.Gmpz, Typing.Gmpz | Typing.Rational, Typing.Rational ->
+    "", [ e ]
+  | Typing.Gmpz, Typing.Rational ->
+    "_z", [ e ]
+  | Typing.Rational, Typing.Gmpz ->
+    "_q", [ e ]
+  | Typing.C_integer IChar, _ ->
+    (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
+     else "_si"),
+    args_uisi e
+  | Typing.C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
+    "_ui", args_uisi e
+  | Typing.C_integer (ISChar | IShort | IInt | ILong), _ ->
+    "_si", args_uisi e
+  | Typing.C_integer (ILongLong | IULongLong as ikind), _ ->
+    raise (Longlong ikind)
+  | Typing.C_float (FDouble | FFloat), _ ->
+    (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
+       Hence, calling [set_d] for both of them is sound.
+       HOWEVER: the machdep MUST NOT be vulnerable to double rounding
+       [TODO] check the statement above *)
+    "_d", [ e ]
+  | Typing.C_float FLongDouble, _ ->
+    Error.not_yet "creating gmp from long double"
+  | Typing.Gmpz, _ | Typing.Rational, _ | Typing.Real, _ | Typing.Nan, _ -> (
+      match Cil.unrollType ty with
+      | TPtr(TInt(IChar, _), _) ->
+        "_str",
+        (* decimal base for the number given as string *)
+        [ e; Cil.integer ~loc:e.eloc 10 ]
+      | _ ->
+        assert false
+    )
 
 let generic_affect ~loc fname lv ev e =
   let ty = Cil.typeOf ev in
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 1d552fd9949088b1ba3f2210fd9382976e8b4148..3b346a01aff99acacaf0c8deec9e839cd9175c97 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -88,7 +88,10 @@ let pred_to_block ~loc kf env ret_vi p =
 
 (* Generate the function's body for terms. *)
 let term_to_block ~loc kf env ret_ty ret_vi t =
-  Typing.type_term ~use_gmp_opt:false ~ctx:(Typing.number_ty_of_typ ret_ty) t;
+  Typing.type_term
+    ~use_gmp_opt:false
+    ~ctx:(Typing.number_ty_of_typ ~post:false ret_ty)
+    t;
   let e, env = !term_to_exp_ref kf env t in
   if Cil.isVoidType ret_ty then
     (* if the function's result is a GMP, it is the first parameter of the
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 4e605aad9d0d237b2cf266cc14ea1d35f4573f4d..fe84f48fc299b5204eeb39a5439468e6b6110a5c 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -117,7 +117,7 @@ let bounds_for_small_type ~loc (t1, lv, t2) =
       let min, max = Misc.finite_min_and_max i in
       let t1 = Logic_const.tint ~loc min in
       let t2 = Logic_const.tint ~loc max in
-      let ctx = Typing.number_ty_of_typ ty in
+      let ctx = Typing.number_ty_of_typ ~post:false ty in
       (* we are assured that we will not have a GMP,
          once again because we intersected with [ity] *)
       Typing.type_term ~use_gmp_opt:false ~ctx t1;
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 172206f198ac77af4182cf62e6ade335dfd96a5c..4c0ae922b43921e75e447b0fd6e5660a77f44a26 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -32,12 +32,7 @@ let init_set ~loc lval vi_e e =
 
 let create ~loc ?name e env kf t_opt =
   let ty = Cil.typeOf e in
-  if Gmp_types.Z.is_t ty then
-    (* GMPQ has no builtin for creating Q from Z. Hence:
-       1) Get the MPZ as a string: gmZ_get_str
-       2) Set the MPQ with that string: gmpQ_set_str *)
-    Error.not_yet "reals: creating Q from Z"
-  else if Gmp_types.Q.is_t ty then
+  if Gmp_types.Q.is_t ty then
     e, env
   else
     let _, e, env =
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 6a77b6530dfb5e6fd13a9a96e9878c3b5d48c6c9..bf9eae67db938901aa42cd1b0ce60543bedef2de 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -932,7 +932,7 @@ let term_to_exp typ t =
     else if Gmp_types.Q.is_t ty then Typing.rational
     else
       match ty with
-      | TInt(ik, _) -> Typing.ikind ik
+      | TInt(ik, _) | TEnum({ ekind = ik }, _) -> Typing.ikind ik
       | TFloat(fk, _) -> Typing.fkind fk
       | _ -> Typing.nan
   in
diff --git a/src/plugins/e-acsl/tests/gmp-only/arith.i b/src/plugins/e-acsl/tests/gmp-only/arith.i
index df97877fb148968c52cd69013790c311dcf6160b..c8ebfe292942522f999afb4a47965af629f183cb 100644
--- a/src/plugins/e-acsl/tests/gmp-only/arith.i
+++ b/src/plugins/e-acsl/tests/gmp-only/arith.i
@@ -35,5 +35,8 @@ int main(void) {
 
   /*@ assert 1 - x == -x + 1; */ // test GIT issue #37
 
+  short a = 1, b = 1;
+  //@ assert a+b > 2.  - 1.; // gitlab eacsl issue #120
+
   return 0;
 }
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
index 58ff928b06ae06fc7cc29f0189bd96640c51f53b..dcdfce7343e960ffd5c60c241410b9144066c9e3 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
@@ -42,3 +42,5 @@
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/gmp-only/arith.i:36: Warning: 
   function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp-only/arith.i:39: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index dc901aa064e92b92e00e8c4b63a5fb05f813fca9..9899c99482fd3a9ee9baba785b2fe903ce547253 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -677,6 +677,52 @@ int main(void)
     __gmpz_clear(__gen_e_acsl_add_7);
   }
   /*@ assert 1 - x ≡ -x + 1; */ ;
+  short a = (short)1;
+  short b = (short)1;
+  {
+    __e_acsl_mpz_t __gen_e_acsl_a;
+    __e_acsl_mpz_t __gen_e_acsl_b;
+    __e_acsl_mpq_t __gen_e_acsl__61;
+    __e_acsl_mpq_t __gen_e_acsl__62;
+    __e_acsl_mpq_t __gen_e_acsl_add_8;
+    __e_acsl_mpq_t __gen_e_acsl__63;
+    __e_acsl_mpq_t __gen_e_acsl__64;
+    __e_acsl_mpq_t __gen_e_acsl_sub_6;
+    int __gen_e_acsl_gt_2;
+    __gmpz_init_set_si(__gen_e_acsl_a,(long)a);
+    __gmpz_init_set_si(__gen_e_acsl_b,(long)b);
+    __gmpq_init(__gen_e_acsl__61);
+    __gmpq_set_z(__gen_e_acsl__61,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_a));
+    __gmpq_init(__gen_e_acsl__62);
+    __gmpq_set_z(__gen_e_acsl__62,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_b));
+    __gmpq_init(__gen_e_acsl_add_8);
+    __gmpq_add(__gen_e_acsl_add_8,
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__61),
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__62));
+    __gmpq_init(__gen_e_acsl__63);
+    __gmpq_set_d(__gen_e_acsl__63,2.);
+    __gmpq_init(__gen_e_acsl__64);
+    __gmpq_set_d(__gen_e_acsl__64,1.);
+    __gmpq_init(__gen_e_acsl_sub_6);
+    __gmpq_sub(__gen_e_acsl_sub_6,
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__63),
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__64));
+    __gen_e_acsl_gt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_8),
+                                   (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub_6));
+    __e_acsl_assert(__gen_e_acsl_gt_2 > 0,"Assertion","main",
+                    "a + b > 2. - 1.","tests/gmp-only/arith.i",39);
+    __gmpz_clear(__gen_e_acsl_a);
+    __gmpz_clear(__gen_e_acsl_b);
+    __gmpq_clear(__gen_e_acsl__61);
+    __gmpq_clear(__gen_e_acsl__62);
+    __gmpq_clear(__gen_e_acsl_add_8);
+    __gmpq_clear(__gen_e_acsl__63);
+    __gmpq_clear(__gen_e_acsl__64);
+    __gmpq_clear(__gen_e_acsl_sub_6);
+  }
+  /*@ assert a + b > 2. - 1.; */ ;
   __retres = 0;
   return __retres;
 }