diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8336ee75a9c1c3d0d3a976549a3bf5ad53b3333d..6a9b2d8ec1a5b9cef6fd6526b9df967f5a1fd4d6 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,7 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
--* E-ACSL       [2014/03/17] Fix bug #1715 about -e-acsl-full-mmodel which
+-* E-ACSL       [2014/03/25] Fix bug #1716 with annotations in while(1).
+-* E-ACSL       [2014/03/25] Fix bug #1715 about -e-acsl-full-mmodel which
 	        generates incorrect code.
 -* E-ACSL       [2014/03/17] Fix bug #1700 about non-ISO empty struct.
 
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 614de29f79a9abd256fdf22329d112fb85461f0c..376ed00d33c05cd9cf7b8255d8e6922d4918dc33 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -599,7 +599,7 @@ end = struct
 	    List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
 	  init_set
       end;
-      D.compute returns
+      D.compute stmts
     with Kernel_function.No_Definition | Kernel_function.No_Statement -> 
       ());
     Options.feedback ~dkey ~level:2 "function %a done."