diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
index d86eae1f0ae80672358120aab8f23cd524a72b08..c94252aec4d01860e4d251c73aef16fc06f3b536 100644
--- a/src/kernel_internals/typing/ghost_cfg.ml
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -114,8 +114,8 @@ let alteredCFG stmt =
 let checkGhostCFG bhv withGhostStart noGhost =
   let rec do_check visited withGhostStart noGhostStart =
     match (nextSync withGhostStart), (nextSync noGhostStart) with
-    | Stmt withGhost, Stmt _ when StmtSet.mem withGhost visited -> visited
     | Stmt withGhost, Stmt noGhost ->
+      let is_visited = StmtSet.mem withGhost visited in
       let visited = StmtSet.add withGhost visited in
       let withGhost =
         StmtSet.contains_single_elt (nextNonGhostSync withGhost)
@@ -124,6 +124,9 @@ let checkGhostCFG bhv withGhostStart noGhost =
         | Some s1, s2 when not (Stmt.equal s1 (Get_orig.stmt bhv s2)) ->
           alteredCFG withGhostStart ; visited
 
+        (* Note: this test is deferred so that bad stmts are detected above *)
+        | Some _, _ when is_visited -> visited
+
         | Some ({ skind = If(_) } as withGhost), noGhost ->
           let wgThen, wgElse = Cil.separate_if_succs withGhost in
           let ngThen, ngElse = Cil.separate_if_succs noGhost in
@@ -141,7 +144,7 @@ let checkGhostCFG bhv withGhostStart noGhost =
           let visited = List.fold_left2 do_check visited wgSuccsNG ngSuccs in
           List.fold_left (fun v s -> do_check v s ngDef) visited mustDefault
 
-        | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_, ngb,_,_,_) } ->
+        | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_,ngb,_,_,_) } ->
           begin match wgb.bstmts, ngb.bstmts with
             | s1 :: _ , s2 :: _ -> do_check visited s1 s2
             | _, _ -> visited
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index 002354fe668613773fb9858468a214863d3cf9f6..2ba5406612ead5a7a208606959a58e84b20b0855 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -109,6 +109,16 @@ int ghost_return() {
   return 0;
 }
 
+void shared_cfgs(int x) {
+  switch (x) {
+    /*@ ghost case 3: ; */
+  case 2: ;
+    x = 5;
+  default: ;
+    x ++;
+  }
+}
+
 #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 c4bf9a5dc2d8a56df4f7e89bdaf062b289ecb09c..9b3c7cfa41cc69869fd92a3af17e5eda163c55af 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -26,5 +26,8 @@
   Ghost code breaks CFG starting at:
   /*@ ghost __retres = 1; */
   /*@ ghost goto return_label; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:114: Warning: 
+  Ghost code breaks CFG starting at:
+  /*@ ghost case 3: ; */
 [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 9a2f4f8338f820d8d2f5d506bce7b21b1347d035..3248acc0fd5b4ced82fdee8120ac6ef5ff02068a 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:117: User Error: 
+[kernel] tests/cil/ghost_cfg.c:127: 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.