diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index 68b823a9620d1d164fc550f247817bdc95a653c3..e9a4cddb44f29c39e12dd5f67688af40dde25608 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -2,12 +2,22 @@
 [kernel] Parsing issue11.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal ZN1a1bIcEEC1v_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN1a1bIcEEC1v_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] [Valid] Goal ZN1a1bIvEEC1v_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN1a1bIvEEC1v_terminates (Cfg) (Trivial)
+[wp] 6 goals scheduled
+[wp] [Valid] typed_fc_init_ZN1aE1c_terminates (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1c_exits (Qed)
 [wp] [Valid] typed___fc_init_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1d_terminates (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1d_exits (Qed)
 [wp] [Valid] typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires (Qed)
-[wp] Proved goals:    2 / 2
-  Qed:             2
+[wp] Proved goals:   10 / 10
+  Terminating:     2
+  Unreachable:     2
+  Qed:             6
 /* Generated by Frama-C */
 struct _frama_c_vmt_content {
    void (*method_ptr)() ;
@@ -40,7 +50,9 @@ void b<void>::Ctor(struct b<void> const *this);
 
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-/*@ requires \valid_read(this); */
+/*@ requires \valid_read(this);
+    terminates \true;
+    exits \false; */
 void b<void>::Ctor(struct b<void> const *this)
 {
   return;
@@ -55,7 +67,9 @@ void b<char>::Ctor(struct b<char> const *this);
 
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
-/*@ requires \valid_read(this); */
+/*@ requires \valid_read(this);
+    terminates \true;
+    exits \false; */
 void b<char>::Ctor(struct b<char> const *this)
 {
   return;
@@ -67,6 +81,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
 struct b<void> c;
+/*@ terminates \true;
+    exits \false; */
 void __fc_init_ZN1aE1c(void) __attribute__((__constructor__));
 void __fc_init_ZN1aE1c(void)
 {
@@ -75,6 +91,8 @@ void __fc_init_ZN1aE1c(void)
 }
 
 struct b<char> d;
+/*@ terminates \true;
+    exits \false; */
 void __fc_init_ZN1aE1d(void) __attribute__((__constructor__));
 void __fc_init_ZN1aE1d(void)
 {
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index 7381b557996c3042203efaf4bdb952972aa00659..633ff61626d298c5b51c2df4f1b940ff94268364 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -2,11 +2,15 @@
 [kernel] Parsing issue23.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Valid] typed_Z1m_assert (Qed)
 [wp] [Valid] typed_Z1m_assert_2 (Qed)
-[wp] Proved goals:    2 / 2
+[wp] Proved goals:    4 / 4
+  Terminating:     1
+  Unreachable:     1
   Qed:             2
 /* Generated by Frama-C */
 struct _frama_c_vmt_content {
@@ -40,6 +44,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
 int i;
+/*@ terminates \true;
+    exits \false; */
 void m(void)
 {
   i = 0;
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index c3f8560f52d5e394626b6290186c4cbcf9266a54..b8936432fae66c27b4e5730206ec5f65e10573f5 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -2,6 +2,8 @@
 [kernel] Parsing issue24.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
 [wp] [Valid] typed_Z1m_assert (Alt-Ergo) (Cached)
@@ -10,7 +12,9 @@ Now output intermediate result
 [wp] [Valid] typed_Z1m_assert_4 (Qed)
 [wp] [Valid] typed_Z1m_assert_5 (Qed)
 [wp] [Valid] typed_Z1m_assert_6 (Alt-Ergo) (Cached)
-[wp] Proved goals:    6 / 6
+[wp] Proved goals:    8 / 8
+  Terminating:     1
+  Unreachable:     1
   Qed:             2
   Alt-Ergo:        4
 /* Generated by Frama-C */
@@ -20,6 +24,8 @@ static int i;
 /*@ predicate pos(ℤ k) = k < 0;
  */
 int i;
+/*@ terminates \true;
+    exits \false; */
 void m(void)
 {
   i = 0;
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index cb4176455a42e11acc1ce062ee139015e6c5b8e0..19db67896227fc5dd6a9c7fa41a4b9bba5b04840 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -3,17 +3,26 @@
 Now output intermediate result
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] [Valid] Goal Z3posi_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3posi_terminates (Cfg) (Trivial)
+[wp] 4 goals scheduled
 [wp] [Valid] typed_Z3posi_ensures (Alt-Ergo) (Trivial)
 [wp] [Valid] typed_Z3posi_ensures_2 (Alt-Ergo) (Cached)
-[wp] Proved goals:    2 / 2
+[wp] [Valid] typed_Z1mi_terminates (Qed)
+[wp] [Valid] typed_Z1mi_exits (Qed)
+[wp] Proved goals:    6 / 6
+  Terminating:     1
+  Unreachable:     1
+  Qed:             2
   Alt-Ergo:        2
 /* Generated by Frama-C */
 /*@ predicate positive(int i) = i > 0;
  */
 /*@ logic _Bool p(int i) = (_Bool)(i > 0? 1: 0);
  */
-/*@ ensures \result ≢ 0 ⇔ positive(\old(k));
+/*@ terminates \true;
+    exits \false;
+    ensures \result ≢ 0 ⇔ positive(\old(k));
     ensures \result ≡ p(\old(k));
  */
 _Bool pos(int k)
@@ -23,6 +32,8 @@ _Bool pos(int k)
   return __retres;
 }
 
+/*@ terminates \true;
+    exits \false; */
 _Bool m(int k)
 {
   _Bool tmp;
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 7e3a1a6cd9167edc2039f6e0ae9017985ae2aaba..2dbd52537448cb3748da846027b15449a9119de6 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -2,11 +2,17 @@
 [kernel] Parsing logiccast.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1mPv_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1mPv_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
+[wp] [Valid] Goal Z1nPc_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1nPc_terminates (Cfg) (Trivial)
 [wp] 2 goals scheduled
 [wp] [Unsuccess] typed_Z1mPv_assert (Alt-Ergo) (Cached)
 [wp] [Unsuccess] typed_Z1nPc_assert (Alt-Ergo) (Cached)
-[wp] Proved goals:    0 / 2
+[wp] Proved goals:    4 / 6
+  Terminating:     2
+  Unreachable:     2
   Unsuccess:       2
 [wp] logiccast.cpp:3: Warning: 
   Memory model hypotheses for function '_Z1mPv':
@@ -20,12 +26,16 @@ Now output intermediate result
   void _Z1nPc(char *r);
 /* Generated by Frama-C */
 char *base;
+/*@ terminates \true;
+    exits \false; */
 void m(void *r)
 {
   /*@ assert \subset(r, (void *)(base + (0 .. 1))); */ ;
   return;
 }
 
+/*@ terminates \true;
+    exits \false; */
 void n(char *r)
 {
   /*@ assert \subset(r, (char *)((void *)(base + (0 .. 1)))); */ ;
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index f5ad26c07a95726d92c91e869c6a8ff69ded65e7..8168060de213053ea08cd183d469b5535946cbec 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -2,21 +2,32 @@
 [kernel] Parsing term.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z2m1_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m1_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
-[wp] [CFG] Goal Z2m2_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z2m3_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z2m4_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z3m3a_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z3m3b_terminates : Valid (Trivial)
+[wp] [Valid] Goal Z2m2_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m2_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z2m3_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m3_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z2m4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m4_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z3m3a_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3m3a_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z3m3b_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3m3b_terminates (Cfg) (Trivial)
 [wp] 3 goals scheduled
 [wp] [Valid] typed_Z2m2_ensures (Qed)
 [wp] [Valid] typed_Z2m3_c_ensures (Qed)
 [wp] [Valid] typed_Z3m3a_c_ensures (Qed)
-[wp] Proved goals:    8 / 8
-  Terminating:     5
+[wp] Proved goals:   15 / 15
+  Terminating:     6
+  Unreachable:     6
   Qed:             3
 /* Generated by Frama-C */
-/*@ behavior c:
+/*@ terminates \true;
+    exits \false;
+    
+    behavior c:
       requires \true; */
 void m1(void)
 {
@@ -25,6 +36,7 @@ void m1(void)
 
 /*@ requires \true;
     terminates \true;
+    exits \false;
     ensures \true; */
 void m2(void)
 {
@@ -32,10 +44,12 @@ void m2(void)
 }
 
 /*@ terminates \true;
+    exits \false;
     
     behavior c:
       requires \true;
-      ensures \true; */
+      ensures \true;
+ */
 void m3(void)
 {
   return;
@@ -43,6 +57,7 @@ void m3(void)
 
 /*@ requires \true;
     terminates \true;
+    exits \false;
     
     behavior c:
       requires \true;
@@ -53,13 +68,15 @@ void m3a(void)
   return;
 }
 
-/*@ terminates \true; */
+/*@ terminates \true;
+    exits \false; */
 void m3b(void)
 {
   return;
 }
 
-/*@ terminates \true; */
+/*@ terminates \true;
+    exits \false; */
 void m4(void)
 {
   return;
diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle
index def23f83aafb2982954c20fb79bc6361be10b232..26550523a5a9938963a7b816101071cca4773ede 100644
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -2,13 +2,19 @@
 [kernel] Parsing expand.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals:    1 / 1
+[wp] Proved goals:    3 / 3
+  Terminating:     1
+  Unreachable:     1
   Qed:             1
 /* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+    exits \false;
+    ensures 45 + 1 ≡ 46; */
 void m(void)
 {
   return;
diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle
index 0cec7aa5a250fd3ac8d10c67a44d59faaa7c6596..e54ea3b07bdce2643dbd4021d9fa874d627addc9 100644
--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -2,13 +2,19 @@
 [kernel] Parsing expandf.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals:    1 / 1
+[wp] Proved goals:    3 / 3
+  Terminating:     1
+  Unreachable:     1
   Qed:             1
 /* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+    exits \false;
+    ensures 45 + 1 ≡ 46; */
 void m(void)
 {
   return;
diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle
index d372c195005060a4362ee694278745d513603512..8aca2fdc69e0d1358eaefa4a736c23ba744463b6 100644
--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -2,13 +2,19 @@
 [kernel] Parsing simple.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals:    1 / 1
+[wp] Proved goals:    3 / 3
+  Terminating:     1
+  Unreachable:     1
   Qed:             1
 /* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+    exits \false;
+    ensures 45 + 1 ≡ 46; */
 void m(void)
 {
   return;
diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle
index d8f050089071e8c54c87d47ed875a88a7ca4f5ca..566204222f315e803f1bbc5fccb2fcc55c508eab 100644
--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -2,13 +2,19 @@
 [kernel] Parsing z.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals:    1 / 1
+[wp] Proved goals:    3 / 3
+  Terminating:     1
+  Unreachable:     1
   Qed:             1
 /* Generated by Frama-C */
-/*@ ensures ∀ ℤ n; n > 0 ∨ n ≤ 0; */
+/*@ terminates \true;
+    exits \false;
+    ensures ∀ ℤ n; n > 0 ∨ n ≤ 0; */
 void m(void)
 {
   return;
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index c4a06f37282c2ef3d9590556a38d0bb10a931b3e..40b79e2c4d8559dca44ad342048c62cd7fb39a57 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -2,9 +2,13 @@
 [kernel] Parsing wp_empty_struct.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
+[wp] [Valid] Goal ZN6Point2E3foo_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN6Point2E3foo_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
 [wp] [Valid] typed_ZN6Point2E3foo_ensures (Qed)
 [wp] [Valid] typed_ZN6Point2E3foo_ensures_2 (Qed)
-[wp] Proved goals:    2 / 2
+[wp] Proved goals:    4 / 4
+  Terminating:     1
+  Unreachable:     1
   Qed:             2