diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 361a4d227a3ad9c5c93cf969b21fdef5d514e401..09dcee7a0282bc7a76bdb3d3aaaba7f9252dbf51 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -812,7 +812,7 @@ class CLUnfolder(object):
 
         # Syntax analyser and type checker
         # Compile a condition expression to a tree representation
-        tree_prop = compile_cond( ## TODO: AUDIT
+        tree_prop = compile_cond(
             property_text,
             self.dynamic_system.symb_tab,
             self.dynamic_system.report
@@ -1175,6 +1175,9 @@ class CLUnfolder(object):
         .. warning:: vvars (frontier values) are not tested. Thus the satisfiability
             is not tested for interesting variables like in squery_solve().
 
+        .. note:: This function checks and corrects incoherent data on step number.
+            __steps_before_check can't be >= max_step
+
         :param max_step: The horizon on which the properties must be satisfied.
         :type max_step: <int>
         """
@@ -1236,6 +1239,9 @@ class CLUnfolder(object):
 
         Otherwise, 1 test is made for each remaining step after each shift() call.
 
+        .. note:: This function checks and corrects incoherent data on step number.
+            __steps_before_check can't be >= max_step
+
         :param max_step: bounded horizon for computations
         :param max_sol: The maximum number of solutions to be returned
         :param vvars: Variables for which solutions must differ.