Kani assert override is more restrictive than standard assert

[tedinski]

This code works as a test but fails with Kani:

#[cfg_attr(test, test)]
#[cfg_attr(kani, kani::proof)]
fn check() {
    let v: bool = true;
    assert!(&v);
}

With test: builds successfully, no warnings/errors, test passes.

With kani:

error[E0308]: mismatched types
  --> test_bool_ref.rs:7:13
   |
7  |     assert!(&v);
   |     --------^^-
   |     |       |
   |     |       expected `bool`, found `&bool`
   |     arguments to this function are incorrect
   |
note: function defined here
  --> /home/ubuntu/rmc/library/kani/src/lib.rs:62:14
   |
62 | pub const fn assert(_cond: bool, _msg: &'static str) {
   |              ^^^^^^

[zhassan-aws]

Interesting. Apparently, this is valid Rust:

fn main() {
    let v: bool = true;
    if !&v {}

$ rustc neg.rs
$

which is what the standard assert macro expands to, but it is not valid without the negation:

fn main() {
    let v: bool = true;
    if &v {}

$ rustc not_neg.rs 
error[E0308]: mismatched types
 --> not_neg.rs:3:8
  |
3 |     if &v { }
  |        ^^ expected `bool`, found `&bool`
  |
help: consider removing the borrow
  |
3 -     if &v { }
3 +     if v { }
  |

error: aborting due to previous error

For more information about this error, try `rustc --explain E0308`.

[zhassan-aws]

I've opened #2117 to fix this via a hack. Out of curiosity, where did you see this? It is a bit confusing that if !&b is valid Rust but if &b isn't.