diff --git a/src/plugins/wp/tests/wp_plugin/bigarray.c b/src/plugins/wp/tests/wp_plugin/bigarray.c
index 266998147bf6ffcc0b21ef49a1156e15ee7ee01a..05b9c3f9bcee56ec9cede170f26dbd0f19b23898 100644
--- a/src/plugins/wp/tests/wp_plugin/bigarray.c
+++ b/src/plugins/wp/tests/wp_plugin/bigarray.c
@@ -1,5 +1,7 @@
 /* run.config
+   EXIT: 0
    OPT: -cpp-extra-args="-DFIT"
+   EXIT: 1
    OPT: -cpp-extra-args="-DLARGE"
  */
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
index c62b8402ac0db48f4a00c2aeaa1b8808dbccb4d2..9fd78a23491e2568ab7e0450d68b57ba394eb657 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
@@ -1,6 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
-[kernel] tests/wp_plugin/bigarray.c:26: Warning: 
+[kernel] tests/wp_plugin/bigarray.c:28: Warning: 
   Cannot represent length of array as an attribute
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
@@ -8,13 +8,13 @@
   Function f
 ------------------------------------------------------------
 
-Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 25):
+Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 27):
 Prove: true.
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'f':
-Effect at line 26
+Effect at line 28
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
index 08244d758f02cf3e53bbe3941ba108f5c7d08cb9..f997c62a18c6ea602114265f971b9acf38ebbf7b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
@@ -1,13 +1,13 @@
 # frama-c -wp [...]
 [kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
-[kernel] tests/wp_plugin/bigarray.c:26: Warning: 
+[kernel] tests/wp_plugin/bigarray.c:28: Warning: 
   Cannot represent length of array as an attribute
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/bigarray.c:26: Warning: 
+[wp] tests/wp_plugin/bigarray.c:28: Warning: 
   Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] tests/wp_plugin/bigarray.c:27: Warning: 
+[wp] tests/wp_plugin/bigarray.c:29: Warning: 
   Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] tests/wp_plugin/bigarray.c:19: User Error: 
+[wp] tests/wp_plugin/bigarray.c:21: User Error: 
   Array size too large (0xFFFFFFFFFFFFFFFF)
 [kernel] Plug-in wp aborted: invalid user input.