[wp] fixed duplicated returns

src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle

@@ -270,7 +270,7 @@ Prove: valid_rw(Malloc_0, p[i], 1).
 Goal Post-condition (file tests/wp_typed/array_initialized.c, line 288) in 'simpl':
 Let x = Mint_0[shift_sint32(t, 0)].
 Assume {
-  Type: is_sint32(x).
+  Type: is_sint32(simpl_0) /\ is_sint32(x).
   (* Heap *)
   Type: region(t.base) <= 0.
   (* Goal *)
@@ -279,8 +279,8 @@ Assume {
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 49) ->
       (Mint_0[shift_sint32(t, i_1)] = x))).
   If 0 <= x
-  Then { (* Return *) Have: simpl_0 = 1. }
-  Else { (* Return *) Have: simpl_0 = 0. }
+  Then { Have: simpl_0 = 1. }
+  Else { Have: simpl_0 = 0. }
 }
 Prove: (0 <= Mint_0[shift_sint32(t, i)]) <-> (simpl_0 = 1).
 

src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle

@@ -273,7 +273,7 @@ Prove: valid_rw(Malloc_0, Mptr_0[shift_PTR(a, i)], 1).
 Goal Post-condition (file tests/wp_typed/array_initialized.c, line 288) in 'simpl':
 Let x = Mint_0[shift_sint32(t, 0)].
 Assume {
-  Type: is_sint32(x).
+  Type: is_sint32(simpl_0) /\ is_sint32(x).
   (* Heap *)
   Type: region(t.base) <= 0.
   (* Goal *)
@@ -282,8 +282,8 @@ Assume {
   Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 49) ->
       (Mint_0[shift_sint32(t, i_1)] = x))).
   If 0 <= x
-  Then { (* Return *) Have: simpl_0 = 1. }
-  Else { (* Return *) Have: simpl_0 = 0. }
+  Then { Have: simpl_0 = 1. }
+  Else { Have: simpl_0 = 0. }
 }
 Prove: (0 <= Mint_0[shift_sint32(t, i)]) <-> (simpl_0 = 1).
 

src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle

@@ -26,7 +26,7 @@ Goal Post-condition (file tests/wp_typed/user_rec.i, line 9) in 'F1':
 Assume {
   Type: is_sint32(F1_0) /\ is_sint32(i) /\ is_sint32(n).
   If n <= 1
-  Then { (* Return *) Have: F1_0 = 1. }
+  Then { Have: F1_0 = 1. }
   Else {
     (* Invariant *)
     Have: L_fact(i - 1) = F1_0.

src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle

@@ -26,7 +26,7 @@ Goal Post-condition (file tests/wp_typed/user_rec.i, line 9) in 'F1':
 Assume {
   Type: is_sint32(F1_0) /\ is_sint32(i) /\ is_sint32(n).
   If n <= 1
-  Then { (* Return *) Have: F1_0 = 1. }
+  Then { Have: F1_0 = 1. }
   Else {
     (* Invariant *)
     Have: L_fact(i - 1) = F1_0.