diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 82f3d1d0f06733038fde09914c47ac9d2ea069d7..65a709f093fea2e4416895ef5b74a7e3f47557d8 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -721,10 +721,12 @@ class cil_printer () = object (self)
     let fundecl = if Cil.isFunctionType v.vtype then Some v else None in
     let v = { v with vtype = self#no_ghost_at_first_level v.vtype } in
     let v =
-      match v.vtype with
-      | TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
-        { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
-      | _ -> v
+      if state.print_cil_as_is then v else begin
+        match v.vtype with
+        | TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
+          { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
+        | _ -> v
+      end
     in
     (* First the storage modifiers *)
     fprintf fmt "%s%a%a%s%a%a"