SE547: CBMC: CBMC Features [15/19]

CBMC handles integer and fixed point arithmetic.

Checks for: overflow, division by zero.