diff --git a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
index 356a117f24e6e6908400b327081bd1d8d7649e75..0a5c1608e7c642b2da40aa0a77192d68e4a61a96 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle
@@ -34,5 +34,9 @@ Prove: true.
 
 ------------------------------------------------------------
 [wp] Warning: Memory model hypotheses for function 'receive':
-  /*@ behavior typed: requires \separated(&size,message+(..)); */
+  /*@
+     behavior typed:
+       requires \separated(message + (..), &size);
+       requires \separated(message + (0 .. \at(size,Post)), &size);
+     */
   void receive(int n, char *message);