Kani should verify the existance of clashing C functions

[celinval]

I tried this code:

pub mod a {
    use std::ffi::c_int;
    extern "C" { fn isalpha(_: c_int) -> c_int; }
    pub fn wrap(x: c_int) -> c_int { unsafe { isalpha(x) } }
}

pub mod b {
    use std::ffi::c_int;
    extern "C" { fn isalpha(_: c_int, _: c_int) -> c_int; }
    pub fn wrap(x: c_int, y: c_int) -> c_int { unsafe { isalpha(x, y) } }
}

fn main() {
    let x = a::wrap(10));
    let y = b::wrap(10, 20);
    assert_eq!(x, y);
}

which is a modified version of rust-lang/rust#105146.

using the following command line invocation:

kani -Z c-ffi clashing.rs

with Kani version: 0.27.0

I expected to see this happen: Kani fails due to the clashing definitions

Instead, this happened: Verification succeeds