Breaking off from https://github.com/model-checking/rmc/issues/240 to have distinct issues. The problem is that we fail verification for calls through `FnOnce` vtable closures: ``` let f: Box<dyn FnOnce()> = Box::new(|x| { assert(x == 2); // should fail }); f(1); ```