[WP] Recursive predicate definition as equivalence

src/plugins/wp/ProverWhy3.ml

@@ -914,7 +914,7 @@ class visitor (ctx:context) c =
                 let t = share cnv Prop (Lang.F.e_prop p) in
                 let t =
                   Why3.Term.t_forall_close vars []
-                    (Why3.Term.t_implies t
+                    (Why3.Term.t_iff t
                        (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result))
                 in
                 let decl =

src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle

@@ -24,7 +24,7 @@
     predicate P_RP int
     
     axiom P_RP_def :
-      forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) -> P_RP i
+      forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
     
     function L_F (i:int) : int = 2 * i