diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 79ef3606a8df5c44eee878b24e8964cdb946bf67..f2adbc17b9bf232bc8f4612baf2c1a092af9ffa4 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -252,7 +252,6 @@ module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
         let lfun = Lang.generated_f ~sort:Logic.Sprop "EqArray%s_%s"
             (Matrix.id ds) (Matrix.natural_id te)
         in
-        let cluster = Definitions.matrix te in
         let denv = Matrix.denv ds in
         let tau = Matrix.tau te ds in
         let xa = Lang.freshvar ~basename:"T" tau in
@@ -269,7 +268,7 @@ module EQARRAYDEF = WpContext.StaticGenerator(Matrix.NATURAL)
           d_lfun = lfun ; d_types = 0 ;
           d_params = denv.size_var @ [xa ; xb ] ;
           d_definition = Predicate(Def,definition) ;
-          d_cluster = cluster ;
+          d_cluster = Definitions.dummy () ;
         }
     end)
 
@@ -281,7 +280,9 @@ module EQARRAY = WpContext.Generator(Matrix.NATURAL)
       type data = Lang.lfun
       let compile mtx =
         let def = EQARRAYDEF.get mtx in
-        Definitions.define_symbol def ; def.d_lfun
+        let d_cluster = Definitions.matrix (fst mtx) in
+        Definitions.define_symbol { def with d_cluster } ;
+        def.d_lfun
     end)
 
 (* -------------------------------------------------------------------------- *)
@@ -310,7 +311,7 @@ module EQCOMPDEF = WpContext.StaticGenerator(Cil_datatype.Compinfo)
         Lang.F.set_builtin lfun reduce_eqcomp ;
         {
           d_lfun = lfun ; d_types = 0 ; d_params = [xa;xb] ;
-          d_cluster = Definitions.compinfo c ;
+          d_cluster = Definitions.dummy () ;
           d_definition = Predicate(Def,def) ;
         }
     end)
@@ -322,7 +323,9 @@ module EQCOMP = WpContext.Generator(Cil_datatype.Compinfo)
       type data = Lang.lfun
       let compile ci =
         let def = EQCOMPDEF.get ci in
-        Definitions.define_symbol def ; def.d_lfun
+        let d_cluster = Definitions.compinfo ci in
+        Definitions.define_symbol { def with d_cluster } ;
+        def.d_lfun
     end)
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 21bb43939f9f3637cb32e3df765b4883c68c8699..30f0dbaf27fde8a3358e4f3825b212b11c76a081 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -212,6 +212,8 @@ let newcluster ~id ?title ?position () =
 let cluster ~id ?title ?position () =
   Cluster.memoize (fun id -> newcluster ~id ?title ?position ()) id
 
+let dummy () = cluster ~id:"dummy" ()
+
 let axiomatic ax =
   Cluster.memoize
     (fun id ->
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 5814a70c95253ca932c96e25f4a68d1e9a0b8a81..cd93d34343df962a901f7601a04525c82e3f94b6 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -28,6 +28,7 @@ open Lang.F
 
 type cluster
 
+val dummy : unit -> cluster
 val cluster : id:string -> ?title:string -> ?position:Filepath.position -> unit -> cluster
 val axiomatic : axiomatic -> cluster
 val section : logic_section -> cluster
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 7fdb796cf1c772e5b4b818c8a647fa0f08403f37..f088afb4eb9c9cb216adb6893e14c88295dcab83 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -540,8 +540,6 @@ let cluster_globals () =
 let cluster_memory () =
   Definitions.cluster ~id:"Compound" ~title:"Memory Compound Updates" ()
 
-let cluster_dummy () = Definitions.cluster ~id:"dummy" ()
-
 module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
     (struct
       let name = "MemTyped.ShiftFieldDef"
@@ -563,7 +561,7 @@ module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
           d_lfun = lfun ; d_types = 0 ;
           d_params = [xloc] ;
           d_definition = dfun ;
-          d_cluster = cluster_dummy () ;
+          d_cluster = Definitions.dummy () ;
         }
 
       let compile = Lang.local generate
@@ -627,7 +625,7 @@ module ShiftGen = WpContext.StaticGenerator(Cobj)
           d_lfun = shift ; d_types = 0 ;
           d_params = [xloc;xk] ;
           d_definition = dfun ;
-          d_cluster = cluster_dummy () ;
+          d_cluster = Definitions.dummy () ;
         }
 
       let compile = Lang.local generate