diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index e58389aab7ece10dcc4c09b551401a652b27463b..e9f59a74ee0e97911167a3e9e9a36fdab8a88d0d 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -997,8 +997,8 @@ axiomatic dynamic_allocation {
   }
  */
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -1056,7 +1056,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1413,7 +1413,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1578,7 +1578,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_functional.res.oracle b/tests/stl/oracle/stl_functional.res.oracle
index b6003ee97c8797af15c78d4e060f2a18b1e803f7..834f4bcf8a79c2e6d52f102aaf2f9e2142e5c0c9 100644
--- a/tests/stl/oracle/stl_functional.res.oracle
+++ b/tests/stl/oracle/stl_functional.res.oracle
@@ -726,8 +726,8 @@ axiomatic dynamic_allocation {
   }
  */
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -785,7 +785,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1142,7 +1142,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1307,7 +1307,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_memory.res.oracle b/tests/stl/oracle/stl_memory.res.oracle
index 6b9236e1c1611a8bbb8e818e0076fdafd6d15f7d..a28010d7e27effbda991b8f2c095611f7242d2a8 100644
--- a/tests/stl/oracle/stl_memory.res.oracle
+++ b/tests/stl/oracle/stl_memory.res.oracle
@@ -729,8 +729,8 @@ axiomatic dynamic_allocation {
   }
  */
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -788,7 +788,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1145,7 +1145,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1310,7 +1310,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 4c0014464f0a196ff0765ef858861cae928db0c1..d44adcdeb8760e12577b77f48f021a5f2da4d8dc 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -726,8 +726,8 @@ axiomatic dynamic_allocation {
 void *malloc(size_t size);
 
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -785,7 +785,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1142,7 +1142,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1307,7 +1307,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 7fd8b8b8cbd279f859d0708f0d02d6785cc7cb8b..e979a9ec076c5182da39013b9e638b269e0aa032 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -707,8 +707,8 @@ axiomatic dynamic_allocation {
 void *malloc(size_t size);
 
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -766,7 +766,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1123,7 +1123,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1288,7 +1288,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index b078461faee210b07d6f13a08255372558c40299..b3e59ee2b9729d1cd4d1f358df3f382c961ffae5 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -708,8 +708,8 @@ axiomatic dynamic_allocation {
 void *malloc(size_t size);
 
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -767,7 +767,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -1124,7 +1124,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1289,7 +1289,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_system_error.res.oracle b/tests/stl/oracle/stl_system_error.res.oracle
index 1755439f0fafe1291823fc02855e9c5c9e5457e7..b2169e75f552185ed7999a4793d0fba91cfb80c5 100644
--- a/tests/stl/oracle/stl_system_error.res.oracle
+++ b/tests/stl/oracle/stl_system_error.res.oracle
@@ -583,8 +583,8 @@ axiomatic dynamic_allocation {
   }
  */
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -641,7 +641,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -998,7 +998,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -1163,7 +1163,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);
diff --git a/tests/stl/oracle/stl_typeinfo.res.oracle b/tests/stl/oracle/stl_typeinfo.res.oracle
index f0fc168c9c4e2a027a3847e92ae596b427ca8882..a5b1a5d1c657001d913339045c5d73dfda0f3023 100644
--- a/tests/stl/oracle/stl_typeinfo.res.oracle
+++ b/tests/stl/oracle/stl_typeinfo.res.oracle
@@ -418,8 +418,8 @@ axiomatic dynamic_allocation {
   }
  */
 /*@
-predicate non_escaping{L}(void *s, size_t n) =
-  ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
+predicate non_escaping{L}(void *s, ℤ n) =
+  ∀ ℤ i; 0 ≤ i < n ⇒ ¬\initialized((char *)s + i);
  */
 /*@
 predicate empty_block{L}(void *s) =
@@ -476,7 +476,7 @@ int memcmp(void const *s1, void const *s2, size_t n);
           ∀ ℤ i;
             (0 ≤ i < \old(n) ⇒
              *((unsigned char *)\old(s) + i) ≡ \old(c)) ⇒
-            \result ≤ \old(s) + i;
+            (unsigned char *)\result ≤ (unsigned char *)\old(s) + i;
     
     behavior not_found:
       assumes char_not_found: memchr((char *)s, c, n) ≡ (0 ≢ 0);
@@ -833,7 +833,7 @@ char *strerror(int errnum);
  */
 char *strcpy(char * __restrict dest, char const * __restrict src);
 
-/*@ requires valid_string_src: valid_read_string(src);
+/*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
     requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
     ensures result_ptr: \result ≡ \old(dest);
@@ -998,7 +998,8 @@ size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n);
  */
 char *strdup(char const *s);
 
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+    assigns \result;
     assigns \result
       \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n),
             (indirect: __fc_heap_status);