diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index eafe23bd7bae4684b87673ef80e6e94e983cdde6..38a8abc359dc4023ec95d78fb48c98b094949e76 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -85,7 +85,11 @@ let t_range e a b ~upper ~lower ~range s =
   ]
 
 let t_replace ?(equal="equal") ~src ~tgt (pi : Tactical.process) s =
-  let s' = Conditions.subst (fun e -> if e == src then tgt else e) s in
+  let s' =
+    Conditions.subst
+      (fun e -> if e == src then tgt else raise Not_found)
+      s
+  in
   (equal , (fst s, p_equal src tgt)) :: (pi s')
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 583d3289c0a2e73140884f09cb795ecc8d01394e..8f109852696f530dd785c9876ae28e309da228f4 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -134,6 +134,7 @@ val subst : (term -> term) -> sequent -> sequent
     Function [f] should only transform the head of the predicate, and can assume
     its sub-terms have been already substituted. The atomic substitution is also applied
     to predicates.
+    [f] should raise [Not_found] on terms that must not be replaced
 *)
 
 val introduction : sequent -> sequent option
diff --git a/src/plugins/wp/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index 381d65d4b6c19362fd87c6d9543e78724cacde37..1585f91ab78a7b821baa21c4ac1932603119a708 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -48,7 +48,7 @@ class overflow =
                 "In-Range", (hs , cond) ;
                 "No-Overflow" ,
                 Conditions.subst
-                  (fun u -> if u == e then v else u)
+                  (fun u -> if u == e then v else raise Not_found)
                   (hs , F.p_imply cond g)
               ])
       | _ -> Not_applicable
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 8bfb88d4f40c115f861e642236f18c71dec6a6c4..f61c15b6cb05d322f453a262ffa999e2224c347a 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -366,7 +366,7 @@ let rewrite ?at patterns sequent =
     (fun (descr,guard,src,tgt) ->
        let sequent =
          Conditions.subst
-           (fun e -> if e == src then tgt else e)
+           (fun e -> if e == src then tgt else raise Not_found)
            sequent in
        let step = Conditions.(step ~descr (When guard)) in
        descr , Conditions.insert ?at step sequent