From 32e5d4417ff263320c411c88f019e246745047b7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 26 Nov 2019 13:06:43 +0100
Subject: [PATCH] [WP] Fixes generation of recursive predicates in Why3
---
src/plugins/wp/ProverWhy3.ml | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 36313df6ce8..bbe2a59b3bd 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -914,9 +914,8 @@ 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_equ
- (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result)
- t)
+ (Why3.Term.t_implies t
+ (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result))
in
let decl =
Why3.Decl.create_prop_decl Why3.Decl.Paxiom
--
GitLab