From aa177cccb09f92d2a4512248ed930e0d2b4a30ae Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 8 Nov 2024 16:30:07 -0600
Subject: [PATCH] Address comments

---
 library/core/src/lib.rs             | 1 +
 library/core/src/str/validations.rs | 3 +--
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs
index 7c0596768b784..2c813ca0cb412 100644
--- a/library/core/src/lib.rs
+++ b/library/core/src/lib.rs
@@ -230,6 +230,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+// Required for Kani loop contracts, which are annotated as custom stmt attributes.
 #![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //
diff --git a/library/core/src/str/validations.rs b/library/core/src/str/validations.rs
index e9e5d5dbee985..f1f8a83da7d7f 100644
--- a/library/core/src/str/validations.rs
+++ b/library/core/src/str/validations.rs
@@ -284,10 +284,9 @@ pub mod verify {
     use super::*;
 
     #[kani::proof]
-    #[kani::unwind(8)]
     pub fn check_run_utf8_validation() {
         if kani::any() {
-            // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
+            // TODO: ARR_SIZE can be much larger with cbmc argument
             // `--arrays-uf-always`
             const ARR_SIZE: usize = 1000;
             let mut x: [u8; ARR_SIZE] = kani::any();