diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index e9b9477243ea904b45bf416c80c619b64a3a8375..e2371df94b2bf5afa62ce0dc71ee146b43d8319a 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -304,7 +304,8 @@ let do_progress goal msg = (* ------------------------------------------------------------------------ *) let do_report_cache_usage mode = - if not (Wp_parameters.has_dkey dkey_shell) && + if !exercised > 0 && + not (Wp_parameters.has_dkey dkey_shell) && not (Wp_parameters.has_dkey VCS.dkey_no_cache_info) then let hits = ProverWhy3.get_hits () in