An integer arithmetic result outside the range of its chosen representation. A programming language may specify wrapping, trapping or another behavior; a proof over mathematical integers must account for that difference.
New to topics? Read the docs here!