diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index e22c883010414384126989c604b625b02faefc05..6b87bdf9097cb33885ed36b48eda26c80cbe342e 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -609,9 +609,11 @@ class markReferencedVisitor = object
     | GVarDecl (varinfo, loc)
     | GFunDecl (_,varinfo, loc)
     | GFun ({svar = varinfo}, loc) ->
-      Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
-      Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
-      varinfo.vreferenced <- true;
+      if not (hasAttribute "FC_BUILTIN" varinfo.vattr) then begin
+        Kernel.debug ~dkey "referenced: var/fun %s@." varinfo.vname;
+        Kernel.debug ~source:(fst loc) ~dkey "referenced: fun %s" varinfo.vname;
+        varinfo.vreferenced <- true;
+      end;
       DoChildren
     | GAnnot _ -> DoChildren
     | _ ->
diff --git a/src/plugins/callgraph/options.ml b/src/plugins/callgraph/options.ml
index 0b2871677733ce0e79af69eb121d9819b7749e65..3677c0d6be6f1d7ad76883e747f411741bcc119d 100644
--- a/src/plugins/callgraph/options.ml
+++ b/src/plugins/callgraph/options.ml
@@ -76,8 +76,7 @@ module Function_pointers =
       let option_name = "-cg-function-pointers"
       let help = "when Eva has not been computed, safely over-approximate \
                   callees in presence of function pointers; \
-                  always done when Eva has been previously computed. \
-                  WARNING: this option is unsound"
+                  always done when Eva has been previously computed."
     end)
 
 module Uncalled =
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 1bbd1d8265a90f971c869754a33f6d6ccca4c435..611e7dd2923083ae9ff8789a1f10690fb29a0f6a 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,7 @@
 #   <Prover>: prover
 ###############################################################################
 
+ - Wp          [2019/05/09] Fixes -wp-simplify-is-cint simplifier
  - Wp          [2019/04/26] Now requires -warn-invalid-bool
  - Wp          [2019/04/26] Removed option -wp-bool-range
  - Wp          [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index db97213a0c468ae98b411ac54309ac9ee440f8c3..874efe45760d3ff83e47c462cc606fdae5f2054a 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -815,6 +815,7 @@ let c_int_bounds_ival f  =
 
 let max_reduce_quantifiers = 1000
 
+(** We know that t is a predicate which is the opened body of a forall *)
 let reduce_bound v dom t : term =
   let module Exc = struct
     exception True
@@ -831,8 +832,9 @@ let reduce_bound v dom t : term =
         Ival.fold_int red dom (); raise Exc.True
       with Exc.Unknown i -> i in
     let max_bound = try
-        Ival.fold_int(*_decrease*) red dom (); raise Exc.True
+        Ival.fold_int_decrease red dom (); raise Exc.True
       with Exc.Unknown i -> i in
+    (** we try to reduce the bounds of the domains, when trivially false *)
     let dom_red = Ival.inject_range (Some min_bound) (Some max_bound) in
     if not (Ival.equal dom_red dom) && Ival.is_included dom_red dom
     then t
@@ -929,6 +931,8 @@ let is_cint_simplifier = object (self)
           domain <- Tmap.add tvar !var_domain domain;
           let t = walk ~is_goal t in
           domain <- Tmap.remove tvar domain;
+          (** Bonus: Add additionnal hypothesis in forall when we could deduce
+              better constraint on the variable *)
           let t = if quant = Forall &&
                      is_goal &&
                      Ival.cardinal_is_less_than !var_domain max_reduce_quantifiers
@@ -936,6 +940,7 @@ let is_cint_simplifier = object (self)
             else t in
           e_bind quant var t
       | Fun(g,[a]) ->
+          (** Here we simplifies the cints which are redoundant *)
           begin try
               let ubound = c_int_bounds_ival (is_cint g) in
               let dom = (Tmap.find a domain) in