diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
index fd636bbb09f5ba89b5108a7ce87a4e990a7a5b87..2bf4af29a7cadc76df178840a9effa9a0a57e63c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle
@@ -6,17 +6,20 @@
   Function complex
 ------------------------------------------------------------
 
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
 Prove: true.
 
 ------------------------------------------------------------
-------------------------------------------------------------
-  Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
index 7af88b3ded647e1a034133916ef6f2aa0e9e03c0..60beed97a627e4bae8fdf8d14e919d8b7aa25c29 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle
@@ -6,17 +6,20 @@
   Function complex
 ------------------------------------------------------------
 
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
 Prove: true.
 
 ------------------------------------------------------------
-------------------------------------------------------------
-  Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
 Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
index 73c76c092af6f8fd3ab0fc93f3f7af41fb7e4d83..a28d76ae998651fd1e431981c7ab1e584be85d87 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle
@@ -2,12 +2,13 @@
 [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_complex_assigns : Valid
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_complex_assigns_exit : Valid
+[wp] [Qed] Goal typed_complex_assigns_normal : Valid
 [wp] [Qed] Goal typed_complex_call_job_requires : Valid
-[wp] Proved goals:    2 / 2
-  Qed:             2
+[wp] Proved goals:    3 / 3
+  Qed:             3
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  complex                   2        -        2       100%
+  complex                   3        -        3       100%
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/unit_tset.i b/src/plugins/wp/tests/wp_typed/unit_tset.i
index deaf2545a0dcf657e65ea5baff302625efa48abf..d08be34855d33feae62db63c647aa138909f2c48 100644
--- a/src/plugins/wp/tests/wp_typed/unit_tset.i
+++ b/src/plugins/wp/tests/wp_typed/unit_tset.i
@@ -1,21 +1,19 @@
-/* run.config_qualif
-   OPT:
-*/
-
-/*@ 
-  requires \valid( p + (0..n-1) ); 
+/*@
+  requires \valid( p + (0..n-1) );
   assigns p[0..n-1];
  */
 void job(int *p,int n);
 
-typedef struct S {
+struct S {
   int size ;
   int value[50] ;
-} ;
+} s ;
 
-/*@ requires s.size < 50; */
-void complex(struct S s)
+/*@
+  requires s.size < 50;
+  assigns s.value[1..s.size];
+*/
+void complex(void)
 {
-  /*@ assigns s.value[1..s.size]; */
   job( & s.value[1] , s.size );
 }