`assert` is ambiguous (E0659) in dependencies that glob-import prelude macros (e.g. libc >= 0.2.188)

[tautschnig]

I tried this code (any crate depending on libc >= 0.2.188, published 2026-07-21; a plain cargo new with libc = "0.2" and any #[kani::proof] harness suffices):

cargo kani

with Kani version: main since #4643 (i.e. any version with the #[macro_use] macro-override injection).

I expected to see this happen: the crate compiles and the harness is verified.

Instead, this happened: compilation of libc fails with dozens of

error[E0659]: `assert` is ambiguous
  --> .../libc-0.2.188/src/types.rs:73:5
   |
73 |     assert!(size_of::<u16>() <= size_of::<c_short>()); // Should always be true
   |     ^^^^^^ ambiguous name
   |
   = note: ambiguous because of a conflict between a name from a glob import and an outer scope during import or macro resolution
note: `assert` could refer to the macro imported here [--> libc's `use crate::prelude::*;`]
note: `assert` could also refer to the macro imported here [--> <kani_macro_overrides>]

Root cause: since #4643, kani-compiler injects #[macro_use] extern crate std as _kani_std_macros; into every std crate it compiles, placing Kani's assert!/panic!/… overrides in the macro_use-prelude scope. That scope shadows the standard prelude silently (intended), but is ambiguous (E0659) against an explicit glob import of the same macro name. libc's internal prelude does pub(crate) use core::{assert, ...} and its modules use crate::prelude::* — harmless until libc 0.2.188 added assert! calls in such a module (src/types.rs type-size sanity checks). Any user whose lockfile resolves libc ≥ 0.2.188 is affected; Kani's own CI regression suites fail on every PR for the same reason (the test manifests use a floating libc = "0.2"; pushes to main still pass only because their last dependency resolution predates the libc release).

Fix in preparation: only inject the overrides into local crates, not external (registry/git) dependencies, using Session::opts.lint_cap as the discriminator (cargo passes --cap-lints allow exactly for non-local dependencies). External dependencies then use the real assert!/panic! macros, which Kani models soundly — consistent with no_std dependencies, which never had the overrides. Local path/workspace dependencies keep the overrides (as pinned by the assert-reach and stubbing-ws-packages tests).