From 45bb2a9f5cdbc13afb6a998ee54eb751ddc5b890 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 7 Oct 2020 10:23:35 +0200
Subject: [PATCH] [wp] force step indexing before strategies
---
src/plugins/wp/ProverSearch.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/ProverSearch.ml b/src/plugins/wp/ProverSearch.ml
index 0425a46e766..85abe2d171a 100644
--- a/src/plugins/wp/ProverSearch.ml
+++ b/src/plugins/wp/ProverSearch.ml
@@ -89,8 +89,10 @@ let search tree ?anchor ?sequent heuristics =
let anchor = ProofEngine.anchor tree ?node:anchor () in
let sequent =
match sequent with
- | Some s -> s | None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
+ | Some s -> s
+ | None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
let lookup h = try h#search pool#add sequent with Not_found -> () in
+ Conditions.index sequent ;
WpContext.on_context
(ProofEngine.node_context anchor)
(List.iter lookup) heuristics ;
--
GitLab