diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.ml b/src/plugins/e-acsl/src/code_generator/typed_number.ml index d9496e647c7ab39432099d49940459b5bb81a1a4..c11eb87ca6ffc76a8f3f956bee8c3bcf6329bb72 100644 --- a/src/plugins/e-acsl/src/code_generator/typed_number.ml +++ b/src/plugins/e-acsl/src/code_generator/typed_number.ml @@ -57,7 +57,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e = Gmp.Z.create ~loc ?name t_opt env kf e | _, false -> if Gmp_types.Q.is_t ctx then - if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *) + if Gmp_types.Q.is_t ty then (* R --> R *) e, env else (* C integer or Z --> R *) Gmp.Q.create ~loc ?name t_opt env kf e