diff --git a/bench/bench b/bench/bench
index 5eb08a0d067de519ad7ffa0455393c91ad62836d..c6a053f0dd38246d1ddbdfd137d4fbad13884dc2 100755
--- a/bench/bench
+++ b/bench/bench
@@ -261,6 +261,7 @@ goods bench/typing/x-good --parse-only
 bads bench/typing/x-good --type-only
 goods bench/programs/good
 goods bench/ce
+goods src/trywhy3/examples "--debug ignore_missing_diverges"
 goods examples/bts
 goods examples/tests
 goods examples/tests-provers
diff --git a/src/mlw/vc.ml b/src/mlw/vc.ml
index 6d01cd73748796d1e044369f4df08272932c0af7..045acf8bfb0461664ca2e6b0ecd57281685c02ce 100644
--- a/src/mlw/vc.ml
+++ b/src/mlw/vc.ml
@@ -32,6 +32,9 @@ let debug_sp = Debug.register_flag "vc_sp"
 let no_eval = Debug.register_flag "vc_no_eval"
   ~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
 
+let debug_ignore_missing_diverges = Debug.register_info_flag "ignore_missing_diverges"
+  ~desc:"Suppress@ warnings@ on@ missing@ diverges"
+
 let case_split = Ident.create_attribute "case_split"
 let add_case t = t_attr_add case_split t
 
@@ -520,6 +523,7 @@ let rec k_expr env lps e res xmap =
   let var_or_proxy = var_or_proxy_case xmap in
   let check_divergence k =
     if eff.eff_oneway && not env.divergent then begin
+      if Debug.test_noflag debug_ignore_missing_diverges then
       Warning.emit ?loc "termination@ of@ this@ expression@ \
         cannot@ be@ proved,@ but@ there@ is@ no@ `diverges'@ \
         clause@ in@ the@ outer@ specification";