diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
index 997a756431859f3f7c0b55c1bbdf6354718dc4e5..13eef5e3004ff3f1a6937f7f69ff58e6f0956cc3 100644
--- a/src/kernel_internals/typing/ghost_cfg.ml
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -29,6 +29,14 @@ module StmtSet = Stmt.Hptset
 
 let error = Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use
 
+
+let annot_attr = "has_annot"
+
+(* For no ghost project, we add an attribute each stmt that has annotations. *)
+let has_annot stmt =
+  Annotations.code_annot stmt <> [] ||
+  Cil.hasAttribute annot_attr stmt.sattr
+
 let noGhostBlock b =
   let noGhostVisitor = object (self)
     inherit genericCilVisitor (refresh (Project.current()))
@@ -44,10 +52,15 @@ let noGhostBlock b =
       end else
         begin match s.skind with
           | Switch(e, block, cases, loc) ->
-            let cases = List.filter (fun s -> not (self#original s).ghost) cases in
+            let cases = List.filter
+              (fun s -> not (self#original s).ghost) cases
+            in
             s.skind <- Switch(e, block, cases, loc) ;
             DoChildren
-          | _ -> DoChildren
+          | _ ->
+            let original = self#original s in
+            s.sattr <- if has_annot original then [AttrAnnot annot_attr] else [] ;
+            DoChildren
         end
 
     method getBehavior () = self#behavior
@@ -62,7 +75,7 @@ type follower =
 let sync stmt =
   match stmt.skind with
   (* We ignore blocks: their successors are their 1st stmt so we visit them *)
-  | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> false
+  | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> has_annot stmt
   | _ -> true
 
 let nextSync stmt =
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index a2faa9ed8c4f40fb1bdb95024bd94b3f39500da0..694c59b9371b5017d9f40c1c03ebc92b02912f33 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -93,6 +93,16 @@ int ghost_goto_ghost(){
   return 0;
 }
 
+void switch_loses_assertion (int c) {
+  //@ ghost int x = 1;
+  switch (c) {
+    case 0: return;
+    //@ ghost case 1: x++; /*@ assert x == 2; */ break;
+    default: /*@ assert x == 1; */ break;
+  }
+  return;
+}
+
 #endif
 
 #ifdef CANT_CHECK
diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle
index 66c3a70366776306887bd37be839d9a1cb9e6eb1..eebfbb855dcededaf30827dd76a62c995e0e0e76 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -19,5 +19,8 @@
 [kernel:ghost:bad-use] tests/cil/ghost_cfg.c:89: Warning: 
   Ghost code breaks CFG starting at:
   /*@ ghost goto X; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning: 
+  Ghost code breaks CFG starting at:
+  case 1: /*@ ghost x ++; */
 [kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle
index 286d75896541aa3b0a9fd374e273cd2323dc2115..0ead348826c41ca25cf5a2651ba6dee46193d46f 100644
--- a/tests/cil/oracle/ghost_cfg.1.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.1.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel] tests/cil/ghost_cfg.c:101: User Error: 
+[kernel] tests/cil/ghost_cfg.c:111: User Error: 
   'goto X;' would jump from normal statement to ghost code
 [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.