diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 4e1f02f1c987c689ab4b6ff8ee2d0bf680f65467..c3e3836b467450ca1a3375244c1d50d5f25a9835 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -305,7 +305,15 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
         }
     end)
 
-let get_code_assertions kf stmt = CodeAssertions.get (kf,stmt)
+let get_code_assertions ?smoking kf stmt =
+  let ca = CodeAssertions.get (kf,stmt) in
+  match smoking with
+  | None -> ca
+  | Some r ->
+      if WpReached.smoking r stmt then
+        let s = smoke kf ~id:"deadcode" ~unreachable:stmt () in
+        { ca with code_verified = s :: ca.code_verified }
+      else ca
 
 (* -------------------------------------------------------------------------- *)
 (* --- Loop Invariants                                                    --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 8ca20ccbf96e797ac33431e51803b08e4c6c8c54..5a06e3cb6dc42e947991c7207e441f8455cf1d25 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -62,7 +62,9 @@ type code_assertions = {
   code_verified: pred_info list ;
 }
 
-val get_code_assertions : kernel_function -> stmt -> code_assertions
+val get_code_assertions :
+  ?smoking:WpReached.reachability ->
+  kernel_function -> stmt -> code_assertions
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Loop Contracts                                --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index fcee261c07430a8d7cdeeae5baed7c4c2ba139c1..b9b2658183ef397e7e0c9c056c51a2d0ae7007ca 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -131,6 +131,7 @@ struct
     props: props;
     body: Cfg.automaton option;
     succ: Cfg.vertex -> Cfg.G.edge list;
+    dead: WpReached.reachability option;
     we: W.t_env;
     wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
     mutable wk: W.t_prop; (* end point *)
@@ -197,7 +198,9 @@ struct
     let kl = Cil.CurrentLoc.get () in
     try
       Cil.CurrentLoc.set (Stmt.loc s) ;
-      let ca = CfgAnnot.get_code_assertions env.mode.kf s in
+      let smoking =
+        if is_default_bhv env.mode then env.dead else None in
+      let ca = CfgAnnot.get_code_assertions ?smoking env.mode.kf s in
       let pi =
         W.label env.we (Some s) (Clabels.stmt s) @@
         List.fold_right (prove_property env) ca.code_verified @@
@@ -370,8 +373,14 @@ struct
     let succ = match body with
       | None -> (fun _ -> [])
       | Some cfg -> Cfg.G.succ_e cfg.graph in
+    let dead =
+      if body <> None &&
+         is_default_bhv mode &&
+         WpLog.SmokeTests.get () &&
+         WpLog.SmokeDeadcall.get ()
+      then Some (WpReached.reachability kf) else None in
     let env = {
-      mode ; props ; body ; succ ;
+      mode ; props ; body ; succ ; dead ;
       we = W.new_env kf ;
       wp = Vhash.create 32 ;
       wk = W.empty ;