From 7226a1eb58dbdae43273448084ea68193bf5bc3f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 11 Jan 2022 17:12:28 +0100
Subject: [PATCH] [wp] Fix condition lift
---
src/plugins/wp/Conditions.ml | 4 +---
src/plugins/wp/Lang.ml | 3 ++-
src/plugins/wp/Lang.mli | 3 ++-
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 67ca47e2b29..f6bd2c4468f 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -678,10 +678,8 @@ let rec flatten_sequence m = function
(* --- Mapping --- *)
(* -------------------------------------------------------------------------- *)
-let lift f e = F.e_prop (f (F.p_bool e))
-
let rec map_condition f = function
- | State s -> State (Mstate.apply (lift f) s)
+ | State s -> State (Mstate.apply (F.p_lift f) s)
| Have p -> Have (f p)
| Type p -> Type (f p)
| When p -> When (f p)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 8dcfa782c14..a75ac05e65c 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -783,7 +783,8 @@ struct
let e_prop t = t
let p_bools xs = xs
let e_props xs = xs
- let lift f x = f x
+ let e_lift f = f
+ let p_lift f = f
let is_zero e = match QED.repr e with
| Kint z -> Integer.equal z Integer.zero
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index b78d557b1d0..c685aeaaca3 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -356,7 +356,8 @@ sig
val e_prop : pred -> term
val p_bools : term list -> pred list
val e_props : pred list -> term list
- val lift : (term -> term) -> pred -> pred
+ val e_lift : (term -> term) -> pred -> pred
+ val p_lift : (pred -> pred) -> term -> term
val p_not : pred -> pred
val p_and : pred -> pred -> pred
--
GitLab