Coercing references to arrays to references of slices confuses Prusti

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

fn main() {}

pub fn test() {
    let a = &mut [1,2,3];
    // let a: &mut [_] = a;
    swap(a);
    assert!(a[0] == 3);
    assert!(a[1] == 2);
    assert!(a[2] == 1);
}

/// Swap the first and last element of a slice.
#[requires(slice.len() >= 2)]
#[ensures(slice[0] == old(slice[slice.len() - 1]))]
#[ensures(old(slice[0]) == slice[slice.len() - 1])]
#[ensures(forall(|i: usize|
    (0 < i && i < slice.len() - 1) ==> (slice[i] == old(slice[i])),
    triggers=[(slice[i],)]
))]
pub fn swap(slice: &mut [i32]) {
    let tmp = slice[0];
    let last = slice.len() -1;
    slice[0] = slice[last];
    slice[last] = tmp;
}

Fails verification with the error:

error: [Prusti: verification error] the asserted expression might not hold
  --> src/lib.rs:27:5
   |
26 |     assert!(a[0] == 3);
   |     ^^^^^^^^^^^^^^^^^^

If I uncomment the line // let a: &mut [_] = a; then verification fails with:

error: [Prusti: verification error] the asserted expression might not hold
  --> src/lib.rs:27:5
   |
27 |     assert!(a[1] == 2);
   |     ^^^^^^^^^^^^^^^^^^

If I modify the method signature of fn swap to pub fn swap(slice: &mut [i32; 3]), then verification succeeds:

use prusti_contracts::*;

fn main() {}

pub fn test() {
    let a = &mut [1,2,3];
    swap(a);
    assert!(a[0] == 3);
    assert!(a[1] == 2);
    assert!(a[2] == 1);
}

/// Swap the first and last element of a slice.
#[requires(slice.len() >= 2)]
#[ensures(slice[0] == old(slice[slice.len() - 1]))]
#[ensures(old(slice[0]) == slice[slice.len() - 1])]
#[ensures(forall(|i: usize|
    (0 < i && i < slice.len() - 1) ==> (slice[i] == old(slice[i])),
    triggers=[(slice[i],)]
))]
pub fn swap(slice: &mut [i32; 3]) {
    let tmp = slice[0];
    let last = slice.len() -1;
    slice[0] = slice[last];
    slice[last] = tmp;
}

I'm digging a little deeper into this one, but so far I did not spot any additional helpful details. I will update this issue if I find something interesting!