diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 07864bf4047d9d9aab541a8e342d3f2685f0bec7..2652369061c2fa5e3363456d7454a7b849bf3f65 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -9,6 +9,7 @@
 - memory profiling
 - [Guillaume] ajouter les annotations de RTE dans la table des annotations
   	      (avec une option)
+- [David Mentré] tset
 
 #####################
 # E-ACSL CONSTRUCTS #
@@ -21,6 +22,7 @@
 - loop variant
 - logical shift (at least in non GMP mode)
 - let-in
+- tset
 - grep "not_yet" *.ml
 
 ########
@@ -69,7 +71,6 @@
   (voir aussi result.i et ./at_stmt_contract.i)
 - interprétation des tableaux logiques
 [Dillon] Windows
-[Guillaume] look like some loop invariants are tagged as "assertion"
 
 [to be check]: no call to full_init or initialize for the assigned result of a 
 function call
@@ -87,5 +88,4 @@ function call
 - inclure exemple du E-ACSL Reference Manual
 - inclure exemple du E-ACSL User Manual
 - inclure exemple du E-ACSL Tutorial
-- test arith.i: mettre les exemples du ACSL manual about div and modulo
-- currently, tests require a non-free version of Frama-C
+- currently, tests require a non-free version of Frama-C (built-ins Value)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 58de08d9fac1de1be8ddf7d5d6e4ba8606d470eb..a9f8c6c57e0e03ab5ea286b10d02dc5aa4f8cf90 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2013/09/25] Some loop invariants were tagged as "assertions".
+
 ###################################
 Plugin E-ACSL 0.3 Fluorine_20130601
 ###################################
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 68fd01bf680a7b389a222f3727819abdf0e005d5..decfc08b779d8902aec46aabe95d8c35b88d1e6c 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -68,6 +68,7 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
 	Misc.mk_block prj last blk :: stmts, env, invariants != []
       | s :: tl -> handle_invariants (s :: stmts, env, false) tl
     in
+    let env = Env.set_annotation_kind env Misc.Invariant in
     let stmts, env, has_loop = handle_invariants ([], env, false) stmts in
     let new_blk = { blk with bstmts = List.rev stmts } in
     { stmt with skind = Loop([], new_blk, loc, cont, break) },