diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 1b38c7811ad60893dd8f275862ee13df3a652ec1..c4abdd45fd4bef8f44f6f8caf59726bc8a444741 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -117,9 +117,13 @@ let typ_of_lty = function
 type computed_info =
   { ty: Number_ty.t;  (* type required for the term *)
     cast: Number_ty.t option; (* if not [None], type of the context which the term
-                                 must be casted to. If [None], no cast needed. *)
+                                 must be cast to. If [None], no cast needed. *)
   }
 
+let pp_computed_info fmt ci =
+  let pp_cast fmt c = Format.fprintf fmt "(%a)" Number_ty.pretty c in
+  Format.fprintf fmt "%a%a" (Pretty_utils.pp_opt pp_cast) ci.cast Number_ty.pretty ci.ty
+
 (* Memoization module which retrieves the computed info of some terms. If the
    info is already computed for a term, it is never recomputed *)
 module Memo: sig
@@ -357,6 +361,7 @@ let rec type_term
     ?ctx
     ~profile
     t =
+  Options.feedback ~dkey ~level:5 "typing (sub-)term %a" Printer.pp_term t;
   let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
   let compute_ctx ?ctx i =
     (* in order to get a minimal amount of generated casts for operators, the
@@ -712,7 +717,10 @@ let rec type_term
          | Some ctx -> coerce ~arith_operand ~ctx ty)
       t
   with
-  | Result.Ok res -> res
+  | Result.Ok result ->
+    Options.debug ~dkey "type_term ~ctx:%a %a = %a"
+      (Pretty_utils.pp_opt Number_ty.pretty) ctx Printer.pp_term t pp_computed_info result;
+    result
   | Result.Error exn -> raise exn
 
 and type_term_lval ~profile (host, offset) =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 714cf3ba890d23ecac351d209b55c3a5125c3fb3..8ae9ce55f459495068880d4a88d8146bc4ca5979 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -170,7 +170,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
     let ty_op = Typing.get_typ ~logic_env t in
     let ty_k = match Typing.get_cast ~logic_env t_min with
       | Some e -> e
-      | _ -> Options.fatal "unexpected error in \\sum translation"
+      | _ -> Options.fatal ~dkey "unexpected error in \\sum translation"
     in
     let e_min, adata, env = to_exp ~adata kf env t_min in
     let e_max, adata, env = to_exp ~adata kf env t_max in
@@ -865,37 +865,43 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
    constructs. *)
 and to_exp ~adata ?inplace kf env t =
   let generate_rte = Env.generate_rte env in
-  Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
+  Options.feedback ~dkey ~level:5 "translating term %a (rte? %b) in local \
                                    environment '%a'"
     Printer.pp_term t generate_rte Profile.pretty
     (Env.Logic_env.get_profile env);
   let logic_env = Env.Logic_env.get env in
   let t = Logic_normalizer.get_term t in
-  Extlib.flatten
-    (Env.with_params_and_result
-       ~rte:false
-       ~f:(fun env ->
-           let e, adata, env, sty, name =
-             context_insensitive_term_to_exp ?inplace ~adata kf env t
-           in
-           let env =
-             if generate_rte then !translate_rte_exp_ref kf env e else env
-           in
-           let cast = Typing.get_cast ~logic_env t in
-           let name = if name = "" then None else Some name in
-           Extlib.nest
-             adata
-             (Typed_number.add_cast
-                ~loc:t.term_loc
-                ?name
-                env
-                kf
-                cast
-                sty
-                (Some t)
-                e)
-         )
-       env)
+  let (rexp, _, _) as result =
+    Extlib.flatten
+      (Env.with_params_and_result
+         ~rte:false
+         ~f:(fun env ->
+             let e, adata, env, sty, name =
+               context_insensitive_term_to_exp ?inplace ~adata kf env t
+             in
+             let env =
+               if generate_rte then !translate_rte_exp_ref kf env e else env
+             in
+             let cast = Typing.get_cast ~logic_env t in
+             let name = if name = "" then None else Some name in
+             Extlib.nest
+               adata
+               (Typed_number.add_cast
+                  ~loc:t.term_loc
+                  ?name
+                  env
+                  kf
+                  cast
+                  sty
+                  (Some t)
+                  e)
+           )
+         env)
+  in
+  Options.debug ~dkey ~level:4 "to_exp %a = %a"
+    Printer.pp_term t Printer.pp_exp rexp;
+  result
+
 
 let term_to_exp_without_inplace ~adata kf env t = to_exp ~adata kf env t