====================================== B_OVERFLOW (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by B_OVERFLOW) Successfully verified. ====================================== B_OVERFLOW.overflow_integer_addition Verification failed. Line: 7. Possible arithmetic overflow. ====================================== B_OVERFLOW.no_overflow_integer_addition Successfully verified. ====================================== B_OVERFLOW.overflow_integer_subtraction Verification failed. Line: 19. Possible arithmetic overflow. ====================================== B_OVERFLOW.no_overflow_integer_subtraction Successfully verified. ====================================== B_OVERFLOW.overflow_natural_addition Verification failed. Line: 31. Possible arithmetic overflow. ====================================== B_OVERFLOW.no_overflow_natural_addition Successfully verified. ====================================== B_OVERFLOW.overflow_natural_subtraction Verification failed. Line: 43. Possible arithmetic overflow. ====================================== B_OVERFLOW.no_overflow_natural_subtraction Successfully verified.