add limitation on FreshState

main.ml

@@ -31,6 +31,8 @@ Utilisation :
 
 Limitations théoriques :
   * Il faut pour le moment définir un invariant explicite pour les boulces (Tant que)
+  * Les pré-conditions de boucles utilisent des sous-formules à part
+      (avec des variables « fraiches ») qui ne sont pas impactées par la simplification
 Limitations techniques :
   * Le modèle et les traitements doivent être implémentés « en dur » dans le code
   * La résolution par Clingo peut être très longue pour certaines formules