diff --git a/examples/basic_arrays_read/basic_arrays_read.spec b/examples/basic_arrays_read/basic_arrays_read.spec
index 2b0c35946..7d3636e36 100644
--- a/examples/basic_arrays_read/basic_arrays_read.spec
+++ b/examples/basic_arrays_read/basic_arrays_read.spec
@@ -1,6 +1,6 @@
 Globals:
 arr: int[2]
 
-L: arr[0] -> false, arr[1] -> false
+L: arr -> false
 Rely: old(arr[0]) == arr[0]
 Guarantee: true
\ No newline at end of file
diff --git a/examples/basic_arrays_write/basic_arrays_write.spec b/examples/basic_arrays_write/basic_arrays_write.spec
index 30f2b3029..cfe441557 100644
--- a/examples/basic_arrays_write/basic_arrays_write.spec
+++ b/examples/basic_arrays_write/basic_arrays_write.spec
@@ -1,7 +1,7 @@
 Globals:
 arr: int[2]
 
-L: arr[0] -> false, arr[1] -> false
+L: arr -> false
 Rely: true
 Guarantee: old(arr[0]) == arr[0]