Add invariant that multiplication uses operands of the same size#8241

kroening merged 1 commit intodiffblue:developdiffblue/cbmc:developfrom

tautschnig:cleanup/multiplier-invarianttautschnig/cbmc:cleanup/multiplier-invariantCopy head branch name to clipboard