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