diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
index 70f61d7719b4a89e725d997324345cb6e509e45c..d0ad66e5c95a02d834c24fbeecd36ba40be2f0bc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
@@ -2,20 +2,20 @@
 [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/terminates_call_options.c:23: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
   Missing terminates clause on call to declaration, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:28: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:29: Warning: 
   Missing terminates clause on call to definition, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
   Missing terminates clause on call to exit, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
   Missing terminates clause on call to div, defaults to \false
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 21) in 'call_declaration':
-Call Effect at line 23
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 22) in 'call_declaration':
+Call Effect at line 24
 Prove: false.
 
 ------------------------------------------------------------
@@ -23,8 +23,8 @@ Prove: false.
   Function call_definition
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 26) in 'call_definition':
-Call Effect at line 28
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 27) in 'call_definition':
+Call Effect at line 29
 Prove: false.
 
 ------------------------------------------------------------
@@ -40,14 +40,14 @@ Prove: true.
   Function libc_call
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (1/2):
-Call Effect at line 37
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call' (1/2):
+Call Effect at line 38
 Prove: false.
 
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (2/2):
-Call Effect at line 38
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call' (2/2):
+Call Effect at line 39
 Prove: false.
 
 ------------------------------------------------------------
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 a48bad2bd1ec50fffd7e1b5332b21d9e572eb331..5a67b6c24f5dec9259e913b62518a064100c9c92 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
@@ -2,23 +2,23 @@
 [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/terminates_call_options.c:19: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:20: Warning: 
   Missing terminates clause for definition, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:31: Warning: 
+[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:23: Warning: 
+[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:32: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+[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:37: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
   Missing terminates clause on call to div, defaults to \true
 ------------------------------------------------------------
   Function call_declaration
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 21) in 'call_declaration':
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 22) in 'call_declaration':
 Prove: true.
 
 ------------------------------------------------------------
@@ -26,7 +26,7 @@ Prove: true.
   Function call_definition
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 26) in 'call_definition':
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 27) in 'call_definition':
 Prove: true.
 
 ------------------------------------------------------------
@@ -42,7 +42,7 @@ Prove: true.
   Function libc_call
 ------------------------------------------------------------
 
-Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call':
+Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call':
 Prove: true.
 
 ------------------------------------------------------------
@@ -51,7 +51,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Termination-condition (generated) in 'no_spec_generates_goal':
-Effect at line 32
+Effect at line 33
 Prove: false.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
index 014de1caf3fb3eba4f97d7292f919a860ae79e6c..61733f7adafd9838864c622d564e1157cc1d6df8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
@@ -2,13 +2,13 @@
 [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/terminates_call_options.c:23: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: 
   Missing terminates clause on call to declaration, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:28: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:29: Warning: 
   Missing terminates clause on call to definition, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: 
   Missing terminates clause on call to exit, defaults to \false
-[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
   Missing terminates clause on call to div, defaults to \false
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
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 780952849c89ce5036da525cc3748a94e866b1cc..027ae6502d5d121d9c893f0f16d0d393469448c0 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
@@ -2,17 +2,17 @@
 [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/terminates_call_options.c:19: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:20: Warning: 
   Missing terminates clause for definition, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:31: Warning: 
+[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:23: Warning: 
+[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:32: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:33: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
+[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:37: Warning: 
+[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: 
   Missing terminates clause on call to div, defaults to \true
 [wp] 5 goals scheduled
 [wp] [Qed] Goal typed_definition_assigns : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
index d26bc0ac61d896cd52c4f37eb2eee76e1e53e3c3..7ccee59bcb13cbc002140807e6e25e6988933708 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
+++ b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c
@@ -9,8 +9,9 @@
 
 #include <stdlib.h>
 
-// -wp-external-declaration-terminates <--- default to FALSE
-// -wp-definition-terminates  <--- default to FALSE
+// -wp-declarations-terminate   <--- default to FALSE
+// -wp-definitions-terminate    <--- default to FALSE
+// -wp-frama-c-stdlib-terminate <--- default to FALSE
 
 //@ assigns \nothing ;
 void declaration(void);