From 5b7a99c748596a33d19807557a5572dafefa852b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 1 Oct 2019 16:05:27 +0200
Subject: [PATCH] [wp/cache] suppress cache info when no goals
---
src/plugins/wp/register.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e9b9477243e..e2371df94b2 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
--
GitLab