diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
index 8e07b35953f76a889c06c6b94390006f13565928..fa483caf5e1f82b71799048d7ecb6e59e2c7bd5f 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
@@ -2,6 +2,4 @@
 [aorai] tests/ltl/goto.c:28: Warning: 
   Call to opc does not follow automaton's specification. This path is assumed to be dead
 [kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
-[wp] TMPDIR/aorai_goto_0.i:4: Warning: 
-  Global invariant not handled yet ('inv' ignored)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index db979fdb7c87c7b1d15c858c8fe51e570b729a72..77d25a48b495feda8bf60ec9eef71fb296c9f135 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -3,5 +3,5 @@
   Calling undeclared function call_to_an_undefined_function. Old style K&R code?
 [kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:87: Warning: 
+[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:88: Warning: 
   Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
index c7334dc7d0e47e4f03ab43e11ff87faab1c583af..b2a72a31779165f4a34aca5ff788988fb660c7d9 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,7 +1,3 @@
 [kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_boucle1_0.i:3: Warning: 
-  Global invariant not handled yet ('inv_cpt' ignored)
-[wp] TMPDIR/aorai_test_boucle1_0.i:6: Warning: 
-  Global invariant not handled yet ('inv_status' ignored)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
index 1da39e22bb3f77b68bdfd9a967e3448f141d13e1..1dfdb4fe0cc91d811c1f9b76d1b2b11d90d85161 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,5 +1,3 @@
 [kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_boucle2_0.i:4: Warning: 
-  Global invariant not handled yet ('inv' ignored)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
index 8f6717a1e318e6976e9ba28deca3fd2c64bc2cdd..6ee998ea14501018f34d2a6f2b749459410d8417 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,5 +1,3 @@
 [kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_boucle3_0.i:4: Warning: 
-  Global invariant not handled yet ('inv' ignored)
 [wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
index b5e9aba20ed217ff7340c60ba5f738a388ba80e9..46b7da645df3c9c958063d90af138cc8593450cc 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
@@ -6,5 +6,5 @@
 [kernel] tests/ltl/test_recursion1.c:54: Warning: 
   parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
 [kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
-[wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: Missing RTE guards
+[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
index 9891c035100b93d2c7f9dfda512688613a83d126..5117f1beb1595982d9a50ad4085d9e9a015b9d1e 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards
 [wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
-[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
index 904f906300cd765dbc82900fc04a8f861e28e484..897ba54e409eb74d7a8fbfd3c68f4602f2031897 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
 [kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
+[wp] Warning: Missing RTE guards
 [wp] Warning: No definition for 'string_len' interpreted as reads nothing
 [wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
-[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
index 5e6c56778cf99c15ab7fd72ef63105540588b23c..19b8be5b1139a9a7291e26024e723d5ca014a172 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
@@ -4,6 +4,4 @@
 [aorai] tests/ltl/test_switch2.c:23: Warning: 
   Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
 [kernel] Parsing TMPDIR/aorai_test_switch2_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_switch2_0.i:4: Warning: 
-  Global invariant not handled yet ('inv' ignored)
 [wp] Warning: Missing RTE guards