I tried this code: cargo-kani/vecdeque-cve/

using the following command line invocation:
./scripts/kani-regressions.sh

with Kani version: git clone --branch 1478-bug-replication https://github.com/YoshikiTakashima/kani.git

I expected to see this happen: This test case to pass.

Instead, this happened: The test case fails b/c spurious warnings
differ from expected output.

It seems he cause appears to be that passing extra symtabs in
kani-driver/src/call_cargo.rs. If that is removed, then the warnings go away.