[wp] Visit each definition with a fresh set of visited terms

Fixes BTS 2501

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

src/plugins/wp/tests/wp_bts/bts_2501.i

+/* 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);
+*/

src/plugins/wp/tests/wp_bts/oracle/bts_2501.res.oracle

+# 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)
+
+------------------------------------------------------------