It would be good to add more regression tests for rvalue codegen for fat pointers as implemented in #101 One good regression test is rust-tests/cbmc-reg/SizeAndAlignOfDst. It would be good to have more.