MPSC Channel test case times out. #1286
Description
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");
}