diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index e20c9582fe1921b7973a4892dde875525275757c..6a55329e78dc75a7ab03e577f4e79e17529a68b3 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -404,12 +404,19 @@ class virtual visitor main =
       | Inductive cases -> List.iter (fun l -> self#vdlemma l) cases
 
     method private vdfun d =
+      let old_terms = terms in
+      terms <- Tset.empty ;
       begin
-        List.iter self#vparam d.d_params ;
-        self#vdefinition d.d_definition ;
-        self#vproperties d.d_definition ;
-        self#on_dfun d ;
-      end
+        try
+          List.iter self#vparam d.d_params ;
+          self#vdefinition d.d_definition ;
+          self#vproperties d.d_definition ;
+          self#on_dfun d ;
+        with e ->
+          terms <- old_terms ;
+          raise e
+      end ;
+      terms <- old_terms
 
     method private vlfun f =
       match Symbol.find f with
diff --git a/src/plugins/wp/tests/wp_bts/bts_2501.i b/src/plugins/wp/tests/wp_bts/bts_2501.i
new file mode 100644
index 0000000000000000000000000000000000000000..442e1d8f59e313e7d59a1a2b1dcc49dba3e0d21f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/bts_2501.i
@@ -0,0 +1,14 @@
+/* run.config
+   OPT:-wp-gen -wp-prover why3
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@
+  logic integer F(integer m) = (m <= 0) ? 0 : F(m) ;
+  logic integer R(integer p) = (p < 0) ? -1 : R(p-1) + F(R(p-1));
+
+  lemma R_1: \forall integer p; R(p) == R(p-1) + F(R(p-1));
+  lemma R_2: \forall integer p; 0 <= R(p);
+*/
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f38cfc4e5fd899a8c35a4e59f8b143d23457487a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/bts_2501.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 2 goals scheduled
+[wp] 2 goals generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma R_1:
+Prove: let x_0 = (L_R (p_0-1)) in (x_0+(L_F x_0))=(L_R p_0)
+
+------------------------------------------------------------
+
+Lemma R_2:
+Assume: 'R_1'
+Prove: 0<=(L_R p_0)
+
+------------------------------------------------------------