As per @thk123 s comments on https://github.com/diffblue/cbmc/pull/1889 there are some additional edge cases which we should be testing for, for instance pointer-to-pointer-to-const.