I added a test case here: [tests/kani/Intrinsics/SizeOfVal/fixme_size_of_fat_ptr.rs](https://github.com/model-checking/kani/commit/2ec1da9473bc298a795e6daa50530f125d07fe9c#diff-1b86643bc21300182c32776e56fd65b6ae1e106b3400593efac0fe2563f46acf) It fails due to incorrect implementation of `size_of_val`. See test for more details.