diff --git a/rust-tests/cbmc-reg/FatPointers/boxmuttrait.rs b/rust-tests/cbmc-reg/FatPointers/boxmuttrait.rs
new file mode 100644
index 000000000000..1876f13cca7d
--- /dev/null
+++ b/rust-tests/cbmc-reg/FatPointers/boxmuttrait.rs
@@ -0,0 +1,14 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::io::{sink, Write};
+
+fn main() {
+    let mut log: Box<dyn Write + Send> = Box::new(sink());
+    let dest: Box<dyn Write + Send> = Box::new(log.as_mut());
+
+    let mut log2: Box<dyn Write + Send> = Box::new(sink());
+    let buffer = vec![1, 2, 3, 5, 8];
+    let num_bytes = log2.write(&buffer).unwrap();
+    assert!(num_bytes == 5);
+}