diff --git a/src/plugins/wp/ProverSearch.ml b/src/plugins/wp/ProverSearch.ml
index 0425a46e766851c56686890a6ede10ad8f6c9eeb..85abe2d171a6276f6f6ab54d16b4d430fd557b75 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 ;