diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 39d30a060ee2c1f76a8eb410739156fb8b681bb3..207a87b2c820ab47af0b85bd12d531e7dc0749a9 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -215,8 +215,6 @@ let get_terminates_clause kf =
   | None when Kernel_function.is_in_libc kf ->
       if not @@ Wp_parameters.TerminatesFCDeclarations.get ()
       then Assumed Logic_const.pfalse
-      else if not @@ Kernel_function.is_definition kf
-      then Assumed Logic_const.ptrue
       else populate_true ()
   | None when Kernel_function.is_definition kf ->
       if not @@ Wp_parameters.TerminatesDefinitions.get ()
@@ -225,7 +223,7 @@ let get_terminates_clause kf =
   | None ->
       if not @@ Wp_parameters.TerminatesExtDeclarations.get ()
       then Assumed Logic_const.pfalse
-      else Assumed Logic_const.ptrue
+      else populate_true ()
   | Some p ->
       defined p
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index 5a67b6c24f5dec9259e913b62518a064100c9c92..d367e2cc0273a670ded48578681bfd4deca900ad 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -6,14 +6,14 @@
   Missing terminates clause for definition, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
-  Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 
+  Missing terminates clause for declaration, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
-  Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
-  Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning: 
+  Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning: 
+  Missing terminates clause for div, populates 'terminates \true'
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index 027ae6502d5d121d9c893f0f16d0d393469448c0..e6da7db09def2a410052da6763e8aa3f9a3056c6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -6,14 +6,14 @@
   Missing terminates clause for definition, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:32: Warning: 
   Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
-  Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning: 
+  Missing terminates clause for declaration, populates 'terminates \true'
 [wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
-  Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
-  Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning: 
+  Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning: 
+  Missing terminates clause for div, populates 'terminates \true'
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
 [wp] [Qed] Goal typed_call_declaration_terminates : Valid