MPSC Channel test case times out.

[YoshikiTakashima]

Tracking issue

Originally posted by @danielsn in #1285 (comment)

Running

./scripts/kani mpsc.rs

on the following code times out as of Kani 0.4.0 on M1 Mac, cargo 1.63.0-nightly (85e457e15 2022-06-07). Note that kani::unwind(1) fails to verify, and kani::unwind(2) or not putting an unwind limit leads to timeout.

// mpsc.rs
use std::sync::mpsc::*;

static mut CELL: i32 = 0;

struct DropSetCELLToOne {}

impl Drop for DropSetCELLToOne {
    fn drop(&mut self) {
        unsafe {
            CELL = 1;
        }
    }
}

#[kani::unwind(2)]
#[kani::proof]
fn main() {
    {
        let (send, recv) = channel::<DropSetCELLToOne>();
        send.send(DropSetCELLToOne {}).unwrap();
        let _to_drop: DropSetCELLToOne = recv.recv().unwrap();
    }
    assert_eq!(unsafe { CELL }, 1, "Drop should be called");
}

[tedinski]

Just to clarify: It times out with the unwind(2)? Or it times out without it and seems weird to need it?

[YoshikiTakashima]

@tedinski It's timeout with unwind(2) and no bound. So no verification success either way.

Text on original issue is also fixed.

[celinval]

Interesting, with the fix for #2164, this test passes on Mac but fails on Linux due to #1781. :(