diff --git a/share/libc/assert.h b/share/libc/assert.h
index 26ee575269c86e3c11193f565b7f4376feaab5a4..0c4f0639509be1c43594a2ee2673bc7cab594430 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -29,7 +29,6 @@ __BEGIN_DECLS
 
 /*@
   requires nonnull_c: c != 0;
-  terminates c != 0;
   assigns \nothing;
 */
 extern void __FC_assert(int c, const char* file, int line, const char*expr);
@@ -42,7 +41,7 @@ __POP_FC_STDLIB
 #endif
 
 #undef assert
-#ifdef NDEBUG 
+#ifdef NDEBUG
 #define assert(ignore) ((void)0)
 #else
 #ifndef __FRAMAC__
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8ce7b3829c60d4afb7a416be103cf3f7f2894c5f..5a35c61690f2dd9a0489f8d22cddd5839c938637 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2505,7 +2505,6 @@ void __FC_assert(int c, char const *file, int line, char const *expr);
 extern void Frama_C_show_each_warning();
 
 /*@ requires nonnull_c: c ≢ 0;
-    terminates c ≢ 0;
     assigns \nothing; */
 void __FC_assert(int c, char const *file, int line, char const *expr)
 {