Compilation error when using loop contracts in const fn

[qinheping]

I tried this code:

// SPDX-License-Identifier: Apache-2.0 OR MIT

// kani-flags: -Z loop-contracts

//! Check if loop contracts is correctly applied.

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

pub const BASE: usize = count_zero(&[]);

#[kani::proof]
pub fn check_counter() {
    assert_eq!(count_zero(&[1, 2]), 0)
}

const fn count_zero(slice: &[u8]) -> usize {
    let mut counter: usize = 0;
    let mut index: usize = 0;

    #[kani::loop_invariant(counter < slice.len())]
    while index < slice.len() {
        if slice[index] == 0 {
           counter += 1;
        }
        index += 1;
    }

    counter
}

with Kani version: #3151

I expected to see this happen: correctly compile.

Instead, this happened:

   |
55 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^ the evaluated program panicked at 'internal error: entered unreachable code: ', /library/kani/src/lib.rs:55:1
   |

[qinheping]

Resolved in #3151