change unwind to solver(cvc5)

Author: thanhnguyen-aws

library/core/src/ffi/c_str.rs

@@ -891,7 +891,7 @@ mod verify {
 
     // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
     #[kani::proof]
-    #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32
+    #[kani::solver(cvc5)] // 7.3 seconds when 16; 33.1 seconds when 32
     fn check_from_bytes_until_nul() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -907,7 +907,7 @@ mod verify {
 
     //  pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr
     #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)]
-    #[kani::unwind(33)]
+    #[kani::solver(cvc5)]
     fn check_from_bytes_with_nul_unchecked() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -926,7 +926,7 @@ mod verify {
 
     // pub fn bytes(&self) -> Bytes<'_>
     #[kani::proof]
-    #[kani::unwind(32)]
+    #[kani::solver(cvc5)]
     fn check_bytes() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -944,7 +944,7 @@ mod verify {
 
     // pub const fn to_str(&self) -> Result<&str, str::Utf8Error>
     #[kani::proof]
-    #[kani::unwind(32)]
+    #[kani::solver(cvc5)]
     fn check_to_str() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -988,7 +988,7 @@ mod verify {
 
     // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError>
     #[kani::proof]
-    #[kani::unwind(17)]
+    #[kani::solver(cvc5)]
     fn check_from_bytes_with_nul() {
         const MAX_SIZE: usize = 16;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -1027,7 +1027,7 @@ mod verify {
 
     // pub const fn to_bytes(&self) -> &[u8]
     #[kani::proof]
-    #[kani::unwind(32)]
+    #[kani::solver(cvc5)]
     fn check_to_bytes() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -1072,7 +1072,7 @@ mod verify {
 
     // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
     #[kani::proof_for_contract(CStr::from_ptr)]
-    #[kani::unwind(33)]
+    #[kani::solver(cvc5)]
     fn check_from_ptr_contract() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();
@@ -1085,7 +1085,7 @@ mod verify {
 
     // pub const fn is_empty(&self) -> bool
     #[kani::proof]
-    #[kani::unwind(33)]
+    #[kani::solver(cvc5)]
     fn check_is_empty() {
         const MAX_SIZE: usize = 32;
         let string: [u8; MAX_SIZE] = kani::any();