From 5007cf39178ec9147c4c30bafead6f04e73d229b Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 6 Jun 2025 09:55:21 -0700
Subject: [PATCH 1/2] edit doc

---
 docs/src/reference/experimental/quantifiers.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/docs/src/reference/experimental/quantifiers.md b/docs/src/reference/experimental/quantifiers.md
index c62a70f2c7b3..2ea9d7cba082 100644
--- a/docs/src/reference/experimental/quantifiers.md
+++ b/docs/src/reference/experimental/quantifiers.md
@@ -14,8 +14,8 @@ Kani currently supports the following quantifiers:
 ```rust
 #[kani::proof]
 fn test_forall() {
-    let v = vec![10; 10];
-    kani::assert(kani::forall!(|i in 0..10| v[i] == 10));
+    let v : [u8;10] = [10; 10];
+    assert!(kani::forall!(|i in (0,10)| v[i] == 10) );
 }
 ```
 
@@ -27,11 +27,13 @@ fn test_forall() {
 ```rust
 #[kani::proof]
 fn test_exists() {
-    let v = vec![1, 2, 3, 4, 5];
-    kani::assert(kani::exists!(|i in 0..v.len()| v[i] == 3));
+    let v : [u8;5] = [1, 2, 3, 4, 5];
+    assert!(kani::exists!(|i in (0,v.len())| v[i] == 3));
 }
 ```
 
+When the range is not specified, it is assumed to be the whole `usize` range.
+
 ### Limitations
 
 #### Array Indexing
@@ -39,7 +41,6 @@ fn test_exists() {
 The performance of quantifiers can be affected by the depth of call stacks in the quantified expressions. If the call stack is too deep, Kani may not be able to evaluate the quantifier effectively, leading to potential timeouts or running out of memory. Actually, array indexing in Rust leads to a deep call stack, which can cause issues with quantifiers. To mitigate this, consider using *unsafe* pointer dereferencing instead of array indexing when working with quantifiers. For example:
 
 ```rust
-
 #[kani::proof]
 fn vec_assert_forall_harness() {
     let v = vec![10 as u8; 128];

From 7aeabe4544937bdd15f57406ac557ec7edf85791 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Tue, 10 Jun 2025 08:02:07 -0700
Subject: [PATCH 2/2] remove unspecified range

---
 docs/src/reference/experimental/quantifiers.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/docs/src/reference/experimental/quantifiers.md b/docs/src/reference/experimental/quantifiers.md
index 2ea9d7cba082..a38698a8023b 100644
--- a/docs/src/reference/experimental/quantifiers.md
+++ b/docs/src/reference/experimental/quantifiers.md
@@ -32,7 +32,6 @@ fn test_exists() {
 }
 ```
 
-When the range is not specified, it is assumed to be the whole `usize` range.
 
 ### Limitations