diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
index 76bd3467780dbaeec8a7aef37d428ecf20a71ca7..5a0ecd8ab3fc64fcf7577ab490e2c83425b1c4b3 100644
--- a/src/kernel_internals/runtime/boot.ml
+++ b/src/kernel_internals/runtime/boot.ml
@@ -59,7 +59,6 @@ let () = Db.Main.play := play_analysis
 
 (* Main: let's go! *)
 let () =
-  Cil_printer.state.Printer_api.print_cil_as_is <- Kernel.debug_atleast 1;
   Sys.catch_break true;
   let f () =
     ignore (Project.create "default");
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 7ca79d3e27a693cf03c3c98cb15f69cc44ebf907..2afe7bfc31ffbf04f057b23e73ad4d9f9cccd5cd 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -522,7 +522,15 @@ class cil_printer () = object (self)
 
   val mutable logic_printer_enabled = true
 
-  method reset () = ()
+  val mutable verbose = false
+  (* Do not add a value that depends on a
+     non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
+     to the way the pretty-printing class is instantiated, this value would be
+     evaluated too soon. Override the [reset] method instead. *)
+
+  method reset () =
+    verbose <- Kernel.debug_atleast 1;
+    state.print_cil_as_is <- Kernel.debug_atleast 1 || Kernel.PrintAsIs.get()
 
   method pp_keyword fmt s = pp_print_string fmt s
   method pp_acsl_keyword = self#pp_keyword
@@ -546,12 +554,6 @@ class cil_printer () = object (self)
     (if block then Pretty_utils.pp_close_block else Format.fprintf)
       fmt "%(%)" suf
 
-  val mutable verbose = false
-  (* Do not add a value that depends on a
-     non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
-     to the way the pretty-printing class is instantiated, this value would be
-     evaluated too soon. Override the [reset] method instead. *)
-
   (* indicates whether we are printing ghost elements *)
   val mutable is_ghost = false
   method private display_comment () = not is_ghost || verbose
@@ -3406,7 +3408,6 @@ class cil_printer () = object (self)
 
   method file fmt file =
     fprintf fmt "@[/* Generated by Frama-C */@\n" ;
-    state.print_cil_as_is <- state.print_cil_as_is || Kernel.PrintAsIs.get ();
     print_std_includes fmt file.globals;
     Cil.iterGlobals file (fun g -> self#global fmt g);
     fprintf fmt "@]@."
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index c8e1bac0d46a728fd3b9b5893f68b4f675d67890..aa74c0cc535e4a9b583243ffb1c973b30a57df4c 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -96,7 +96,6 @@ class printer_with_annot () = object (self)
 
   method! reset () =
     super#reset ();
-    verbose <- Kernel.debug_atleast 1;
     declared_globs <- Cil_datatype.Varinfo.Set.empty;
     print_spec <- false
 
diff --git a/tests/pdg/oracle/dyn_dpds.res.oracle b/tests/pdg/oracle/dyn_dpds.res.oracle
index 658d717167d486e40fee9e8561a91e94832cd3ed..7a8f17e711a5ffcf5f46ada7b3907b49075c29fa 100644
--- a/tests/pdg/oracle/dyn_dpds.res.oracle
+++ b/tests/pdg/oracle/dyn_dpds.res.oracle
@@ -40,6 +40,9 @@ int main(int a, int b, int c)
     x = - x;
     /* sid:6 */
     /*@ assert *p > G; */ ;
+  }
+  else {
+    
   }
   /* sid:9 */
   return x;
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index e3f67044af38fd7e0b6bc3940c501fb55455fc03..496a8f1ac4c893c631e765c4dd9838e59bf6a11f 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -973,9 +973,15 @@
   
   int max(int i, int j)
   {
+    /* Locals: tmp */
     int tmp;
-    
-    if (i >= j) tmp = i; else tmp = j;
+    ;
+    if (i >= j) {
+      tmp = i;
+    }
+    else {
+      tmp = j;
+    }
     return tmp;
   }
 [kernel:file:annotation] Marking properties