diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 5a29bdd61665c9025f8aae4b95af27a1f7742de6..94ce3aa7a62774646b8f88d0b4a49e62ff6c60cc 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -323,6 +323,8 @@ sig
   sig
     type t = sigma
     val create : ?pool:pool -> unit -> t
+
+    val cache : sigma -> term cache
     val fresh : t -> tau -> var
     val get : t -> term -> term
     val filter : t -> term -> bool
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index f7e80b8320e3d02adc0ee51763ab508fab8d3f98..c3df0e1d46e8797d09fe245f7d1dac7208033735 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2087,6 +2087,11 @@ struct
       filter = [] ;
     }
 
+    let cache sigma =
+      ref begin
+        match sigma.shared with MAP( m , _ ) -> m | _ -> Tmap.empty
+      end
+
     let fresh sigma t = fresh sigma.pool t
 
     let rec compute e = function
@@ -2124,15 +2129,16 @@ struct
 
   let sigma = Subst.create
 
+  let filter sigma e =
+    Subst.filter sigma e || not (Bvars.is_empty e.bind)
+
   let rec subst sigma alpha e =
-    if Subst.filter sigma e then
-      let mu = cache () in
-      let v = compute mu sigma alpha e in
-      set mu e v ; v
+    if filter sigma e then
+      incache (Subst.cache sigma) sigma alpha e
     else e
 
   and incache mu sigma alpha e =
-    if Subst.filter sigma e then
+    if filter sigma e then
       get mu (compute mu sigma alpha) e
     else e
 
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index b0a2fcc180178a62dd00c03ec456b22f3552068d..21e9a0e9e7177b5478d0caa946f1f8decef8c06e 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -922,8 +922,7 @@ let alpha () =
     match F.repr e with
     | Fvar x -> lookup e x
     | _ -> raise Not_found in
-  F.Subst.add_fun sigma compute ;
-  sigma
+  F.Subst.add_fun sigma compute ; sigma
 
 let subst xs vs =
   let bind w x v = Tmap.add (e_var x) v w in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index fedd25bd69d070f026620ad645d986cc3478cd9c..9516c35ee354ca7d2727f6b5170dd6ffabea065d 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -227,18 +227,13 @@ struct
 
   let safecompute g =
     begin
-      try
-        g.simplified <- true ;
-        let timer = ref 0.0 in
-        Wp_parameters.debug ~dkey "Simplify goal" ;
-        Command.time ~rmax:timer preprocess g ;
-        Wp_parameters.debug ~dkey "Simplification time: %a"
-          Rformat.pp_time !timer ;
-        g.time <- !timer ;
-      with e ->
-        Format.eprintf "PREPROCESS ERROR(%s)@."
-          (Printexc.to_string e) ;
-        assert false
+      g.simplified <- true ;
+      let timer = ref 0.0 in
+      Wp_parameters.debug ~dkey "Simplify goal" ;
+      Command.time ~rmax:timer preprocess g ;
+      Wp_parameters.debug ~dkey "Simplification time: %a"
+        Rformat.pp_time !timer ;
+      g.time <- !timer ;
     end
 
   let compute g =