diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..53e8b93a4eb19154655eac272508d2554e39a0e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
@@ -0,0 +1,24 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function mess1
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_acsl/postassigns2.c, line 6) in 'mess1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
+Call Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
+Call Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e6a7ddd408dd3858206a0e01bc153794d6b812d2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_mess1_exits : Valid
+[wp] [Qed] Goal typed_mess1_assigns_exit : Valid
+[wp] [Qed] Goal typed_mess1_assigns_normal : Valid
+[wp] Proved goals:    3 / 3
+  Qed:             3
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  mess1                     3        -        3       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/postassigns2.c b/src/plugins/wp/tests/wp_acsl/postassigns2.c
new file mode 100644
index 0000000000000000000000000000000000000000..eedaa11f4c32e8ccf3f4e22881f01d2ea4cca500
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/postassigns2.c
@@ -0,0 +1,11 @@
+/*@ exits \false;
+  @ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
+*/
+void receive1(unsigned char *message, unsigned int *size);
+
+/*@ exits \false;
+  @ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
+*/
+void mess1(unsigned char *message, unsigned int *size) {
+   receive1(message, size);
+}