From 7d7db9ff0bf0e8f4e305e4866a925eaf4b6a56a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 28 Jul 2022 11:23:00 +0200
Subject: [PATCH] [wp] fix console for valid results
---
src/plugins/wp/register.ml | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 0ab24ee3c0a..82763ef243f 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -334,17 +334,19 @@ let do_wpo_success ~shell ~cache goal success =
let smoke = Wpo.is_smoke_test goal in
let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
let cstats = ProofEngine.consolidated goal in
- let proof, target = Wpo.get_proof goal in
+ let success = Wpo.is_passed goal in
begin
global_stats := Stats.add !global_stats gstats ;
if cstats.tactics > 0 then
script_stats := Stats.add !script_stats cstats ;
- if shell || proof <> `Passed then
+ if shell || not success then
do_report_stats ~shell ~cache goal ~smoke cstats ;
- if smoke && proof <> `Passed then
+ if smoke then
begin
- let source = fst (Property.location target) in
- Wp_parameters.warning ~once:true ~source "Failed smoke-test"
+ let proof, target = Wpo.get_proof goal in
+ if proof <> `Passed then
+ let source = fst (Property.location target) in
+ Wp_parameters.warning ~once:true ~source "Failed smoke-test"
end ;
end
--
GitLab