Update kani version

library/alloc/src/lib.rs

@@ -193,7 +193,6 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
-#![cfg_attr(kani, feature(proc_macro_hygiene))]
 #![rustc_preserve_ub_checks]
 // tidy-alphabetical-end
 //

library/core/src/lib.rs

@@ -246,6 +246,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+#![feature(proc_macro_hygiene)]
 // tidy-alphabetical-end
 //
 // Target features:

library/core/src/ptr/mod.rs

@@ -2626,7 +2626,7 @@ mod verify {
     }
 
     #[kani::proof]
-    pub fn check_swap_nonoverlapping_simple_untyped() {
+    pub fn check_swap_nonoverlapping_simple_untyped_slice_ptr() {
         const ARR_SIZE: usize = (2 << 32) -1;
         let mut x: [u8; ARR_SIZE] = kani::any();
         let mut xs = kani::slice::any_slice_of_array_mut(&mut x);
@@ -2636,6 +2636,5 @@ mod verify {
         unsafe {
             swap_nonoverlapping_simple_untyped(xs.as_mut_ptr(), ys.as_mut_ptr(), s);
         }
-}
-
+    }
 }

scripts/run-kani.sh

@@ -183,7 +183,7 @@ main() {
 
     echo "Running Kani verify-std command..."
 
-    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
+    "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
 }
 
 main

tool_config/kani-version.toml

@@ -2,4 +2,4 @@
 # incompatible with the verify-std repo.
 
 [kani]
-commit = "5f8f513d297827cfdce4c48065e51973ba563068"
+commit = "8400296f5280be4f99820129bc66447e8dff63f4"