Skip to content

Concrete Playback playback subcommand picks up regular unit tests and fails to compile #2489

@jaisnan

Description

@jaisnan

When there are other unit tests present, running cargo kani playback -- kani_concrete_playback_harness_i64_13477596495325479973 for example, gives compilation errors that are picked up from unit tests unrelated to kani. The command breaks completely and displays an empty output.

Metadata

Metadata

Assignees

No one assigned

    Labels

    T-High PriorityTag issues that have high priority[C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions