Skip to content

Spurious failure in tests/kani/FunctionContracts/modify_slice_elem.rs #4029

Description

@zhassan-aws

This is a tracking issue for resolving the spurious failure with tests/kani/FunctionContracts/modify_slice_elem.rs which started failing with the 2025-04-05 toolchain upgrade. This was changed to a fixme test in #4018.

More details on the cause for spurious failure is in #4009.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions