diff --git a/src/plugins/wp/StmtCompiler.ml b/src/plugins/wp/StmtCompiler.ml
index 7d07d794a34e3790ca1f221e29578df3da81d599..53534a42a13286ff11c70e376c627921529e790a 100644
--- a/src/plugins/wp/StmtCompiler.ml
+++ b/src/plugins/wp/StmtCompiler.ml
@@ -29,7 +29,6 @@ sig
 
   module M : Model
 
-
   module Node : sig
     type t
     module Map : Qed.Idxmap.S with type key = t
@@ -43,29 +42,28 @@ sig
   module E : sig
     type t
     val create : M.sigma sequence -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it *)
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val writes : t -> M.domain
     val relocate : M.sigma sequence -> t -> t
-    val get: t -> F.pred
   end
 
-  (** Relocatable predicate *)
-  module P :
-  sig
-    type t
-    val create : M.sigma Node.Map.t -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma Node.Map.t -> t -> t
-    val get: t -> F.pred
-  end
-  
-  (** Relocatable condition *)
   module C :
   sig
     type t
     val create : M.sigma -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it. *)
+    val get : t -> F.pred
+    val reads : t -> M.domain
     val relocate : M.sigma -> t -> t
+  end
+
+  module P :
+  sig
+    type t
+    val create : M.sigma Node.Map.t -> F.pred -> t
     val get: t -> F.pred
+    val reads : t -> M.domain Node.Map.t
+    val relocate : M.sigma Node.Map.t -> t -> t
   end
 
   type cfg
diff --git a/src/plugins/wp/StmtCompiler.mli b/src/plugins/wp/StmtCompiler.mli
index 973b33d11d8c186ec93ce2c7730eef1628dd92b3..2dddde5ca986e5c460ea259d15d4dffdb8511f39 100644
--- a/src/plugins/wp/StmtCompiler.mli
+++ b/src/plugins/wp/StmtCompiler.mli
@@ -73,9 +73,9 @@ sig
   end
 
   type node = Node.t
-                                                  
-  val node : unit -> node
+
   (** fresh node *)
+  val node : unit -> node
 
   (** {2 Relocatable Formulae}
       Can be created once with fresh environment, and used several
@@ -84,31 +84,37 @@ sig
   (** Relocatable set of equations *)
   module E : sig
     type t
-    val create : M.sigma sequence -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it *)
+    val create : M.sigma sequence -> F.pred -> t
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val writes : t -> M.domain
     val relocate : M.sigma sequence -> t -> t
-    val get: t -> F.pred
   end
 
-  (** Relocatable predicate *)
-  module P :
+  (** Relocatable condition *)
+  module C :
   sig
     type t
-    val create : M.sigma Node.Map.t -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma Node.Map.t -> t -> t
-    val get: t -> F.pred
+    val create : M.sigma -> F.pred -> t
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val relocate : M.sigma -> t -> t
   end
 
-
-  (** Relocatable condition *)
-  module C :
+  (** Relocatable predicate *)
+  module P :
   sig
     type t
-    val create : M.sigma -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma -> t -> t
+    val create : M.sigma Node.Map.t -> F.pred -> t
     val get: t -> F.pred
+    val reads : t -> M.domain Node.Map.t
+    val relocate : M.sigma Node.Map.t -> t -> t
   end
 
   type cfg (** Structured collection of traces. *)