From bf568533d0c293134058da8573bed96b8f0f03d4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 May 2022 16:37:03 +0200
Subject: [PATCH] [wp] fix crash with interactive proof
---
src/plugins/wp/ProverWhy3.ml | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 314769066fb..212fe6f8bab 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1338,10 +1338,9 @@ let prepare ~mode wpo driver task =
end
else None
-let interactive ~mode wpo pconf driver prover task =
+let interactive ~mode wpo pconf ~conf driver prover task =
let time = Wp_parameters.InteractiveTimeout.get () in
let timeout = if time <= 0 then None else Some time in
- let conf = get_why3_conf () in
match prepare ~mode wpo driver task with
| None -> Task.return VCS.unknown
| Some (script, merge) ->
@@ -1392,7 +1391,7 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
Task.return VCS.valid
else
if pconf.interactive then
- interactive ~mode wpo pconf drv prover task
+ interactive ~mode wpo pconf ~conf drv prover task
else
Cache.get_result
~digest:(digest wpo drv)
--
GitLab