diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c3e3836b467450ca1a3375244c1d50d5f25a9835..3ed9641b47167708c1ecd365eca05cce53d7f435 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -259,7 +259,16 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
         }
     end)
 
-let get_call_contract = CallContract.get
+let get_call_contract ?smoking kf =
+  let cc = CallContract.get kf in
+  match smoking with
+  | None -> cc
+  | Some s ->
+      let g = smoke kf ~id:"dead_call" ~unreachable:s () in
+      { cc with
+        call_post = g :: cc.call_post ;
+        call_exit = g :: cc.call_exit ;
+      }
 
 (* -------------------------------------------------------------------------- *)
 (* --- Code Assertions                                                    --- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 5a06e3cb6dc42e947991c7207e441f8455cf1d25..9ba615b43056e2600261b51cbb211af869417a0c 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -95,7 +95,7 @@ type call_contract = {
 }
 
 val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
-val get_call_contract : kernel_function -> call_contract
+val get_call_contract : ?smoking:stmt -> kernel_function -> call_contract
 
 (* -------------------------------------------------------------------------- *)
 (* --- Clear Tablesnts                                                    --- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index b9b2658183ef397e7e0c9c056c51a2d0ae7007ca..431b3df41f3c2eab9c205f8e8bebc60b84fdf426 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -294,7 +294,12 @@ struct
         W.use_assigns env.we None (WpPropId.mk_asm_assigns_desc s) w
 
   and call env s r kf es wr : W.t_prop =
-    let c = CfgAnnot.get_call_contract kf in
+    let smoking =
+      if is_default_bhv env.mode &&
+         WpLog.SmokeTests.get () &&
+         WpLog.SmokeDeadcall.get ()
+      then Some s else None in
+    let c = CfgAnnot.get_call_contract ?smoking kf in
     let w_call = W.call env.we s r kf es
         ~pre:c.call_pre
         ~post:c.call_post
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index db7a24fa9c2e464c38476a6b5021ee560798263b..b25934771ab7cd4d7afda9a25199b5f7cc2f2d79 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -657,7 +657,7 @@ let add_called_post called_kf termination_kind acc =
 let add_call_checks config s kf posts exits =
   if cur_fct_default_bhv config
   && Wp_parameters.SmokeTests.get ()
-  && Wp_parameters.SmokeDeadcode.get ()
+  && Wp_parameters.SmokeDeadcall.get ()
   then
     WpStrategy.add_prop_dead_call kf s posts exits
   else