[wp] limit strategy depth

src/plugins/wp/ProofEngine.ml

@@ -138,6 +138,11 @@ let iteri f tree =
     let k = ref 0 in
     walk (fun node -> f !k node ; incr k) r
 
+let rec depth node =
+  match node.parent with
+  | None -> 0
+  | Some p -> depth p
+
 (* -------------------------------------------------------------------------- *)
 (* --- Consolidating                                                      --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/ProofEngine.mli

@@ -73,6 +73,7 @@ val proved : node -> bool
 val pending : node -> int
 val stats : node -> Stats.stats
 val parent : node -> node option
+val depth : node -> int
 val children : node -> (string * node) list
 val tactical : node -> ProofScript.jtactic option
 val get_strategies : node -> int * Strategy.t array (* current index *)

src/plugins/wp/ProverScript.ml

@@ -374,12 +374,14 @@ and explore_fallback env process a node =
   | Some s -> explore_strategie env process s node
 
 let explore_hint env process node =
-  match ProofEngine.get_hint node with
-  | None -> failed
-  | Some s ->
-    match ProofStrategy.find s with
+  if ProofEngine.depth node > env.Env.depth then failed
+  else
+    match ProofEngine.get_hint node with
     | None -> failed
-    | Some s -> explore_strategie env process s node
+    | Some s ->
+      match ProofStrategy.find s with
+      | None -> failed
+      | Some s -> explore_strategie env process s node
 
 let explore_further env process strategy node =
   let marked =