A comment in the Kani backend claims the following about compare-and-exchange operations:

In a sequential context, the update is always sucessful so we assume the second value to be true.

Is this true? Consider the program cas.rs:

use std::sync::atomic::{AtomicU8, Ordering};

fn main() {
    let x = AtomicU8::new(0);
    let r = x.compare_exchange(1, 2, Ordering::Relaxed, Ordering::Relaxed);
    println!("{}", r.is_err());
}

#[cfg(kani)]
#[kani::proof]
fn check_is_err() {
    let x = AtomicU8::new(0);
    let r = x.compare_exchange(1, 2, Ordering::Relaxed, Ordering::Relaxed);
    assert!(r.is_err());
}

$ rustc cas.rs && ./cas
true

$ kani cas.rs --harness check_is_err
...

SUMMARY:
 ** 1 of 101 failed (1 unreachable)
Failed Checks: assertion failed: r.is_err()
 File: "cas.rs", line 17, in check_is_err

VERIFICATION:- FAILED

It seems like the claim is true assuming the sequential code is correct. But assuming that the code is correct kind of defeats the purpose of using Kani.

This issue also affects the compare_exchange_weak method.