Test that boxed fn parameters are implemented. (model-checking#3361)

This regression test ensures that issue model-checking#2874 does not reoccur, which
was last encountered in commit 9190831.

Resolves model-checking#2874

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Jacob Salzberg <[email protected]>
Co-authored-by: Jaisurya Nanduri <[email protected]>

tests/kani/Closure/boxed_closure.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// compile-flags: -Zmir-opt-level=2
+
+// The main function of this test moves an integer into a closure,
+// boxes the value, then passes the closure to a function that calls it.
+// This test covers the issue
+// https://github.com/model-checking/kani/issues/2874 .
+
+fn call_boxed_closure(f: Box<dyn Fn() -> ()>) -> () {
+    f()
+}
+
+// #[kani::proof]
+fn main() {
+    let x = 1;
+    let closure = move || {
+        let _ = x;
+        ()
+    };
+    call_boxed_closure(Box::new(closure));
+}