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 fc8605283009333c1cc2ed29037b8ce30203b737..45299879b14e3dca2096f688d1cba863728a4377 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
@@ -36,6 +36,6 @@ Prove: true.
   /*@
      behavior typed:
        requires \separated(message + (..), &size);
-       requires \separated(message + (0 .. \at(size,Post)), &size);
+       ensures \separated(message + (0 .. \at(size,Post)), &size);
      */
   void receive(int n, char *message);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
index d2e3f2a9cd72abe8c290a08496c943a44251a532..498ce46ee4c976e50fbcd1c9a8222ecf5eac4b41 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.0.res.oracle
@@ -59,3 +59,7 @@ Assume {
 Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
 
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'h':
+  /*@ behavior typed:
+        ensures \separated(\result, &x); */
+  int *h(int x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
index 115e7900443a3b47594946cdc03820b159258291..9bc96f2981db0f1496e3ae32dd39f01cb210b55c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_alloc.1.res.oracle
@@ -59,3 +59,7 @@ Assume {
 Prove: !valid_rw(Malloc_0[L_y_25 <- 0], a, 1).
 
 ------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'h':
+  /*@ behavior typed_ref:
+        ensures \separated(\result, &x); */
+  int *h(int x);