diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 30272295f402784cfca682a2b0c3b1fd186c7df2..5530d826bccb14f995d230f11bdcf06ecdb01f9a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,9 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2015/11/06] Fix a crash occuring when using a recent libc
+	        while GMP headers provided by E-ACSL are used.
+
 ########################
 Plugin E-ACSL 0.5 Sodium
 ########################
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 66672aa36b5b8ce9f93849fdc12958d41ce1e9e1..40533cbe9b3965aa8408a8492a59c555bfe90c27 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -341,7 +341,8 @@ if there are memory-related annotations.@]"
     | Before_gmp -> before_memory_model <- Gmp
     | Gmp | Memory_model -> ()
     | After_gmp -> before_memory_model <- Memory_model
-    | Code -> assert false);
+    | Code -> () (* still processing the GMP and memory model headers,
+                    but reading some libc code *));
     Cil.JustCopy
   | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
       when Cil.is_builtin vi ->