diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 56bdc4be01fa55488dceaaea12694183e084388d..166bab88bf123e829412ac3c1e7d8524a0ba5329 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2903,13 +2903,14 @@ let areCompatibleTypes ?context t1 t2 =
 (* Specify whether the cast is from the source code *)
 let rec castTo ?context ?(fromsource=false)
     (ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
-  Kernel.debug ~dkey:Kernel.dkey_typing_cast "@[%t: castTo:%s %a->%a@\n@]"
+  let dkey = Kernel.dkey_typing_cast in
+  Kernel.debug ~dkey "@[%t: castTo:%s %a->%a@\n@]"
     Cil.pp_thisloc (if fromsource then "(source)" else "")
     Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt;
   if not fromsource && not (need_cast ot nt) then begin
     (* Do not put the cast if it is not necessary, unless it is from the
      * source. *)
-    Kernel.debug ~dkey:Kernel.dkey_typing_cast "no cast to perform";
+    Kernel.debug ~dkey "no cast to perform";
     (ot, e)
   end else begin
     let nt = if fromsource then nt else !typeForInsertedCast e ot nt in
@@ -2921,8 +2922,7 @@ let rec castTo ?context ?(fromsource=false)
     in
     (*  [BM] uncomment the following line to enable attributes static typing
         ignore (check_strict_attributes true ot nt  && check_strict_attributes false nt ot);*)
-    Kernel.debug ~dkey:Kernel.dkey_typing_cast
-      "@[castTo: ot=%a nt=%a\n  result is %a@\n@]"
+    Kernel.debug ~dkey "@[castTo: ot=%a nt=%a\n  result is %a@\n@]"
       Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt
       Cil_printer.pp_exp (snd result);
     (* Now see if we can have a cast here *)
@@ -2930,14 +2930,19 @@ let rec castTo ?context ?(fromsource=false)
     | TNamed _, _
     | _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in castTo"
     | t, TInt(IBool,_) when is_scalar_type t ->
-      if is_boolean_result e then result
-      else
+      if is_boolean_result e then begin
+        Kernel.debug ~dkey "Explicit cast to Boolean: %a" Cil_printer.pp_exp e;
+        nt,Cil.mkCastT ~oldt:ot ~newt:nt e
+      end else begin
+        Kernel.debug ~dkey
+          "bool conversion by checking !=0: %a" Cil_printer.pp_exp e;
         nt,
         Cil.mkCastT
           ~oldt:ot ~newt:nt
           (constFold true
              (new_exp  ~loc:e.eloc
                 (BinOp(Ne,e,Cil.integer ~loc:e.eloc 0,intType))))
+      end
     | TInt(_,_), TInt(_,_) ->
       (* We used to ignore attributes on integer-integer casts. Not anymore *)
       (* if ikindo = ikindn then (nt, e) else *)
@@ -3046,12 +3051,12 @@ let rec castTo ?context ?(fromsource=false)
       result
 
     | (TInt _ | TPtr _), TBuiltin_va_list _ ->
-      Kernel.debug ~dkey:Kernel.dkey_typing_cast ~current:true
+      Kernel.debug ~dkey ~current:true
         "Casting %a to __builtin_va_list" Cil_datatype.Typ.pretty ot ;
       result
 
     | TPtr _, TEnum _ ->
-      Kernel.debug ~dkey:Kernel.dkey_typing_cast ~current:true
+      Kernel.debug ~dkey ~current:true
         "Casting a pointer into an enumeration type" ;
       result