Update test small_slice_eq

tests/expected/loop-contract/small_slice_eq.rs

@@ -6,20 +6,25 @@
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks --object-bits 8
+// kani-flags: -Z loop-contracts -Z mem-predicates --enable-unstable --cbmc-args --object-bits 8
 
-//! Check if loop contracts are correctly applied. The flag --no-standard-checks should be
-//! removed once same_object predicate is supported in loop contracts.
+//! Check if loop contracts are correctly applied.
 
 #![feature(stmt_expr_attributes)]
 #![feature(proc_macro_hygiene)]
 #![feature(ptr_sub_ptr)]
+
+extern crate kani;
+
+use kani::mem::same_allocation;
+
 unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     debug_assert_eq!(x.len(), y.len());
     unsafe {
         let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
         let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
-        #[kani::loop_invariant( px as isize >= x.as_ptr() as isize
+        #[kani::loop_invariant( same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
+        && px as isize >= x.as_ptr() as isize
         && py as isize >= y.as_ptr() as isize
         && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))]
         while px < pxend {
@@ -43,9 +48,10 @@ fn small_slice_eq_harness() {
     // because DFCC contract enforcement assumes that a definition for `free`
     // exists.
     let _ = Box::new(10);
-    let mut a = [1; 2000];
-    let mut b = [1; 2000];
+    const ARR_SIZE: usize = 2000;
+    let x: [u8; ARR_SIZE] = kani::any();
+    let y: [u8; ARR_SIZE] = kani::any();
     unsafe {
-        small_slice_eq(&mut a, &mut b);
+        small_slice_eq(&x, &y);
     }
 }