diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 522e044fa887e2251b4e1633b21b190d6c245099..b4550d92a6c071e0065b811e83d63b2848ab2dad 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1225,6 +1225,8 @@ class cil_printer () = object (self)
      | [ { skind = Block b } ], [], [], _ -> self#require_braces ctxt b
      | [ { skind = UnspecifiedSequence s } ], [], [], _ ->
        self#require_braces ctxt (Cil.block_from_unspecified_sequence s)
+     | [s],[],[], (Then_with_else | Other)
+       when (not is_ghost) && s.ghost -> true
      | [_],[],[], Then_with_else -> self#block_has_dangling_else blk
      | [ _ ], [], [], _ -> false
      | [],[],[],_ -> false)
diff --git a/tests/pretty_printing/oracle/ghost_else.res.oracle b/tests/pretty_printing/oracle/ghost_else.res.oracle
index 300e658bdf46af2640b353022d29782bf9dbfb50..664d11027eb5cecfeabfce439b5daad31d1ef2fe 100644
--- a/tests/pretty_printing/oracle/ghost_else.res.oracle
+++ b/tests/pretty_printing/oracle/ghost_else.res.oracle
@@ -2,13 +2,15 @@
 /* Generated by Frama-C */
 void if_ghost_else_one_line(int x, int y)
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
 void if_ghost_else_block(int x, int y)
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
@@ -26,14 +28,16 @@ void if_ghost_else_multi_line_block(int x, int y)
 void normal_if_ghost_else_intricated(int x, int y)
 {
   if (x) 
-    if (x) x ++; /*@ ghost else y ++;*/
+    if (x) x ++;
+    /*@ ghost else y ++;*/
   return;
 }
 
 void ghost_else_plus_else_association(int x, int y)
 {
   if (x) {
-    if (x) x ++; /*@ ghost else y --;*/
+    if (x) x ++;
+    /*@ ghost else y --;*/
   }
   else x ++;
   return;
@@ -45,23 +49,25 @@ void ghost_else_plus_else_association(int x, int y)
 [kernel] tests/pretty_printing/ghost_else.i:1: Warning: 
   dropping duplicate def'n of func if_ghost_else_one_line at tests/pretty_printing/ghost_else.i:1 in favor of that at tests/pretty_printing/result/ghost_else.c:2
 [kernel] tests/pretty_printing/ghost_else.i:7: Warning: 
-  dropping duplicate def'n of func if_ghost_else_block at tests/pretty_printing/ghost_else.i:7 in favor of that at tests/pretty_printing/result/ghost_else.c:8
+  dropping duplicate def'n of func if_ghost_else_block at tests/pretty_printing/ghost_else.i:7 in favor of that at tests/pretty_printing/result/ghost_else.c:9
 [kernel] tests/pretty_printing/ghost_else.i:15: Warning: 
-  dropping duplicate def'n of func if_ghost_else_multi_line_block at tests/pretty_printing/ghost_else.i:15 in favor of that at tests/pretty_printing/result/ghost_else.c:14
+  dropping duplicate def'n of func if_ghost_else_multi_line_block at tests/pretty_printing/ghost_else.i:15 in favor of that at tests/pretty_printing/result/ghost_else.c:16
 [kernel] tests/pretty_printing/ghost_else.i:25: Warning: 
-  dropping duplicate def'n of func normal_if_ghost_else_intricated at tests/pretty_printing/ghost_else.i:25 in favor of that at tests/pretty_printing/result/ghost_else.c:25
+  dropping duplicate def'n of func normal_if_ghost_else_intricated at tests/pretty_printing/ghost_else.i:25 in favor of that at tests/pretty_printing/result/ghost_else.c:27
 [kernel] tests/pretty_printing/ghost_else.i:32: Warning: 
-  dropping duplicate def'n of func ghost_else_plus_else_association at tests/pretty_printing/ghost_else.i:32 in favor of that at tests/pretty_printing/result/ghost_else.c:32
+  dropping duplicate def'n of func ghost_else_plus_else_association at tests/pretty_printing/ghost_else.i:32 in favor of that at tests/pretty_printing/result/ghost_else.c:35
 /* Generated by Frama-C */
 void if_ghost_else_one_line(int x, int y)
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
 void if_ghost_else_block(int x, int y)
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
@@ -79,14 +85,16 @@ void if_ghost_else_multi_line_block(int x, int y)
 void normal_if_ghost_else_intricated(int x, int y)
 {
   if (x) 
-    if (x) x ++; /*@ ghost else y ++;*/
+    if (x) x ++;
+    /*@ ghost else y ++;*/
   return;
 }
 
 void ghost_else_plus_else_association(int x, int y)
 {
   if (x) {
-    if (x) x ++; /*@ ghost else y --;*/
+    if (x) x ++;
+    /*@ ghost else y --;*/
   }
   else x ++;
   return;
diff --git a/tests/syntax/ghost-else.i b/tests/syntax/ghost-else.i
index ba81f8b497b4a4aad5a4f0b68a4fc1cd066eb945..fa371c6a587d8ab638df06a293770ec7104c2bbb 100644
--- a/tests/syntax/ghost-else.i
+++ b/tests/syntax/ghost-else.i
@@ -91,4 +91,11 @@ void ghost_else_plus_else_association(int x) /*@ ghost(int y)*/ {
     if (x) x++ ;
     //@ ghost else y-- ;
   } else x ++ ;
-}
\ No newline at end of file
+}
+
+void non_ghost_if_with_ghost_body(int x)  /*@ ghost(int y)*/ {
+  // pretty-printer must take care of keeping the braces around the
+  // single-(ghost)-statement blocks. Otherwise, the code is syntactically
+  // invalid (empty, from a non-ghost point-of-view, then clause)
+  if (x) { /*@ ghost y++; */ } else { /*@ ghost y--; */ }
+}
diff --git a/tests/syntax/oracle/ghost-else.res.oracle b/tests/syntax/oracle/ghost-else.res.oracle
index 27c6a24e457243d20f4f72272d5c618258286b92..870a783d7d4771730c8852960ace204e950fc49a 100644
--- a/tests/syntax/oracle/ghost-else.res.oracle
+++ b/tests/syntax/oracle/ghost-else.res.oracle
@@ -24,19 +24,22 @@ void normal_if_else_intricated(int x, int y)
 
 void if_ghost_else_one_line(int x) /*@ ghost (int y) */
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
 void if_ghost_else_one_line_escaped(int x) /*@ ghost (int y) */
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
 void if_ghost_else_block(int x) /*@ ghost (int y) */
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   return;
 }
 
