diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index f7b0628225193fc8fb2837dfe0d1925ce94a7423..7a88530125422d7b9bd618f1e9c4b2b762d4442d 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -26,7 +26,7 @@
 
 type map = Memory.map
 type node = Memory.node
-let map kf = (Code.domain kf).map
+let map kf = (Analysis.get kf).map
 let id n = Memory.id n
 let uid m n = Memory.id @@ Memory.node m n
 let iter = Memory.iter
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index 252bb026bd047bf6ffe9cd1766b8cdb945b007e0..8fd275216e39e9ae08e3a0db8463fb1056fbf4e6 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -56,16 +56,6 @@ let get kf =
     Options.feedback ~ontty:`Transient "Function %a…" Kernel_function.pretty kf ;
     let domain = Code.domain kf in
     STATE.add kf domain ;
-    Options.result "@[<v 2>Function %a:%t@]@."
-      Kernel_function.pretty kf
-      begin fun fmt ->
-        List.iter
-          begin fun r ->
-            Format.pp_print_newline fmt () ;
-            Memory.pp_region fmt r ;
-          end @@
-        Memory.regions domain.map
-      end ;
     domain
 
 let compute kf = ignore @@ get kf
diff --git a/src/plugins/region/register.ml b/src/plugins/region/register.ml
index 54cd5cdd62b1d0f0a2e294a2b7ebce49a6390fca..0d904f9fd3ef8e01ccde1980924a745a6a43e312 100644
--- a/src/plugins/region/register.ml
+++ b/src/plugins/region/register.ml
@@ -31,7 +31,20 @@ let main () =
     begin
       Ast.compute () ;
       R.feedback "Analyzing regions" ;
-      Globals.Functions.iter Analysis.compute ;
+      Globals.Functions.iter
+        begin fun kf ->
+          let domain = Analysis.get kf in
+          Options.result "@[<v 2>Function %a:%t@]@."
+            Kernel_function.pretty kf
+            begin fun fmt ->
+              List.iter
+                begin fun r ->
+                  Format.pp_print_newline fmt () ;
+                  Memory.pp_region fmt r ;
+                end @@
+              Memory.regions domain.map
+            end
+        end
     end
 
 let () = Boot.Main.extend main
diff --git a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
index 6fd76bcdc0e6a7dd48f86711e51fd725a837ed8b..1c937abfbab7553150f053b3fe205b6a7e57d7d8 100644
--- a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
@@ -6,366 +6,6 @@
 [wp] Warning: Missing RTE guards
 [region] array.c:23: Warning: Annotations not analyzed
 [region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function add_first4
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
index b50ed95f5a1a3c59a90f9d702859bcf76e3f60d6..75bce10e9805bbf6ad133de1cd99b97755d66e1d 100644
--- a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
@@ -7,294 +7,6 @@
 [region] copy_array.c:15: Warning: Annotations not analyzed
 [region] copy_array.c:18: Warning: Annotations not analyzed
 [region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function copy
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
index f7b3f9e10a0a8fe3c6adcd6578592bb6f035ea1d..a6a8f41e11a888e1a6f98cda200b495d786522d4 100644
--- a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
@@ -5,50 +5,6 @@
 [wp] [Valid] Goal g_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function g
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
index 7ba53f1df822f74da95fd6bf2ec012b34e5a27c5..721829172e9de5998570491c9e65070ce79fac74 100644
--- a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
@@ -5,113 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function f
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
index 87cfc66c4553a4f000d9bc1999b820d12fe57e7e..7023fcc52f23930b494cefea0d98c9ca702accf0 100644
--- a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
@@ -5,54 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
 ------------------------------------------------------------
   Function f
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
index 132cfb8a7b39546b7fa264271c771caa1c10901a..6162ad43a5af37856e2f4eeea2582d191f330e86 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
@@ -6,366 +6,6 @@
 [wp] Warning: Missing RTE guards
 [region] array.c:23: Warning: Annotations not analyzed
 [region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
-[region] array.c:23: Warning: Annotations not analyzed
-[region] array.c:24: Warning: Annotations not analyzed
 [wp] 6 goals scheduled
 [wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_add_first4_ensures_2 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
index 7071946431da6f0dc59ab0acdafbc1460cc94583..87119772a2ea41da0a911917fa0dd40913588d9c 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
@@ -7,294 +7,6 @@
 [region] copy_array.c:15: Warning: Annotations not analyzed
 [region] copy_array.c:18: Warning: Annotations not analyzed
 [region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
-[region] copy_array.c:15: Warning: Annotations not analyzed
-[region] copy_array.c:18: Warning: Annotations not analyzed
-[region] copy_array.c:19: Warning: Annotations not analyzed
 [wp] 13 goals scheduled
 [wp] [Valid] region_copy_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_copy_loop_invariant_Copy_preserved (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
index 5ef48e91de1c916556cd874542a66ad21d7b6f90..cc19d2134ab95a9f647e807f4b7d9d8d8e377ccf 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
@@ -5,50 +5,6 @@
 [wp] [Valid] Goal g_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
-[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
 [wp] 4 goals scheduled
 [wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
 [wp] [Valid] region_g_assigns_part1 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
index cc8d40d8228b23508cfe3f43612df60f4a679dbc..166e787cf3e5c5feb8bc5d0eaf440e4162ba7ea7 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
@@ -5,113 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
-[region] record.c:22: Warning: Annotations not analyzed
 [wp] 4 goals scheduled
 [wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_f_ensures_2 (Qed)
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
index 40300a0021d5e2fd988683d69c7f78d10cddbbfb..8ac57f31244c3cae6924ce5daae5907e69300be5 100644
--- a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
@@ -5,54 +5,6 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
-[region] union.i:14: Warning: Annotations not analyzed
 [wp] 6 goals scheduled
 [wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] region_f_assert (Alt-Ergo) (Cached)