#874 spotted a bug in a CBMC harness where an uint8_t was passed to the function-under-proof, instead of a uint8_t *. This likely did not meaningfully reduce the expressivity of the proof, but was still a bug.
Task: Modify CBMC build so that the above issue would have been caught.