diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index c56fe8cb7764666de523e6cef164eafccc02934e..804a82b615992073ded5220620d791befb983065 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -16,6 +16,7 @@
 #########
 
 - tester les opérations binaires sur les pointeurs (requiert complex left value)
+- tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745
 - améliorer test "arith.i" quand bug fixed #751
 
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 94504c62f464b06e1548dd40395dd91bb62a9242..d7383514c0d2136af9854164289c45e9494815af 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -473,7 +473,9 @@ let rec named_predicate_to_exp env p =
 (* ************************************************************************** *)
 
 let convert_preconditions _only_behaviors env _funspec behaviors =
-  if behaviors <> [] then not_yet "requires of behaviors";
+  List.iter
+    (fun b -> if b.b_requires <> [] then not_yet "requires of behaviors")
+    behaviors;
   let p = Logic_const.ptrue in
   let e, env = named_predicate_to_exp env p in
   p, e, env