diff --git a/src/exercises/array_init.c b/src/exercises/array_init.c
index a4755894..fcabe95f 100644
--- a/src/exercises/array_init.c
+++ b/src/exercises/array_init.c
@@ -1,14 +1,14 @@
 void array_init (char *p, unsigned int n)
-/*@ requires take A = each(integer i; i < n) { 
+/*@ requires take A = each(integer i; 0 <= i && i < n) {
                          RW<char>( array_shift<char>(p, i)) };
-    ensures  take A_post = each(integer i; i < n) { 
+    ensures  take A_post = each(integer i; 0 <= i && i < n) {
                              RW<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take Ai = each(integer i; i < n) { 
+  /*@ inv take Ai = each(integer i; 0 <= i && i < n) {
                       RW<char>( array_shift<char>(p, i)) };
           {p} unchanged; 
           {n} unchanged;
diff --git a/src/exercises/array_init_rev.c b/src/exercises/array_init_rev.c
index 03ede4cd..cde7086e 100644
--- a/src/exercises/array_init_rev.c
+++ b/src/exercises/array_init_rev.c
@@ -1,14 +1,14 @@
 void array_init_rev (char *p, unsigned int n)
-/*@ requires take A = each(integer i; i < n) { 
+/*@ requires take A = each(integer i; 0 <= i && i < n) {
                         RW<char>( array_shift<char>(p, i)) };
-    ensures  take A_post = each(integer i; i < n) { 
+    ensures  take A_post = each(integer i; 0 <= i && i < n) {
                              RW<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take Al = each(integer i; i < n-j) { 
+  /*@ inv take Al = each(integer i; 0 <= i && i < n-j) {
                       RW<char>( array_shift<char>(p, i)) };
           take Ar = each(integer i; n-j <= i && i < n) { 
                       RW<char>( array_shift<char>(p, i)) };
diff --git a/src/exercises/array_load.c b/src/exercises/array_load.c
index f1efd5cf..9f7705e7 100644
--- a/src/exercises/array_load.c
+++ b/src/exercises/array_load.c
@@ -1,8 +1,8 @@
 unsigned int read (unsigned int *p, unsigned int n, unsigned int i)
-/*@ requires take A = each(integer j; j < n)
+/*@ requires take A = each(integer j; 0 <= j && j < n)
                       { RW<unsigned int>(array_shift<unsigned int>(p,j)) };
              i < n; 
-    ensures take A_post = each(integer j; j < n) 
+    ensures take A_post = each(integer j; 0 <= j && j < n)
                           { RW<unsigned int>(array_shift<unsigned int>(p,j)) };
             return == A[i];
 @*/