Fix CI: remove loop invariants that cause CBMC assigns check interference

The #[loop_invariant] annotations we added triggered CBMC's loop contract
assigns checking globally, causing the pre-existing check_from_ptr_contract
harness to fail ("Check that len is assignable" in strlen). This also caused
the kani-compiler to crash (SIGABRT) in autoharness metrics mode.

Fix: Replace loop-based #[cfg(kani)] abstractions with straight-line
nondeterministic abstractions that eliminate the loops entirely under Kani.
This achieves the same unbounded verification without loop invariants:
- next_reject/next_reject_back: single nondeterministic step
- MCES overrides: single nondeterministic step
- next_match/next_match_back: keep real implementation (no loop invariant)

Revert the safety import cfg change since we no longer use loop_invariant.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: jrey8343