add test for a weird mode corner case

Author: tjhance

source/rust_verify_test/tests/lifetime.rs

@@ -1009,3 +1009,20 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "used binding `t` isn't initialized")
 }
+
+test_verify_one_file! {
+    #[test] spec_fn_call_fn_arg_proof_code verus_code! {
+        struct R { }
+
+        pub proof fn consume(tracked r: R) {
+        }
+
+        pub proof fn y(tracked r: R) {
+            let z = ({
+                consume(r);
+                |y: int| y + 1
+            })(5);
+            consume(r);
+        }
+    } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::consume` with mode proof")
+}