diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 3ec3b7227a1b0744cae8d2817be3cd31ce299614..dbf2df8ce7a15614a2235f8fd11fea846bf7d5be 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -59,7 +59,8 @@ let library = "cint"
 let make_fun_int op i =
   Lang.extern_f ~library ~result:Logic.Int "%s_%a" op Ctypes.pp_int i
 let make_pred_int op i =
-  Lang.extern_f ~library ~result:Logic.Prop "%s_%a" op Ctypes.pp_int i
+  Lang.extern_f
+    ~library ~result:Logic.Prop ~coloring:true "%s_%a" op Ctypes.pp_int i
 
 (* let fun_int op = Ctypes.imemo (make_fun_int op) *) (* unused for now *)
 (* let pred_int op = Ctypes.imemo (make_pred_int op) *) (* unused for now *)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index d26aee33e7d63313fd60a43d4d65ceaa2d7354db..207ac81a387db1f63c5eff26e6a0e0d47d0d1ad9 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -241,7 +241,7 @@ struct
 
   and is_record c s =
     Definitions.call_pred
-      (Lang.generated_p (C.prefix ^ Lang.comp_id c))
+      (Lang.generated_p ~coloring:true (C.prefix ^ Lang.comp_id c))
       (fun lfun ->
          let basename = if c.cstruct then "S" else "U" in
          let s = Lang.freshvar ~basename (Lang.t_comp c) in
@@ -261,7 +261,7 @@ struct
 
   and is_array elt ds t =
     Definitions.call_pred
-      (Lang.generated_p (array_name elt ds))
+      (Lang.generated_p ~coloring:true (array_name elt ds))
       (fun lfun ->
          let cluster =
            match elt with
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 238250786e76b477634e4d5700ceee7c10bf460a..81aa77b29c469e1cb91c7915c20944925ac0e41d 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -759,7 +759,7 @@ struct
           let frame = logic_frame lt_name [] in
           in_frame frame
             begin fun () ->
-              let lfun = Lang.generated_p ("is_" ^ lt_name) in
+              let lfun = Lang.generated_p ~coloring:true ("is_" ^ lt_name) in
               let tau_lt = Lang.tau_of_ltype (Ltype(lt, [])) in
               Typedefs.update lt (Some lfun) ;
               let term_constraint ltyp =
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index cc27b7e46b1b1fabf531ae155d018ae3b8fce248..2a1f2ec14ab720ecd36bbcfad79c12668358e1c1 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -80,15 +80,15 @@ let p_separated = Lang.extern_fp ~library "separated"
 let p_included = Lang.extern_fp ~library "included"
 let p_eqmem = Lang.extern_fp ~library "eqmem"
 let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
-let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
-let p_linked = Lang.extern_fp ~library "linked" (* allocation-table -> prop *)
-let p_sconst = Lang.extern_fp ~library "sconst" (* int-memory -> prop *)
+let f_region = Lang.extern_f ~coloring:true ~library ~result:L.Int "region" (* base -> region *)
+let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
+let p_linked = Lang.extern_fp ~coloring:true ~library "linked" (* allocation-table -> prop *)
+let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
 let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
 let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
 let f_set_init =
   Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
-let p_cinits = Lang.extern_fp ~library "cinits" (* initializaton-table -> prop *)
+let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits" (* initializaton-table -> prop *)
 let p_is_init_r = Lang.extern_fp ~library "is_init_range"
 let p_monotonic = Lang.extern_fp ~library "monotonic_init"
 
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0eee23062cc8620b7753382fea1758285d8f9bcf..f79ee802cf54e287c0282b3048637d50ca121947 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -987,7 +987,7 @@ module ChunkContent = WpContext.Generator(Chunk)
         let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
         let m = e_var p in
         let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
-        let lfun = Lang.generated_p name in
+        let lfun = Lang.generated_p ~coloring:true name in
         let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
         let is_int = Cint.range k in
         let def = p_forall [l] (is_int (F.e_get m (e_var l))) in