Incorrect verification results for function/closure dyn traits

The following fails to verify:

```rust
fn foo(fun: &mut dyn FnMut(i32) -> i32) -> i32 {
    fun(1)
}

fn main() {
    let r = foo(&mut move |z : i32| { z } );
    assert!(r == 1); // should succeed
}
```

In the generated CBMC-C code, in some places we pass the closure argument as a tuple, but in others we expect the flattened int. 
