Once this lands: https://github.com/diffblue/cbmc/pull/6376 - [x] Update minimum CBMC version. - [ ] Enable fixme unit tests under `src/test/rmc/DynTrait/*_fixme.rs`. - [ ] Add unit test for InternedString deserialization. - [ ] Move flag check inside block, as listed here: https://github.com/model-checking/rmc/pull/536