Do not copy on initialization#4220

tautschnig merged 1 commit intodiffblue:developdiffblue/cbmc:developfrom

peterschrammel:fix-copy-on-initpeterschrammel/cbmc:fix-copy-on-initCopy head branch name to clipboard