diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index ef36ce6af08ad80830385d2fbcf1aa90934b2b5f..52c83f5c4e1185e2c53138d937303359c64509f5 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/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                                                      --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 81f682d62f62315225dc83dd4add8ccca77773a1..33cb4ae786c960a0d0cc42f06e9e58f66ca2293b 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/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 *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index a2696a8832563c29ea0eaa66d3093d42927b3a80..e146dc0edfb113d1094b7eddd70b2c182bee66d0 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/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 =