The program ``` void main() { signed char i, j; i = j; i += 1; } ``` yields a goto program: ``` signed char i; signed char j; i = j; (signed int)i = (signed int)i + 1; ``` Broken since https://github.com/diffblue/cbmc/commit/e78e7d105c7e5716ae5205697f62380278bb8a23 See also https://github.com/diffblue/cbmc/pull/4209.