From d557cd408e084b446f5c2829762f5da1e3badb05 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 1 Oct 2019 15:18:51 +0200
Subject: [PATCH] [wp/cache] fix interrupted provers counted as missed
---
src/plugins/wp/ProverWhy3.ml | 17 ++++++++---------
1 file changed, 8 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 951cb4e249c..c125e1c0cec 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1305,15 +1305,14 @@ let prove ?timeout ?steplimit ~prover wpo =
Task.return result
end
else
- begin
- incr miss ;
- Task.finally
- (call_prover ~timeout ~steplimit drv prover config task)
- (function
- | Task.Result result when VCS.is_verdict result ->
- set_cache_result ~mode hash prover result
- | _ -> ())
- end
+ Task.finally
+ (call_prover ~timeout ~steplimit drv prover config task)
+ begin function
+ | Task.Result result when VCS.is_verdict result ->
+ incr miss ;
+ set_cache_result ~mode hash prover result
+ | _ -> ()
+ end
end ()
with exn ->
let bt = Printexc.get_raw_backtrace () in
--
GitLab