Compilation error when using string in assert

[zhassan-aws]

The following code is valid (albeit deprecated) in Rust 2018, but Kani fails to compile it.

#[kani::proof]
fn main() {
    let s = String::new();
    assert!(true, s);
}

using the following steps:

1. cargo new --edition 2018 foo
2. cd foo
3. Replace src/main.rs with the code above.
4. Run cargo kani

with Kani version: b774d40

I expected to see this happen: Verification successful

Instead, this happened:

$ cargo kani
Kani Rust Verifier 0.56.0 (cargo plugin)
   Compiling foo v0.1.0 (/home/ubuntu/examples/assert/foo)
error: format argument must be a string literal
 --> src/main.rs:4:19
  |
4 |     assert!(true, s);
  |                   ^
  |
help: you might be missing a string literal to format with
  |
4 |     assert!(true, "{}", s);
  |                   +++++

error: could not compile `foo` (bin "foo") due to 1 previous error
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

If I remove #[kani::proof], I'm able to run it with cargo run:

$ cargo run
   Compiling foo v0.1.0 (/home/ubuntu/examples/assert/foo)
warning: panic message is not a string literal
 --> src/main.rs:3:19
  |
3 |     assert!(true, s);
  |                   ^
  |
  = note: this usage of `assert!()` is deprecated; it will be a hard error in Rust 2021
  = note: for more information, see <https://doc.rust-lang.org/nightly/edition-guide/rust-2021/panic-macro-consistency.html>
  = note: `#[warn(non_fmt_panics)]` on by default
help: add a "{}" format string to `Display` the message
  |
3 |     assert!(true, "{}", s);
  |                   +++++

warning: `foo` (bin "foo") generated 1 warning (run `cargo fix --bin "foo"` to apply 1 suggestion)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.13s
     Running `target/debug/foo`