Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt)#3252

kroening merged 1 commit intodiffblue:developdiffblue/cbmc:developfrom

tautschnig:vs-no-to_integertautschnig/cbmc:vs-no-to_integerCopy head branch name to clipboard