Skip to content

Playback subcommand should respect Cargo.toml configuration #2467

@celinval

Description

@celinval

I tried running cargo kani playback in a package with the following Cargo.toml:

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
[package]
name = "test"
version = "0.1.0"
edition = "2021"

[package.metadata.kani.flags]
debug=true

[package.metadata.kani.unstable]
concrete-playback = true

using the following command line invocation:

cargo kani playback --test kani_concrete

with Kani version: #2464

I expected to see this happen: Playback should run the test

Instead, this happened: I get the following error:

error: The `playback` subcommand is unstable and requires `-Z concrete-playback` to be used.                                    
                                                                                                                                
Usage: cargo-kani [OPTIONS] [COMMAND]                           
                                                                                                                                
For more information, try '--help'.

If I add -Z concrete-playback, Kani runs but not in debug mode.

Metadata

Metadata

Labels

[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions