/* frama-c -wp -wp-rte   */
/* alt-ergo version 0.94 */

void arithmetic_testcase(unsigned i) {
    /*@ assert i <= (unsigned) -10 ==> i + 9 <= (unsigned) -1; */
}