diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 5c23a7358caf..4c0fe98cc65d 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -532,12 +532,16 @@ impl ValidateArgs for VerificationArgs { ); } - if self.visualize && !self.common_args.enable_unstable { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "Missing argument: --visualize now requires --enable-unstable + if self.visualize { + if !self.common_args.enable_unstable { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "Missing argument: --visualize now requires --enable-unstable due to open issues involving incorrect results.", - )); + )); + } else { + print_deprecated(&self.common_args, "--visualize", "--concrete-playback"); + } } if self.mir_linker { diff --git a/tests/cargo-kani/simple-visualize/main.expected b/tests/cargo-kani/simple-visualize/main.expected index a863a195a4ff..1d0839175310 100644 --- a/tests/cargo-kani/simple-visualize/main.expected +++ b/tests/cargo-kani/simple-visualize/main.expected @@ -1 +1,2 @@ +warning: The `--visualize` option is deprecated. This option will be removed soon. Consider using `--concrete-playback` instead report-main/html/index.html