@@ -53,7 +56,8 @@ void if_ghost_else_multi_line_block(int x) /*@ ghost (int y) */
 
 void if_ghost_else_block_comments(int x) /*@ ghost (int y) */
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   /* // comment 1 */
   /* // comment 2 */
   return;
@@ -61,7 +65,8 @@ void if_ghost_else_block_comments(int x) /*@ ghost (int y) */
 
 void if_ghost_else_block_comments_escaped(int x) /*@ ghost (int y) */
 {
-  if (x) x ++; /*@ ghost else y ++;*/
+  if (x) x ++;
+  /*@ ghost else y ++;*/
   /* // comment 1\ */
   /* continued */
   return;
@@ -70,7 +75,8 @@ void if_ghost_else_block_comments_escaped(int x) /*@ ghost (int y) */
 void normal_if_ghost_else_intricated(int x) /*@ ghost (int y) */
 {
   if (x) 
-    if (x) x ++; /*@ ghost else y ++;*/
+    if (x) x ++;
+    /*@ ghost else y ++;*/
   return;
 }
 
@@ -79,10 +85,25 @@ void normal_if_ghost_else_intricated(int x) /*@ ghost (int y) */
 void ghost_else_plus_else_association(int x) /*@ ghost (int y) */
 {
   if (x) {
-    if (x) x ++; /*@ ghost else y --;*/
+    if (x) x ++;
+    /*@ ghost else y --;*/
   }
   else x ++;
   return;
 }
 
+/*  pretty-printer must take care of keeping the braces around the */
+/*  single-(ghost)-statement blocks. Otherwise, the code is syntactically */
+/*  invalid (empty, from a non-ghost point-of-view, then clause) */
+void non_ghost_if_with_ghost_body(int x) /*@ ghost (int y) */
+{
+  if (x) {
+    /*@ ghost y ++; */
+  }
+  else {
+    /*@ ghost y --; */
+  }
+  return;
+}
+