# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 18
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_100_0 − i_0 ≤ 0 ∧ 2 − i_0 + j_post ≤ 0 ∧ −2 + i_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 0 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_100_0 + i_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 3 2 4: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 2 3 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 5 4 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 7 5 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j10_0 + j10_post ≤ 0 ∧ 1 + j10_0 − j10_post ≤ 0 ∧ j10_0 − j10_post ≤ 0 ∧ − j10_0 + j10_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 8 6 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 8 7 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 8 8 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 9 9 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − j10_0 + ret_check12_post ≤ 0 ∧ j10_0 − ret_check12_post ≤ 0 ∧ j_post − ret_check12_post ≤ 0 ∧ − j_post + ret_check12_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ ret_check12_0 − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 9 10 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 10 11 11: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 12 12 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ j10_post − j_0 ≤ 0 ∧ − j10_post + j_0 ≤ 0 ∧ j10_0 − j10_post ≤ 0 ∧ − j10_0 + j10_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 13 13 12: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 13 14 3: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 13 15 12: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 14 16 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 15 17 14: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j6_0 + j6_post ≤ 0 ∧ 1 + j6_0 − j6_post ≤ 0 ∧ j6_0 − j6_post ≤ 0 ∧ − j6_0 + j6_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 6 18 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 16 19 15: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 16 20 14: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 16 21 15: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 11 22 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − j6_0 + ret_check8_post ≤ 0 ∧ j6_0 − ret_check8_post ≤ 0 ∧ j_post − ret_check8_post ≤ 0 ∧ − j_post + ret_check8_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ ret_check8_0 − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 11 23 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 1 24 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 ≤ 0 ∧ j6_post − j_0 ≤ 0 ∧ − j6_post + j_0 ≤ 0 ∧ j6_0 − j6_post ≤ 0 ∧ − j6_0 + j6_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 1 25 4: − i_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 17 26 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 18 27 17: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: 1 + i_0 ≤ 0 4: TRUE 5: 1 + i_0 ≤ 0 6: 1 + i_0 ≤ 0 7: 1 + i_0 ≤ 0 8: 1 + i_0 ≤ 0 9: 1 + i_0 ≤ 0 10: 1 + i_0 ≤ 0 11: 1 + i_0 ≤ 0 12: 1 + i_0 ≤ 0 13: 1 + i_0 ≤ 0 14: 1 + i_0 ≤ 0 15: 1 + i_0 ≤ 0 16: 1 + i_0 ≤ 0 17: TRUE 18: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) TRUE 2 (2) TRUE 3 (3) 1 + i_0 ≤ 0 4 (4) TRUE 5 (5) 1 + i_0 ≤ 0 6 (6) 1 + i_0 ≤ 0 7 (7) 1 + i_0 ≤ 0 8 (8) 1 + i_0 ≤ 0 9 (9) 1 + i_0 ≤ 0 10 (10) 1 + i_0 ≤ 0 11 (11) 1 + i_0 ≤ 0 12 (12) 1 + i_0 ≤ 0 13 (13) 1 + i_0 ≤ 0 14 (14) 1 + i_0 ≤ 0 15 (15) 1 + i_0 ≤ 0 16 (16) 1 + i_0 ≤ 0 17 (17) TRUE 18 (18) TRUE
• initial node: 18
• cover edges:
• transition edges:  0 0 1 0 1 2 1 24 10 1 25 4 2 3 0 3 2 4 5 4 6 6 18 9 7 5 5 8 6 7 8 7 5 8 8 7 9 9 3 9 10 8 10 11 11 11 22 13 11 23 16 12 12 6 13 13 12 13 14 3 13 15 12 14 16 10 15 17 14 16 19 15 16 20 14 16 21 15 17 26 2 18 27 17

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 2 28 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 6 35 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 10 42 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 2, 9, 12, 13, 14, 15, 22, 24, 25, 26, 27 using the following ranking functions, which are bounded by −29.

 18: 0 17: 0 0: 0 2: 0 1: 0 10: 0 11: 0 14: 0 15: 0 16: 0 13: 0 12: 0 5: 0 6: 0 7: 0 8: 0 9: 0 3: 0 4: 0 18: −11 17: −12 0: −13 2: −13 2_var_snapshot: −13 2*: −13 1: −14 10: −15 11: −15 14: −15 15: −15 16: −15 10_var_snapshot: −15 10*: −15 13: −16 12: −17 5: −18 6: −18 7: −18 8: −18 9: −18 6_var_snapshot: −18 6*: −18 3: −19 4: −24

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2* 31 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2 29 2_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6* 38 6: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6 36 6_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

10* 45 10: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

10 43 10_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_check8_post + ret_check8_post ≤ 0ret_check8_postret_check8_post ≤ 0ret_check8_0 + ret_check8_0 ≤ 0ret_check8_0ret_check8_0 ≤ 0ret_check12_post + ret_check12_post ≤ 0ret_check12_postret_check12_post ≤ 0ret_check12_0 + ret_check12_0 ≤ 0ret_check12_0ret_check12_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0j6_post + j6_post ≤ 0j6_postj6_post ≤ 0j6_0 + j6_0 ≤ 0j6_0j6_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

### 10 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

### 10.1 SCC Subproblem 1/3

Here we consider the SCC { 5, 6, 7, 8, 9, 6_var_snapshot, 6* }.

### 10.1.1 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

### 10.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 35.

The following invariants are asserted.

 0: − i_0 ≤ 0 1: − i_0 ≤ 0 2: − i_0 ≤ 0 3: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 4: TRUE 5: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 6: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 7: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 8: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 9: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 10: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 11: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 12: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 13: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 14: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 15: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 16: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 17: TRUE 18: TRUE 5: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 6: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 7: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 8: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 9: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 6_var_snapshot: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 6*: 1 ≤ 0 ∧ 1 + i_0 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (18) TRUE 1 (17) TRUE 2 (2) − i_0 ≤ 0 3 (0) − i_0 ≤ 0 5 (1) − i_0 ≤ 0 6 (2) − i_0 ≤ 0 7 (10) 1 ≤ 0 ∧ 1 + i_0 ≤ 0 8 (4) TRUE
• initial node: 0
• cover edges:  6 → 2
• transition edges:  0 27 1 1 26 2 2 3 3 3 0 5 3 1 6 5 24 7 5 25 8

### 10.1.1.1.2 Transition Removal

We remove transition 36 using the following ranking functions, which are bounded by −9.

 5: −1 6: −2 7: −3 8: −4 9: −5 6_var_snapshot: −6 6*: −7

### 10.1.1.1.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

### 10.2 SCC Subproblem 2/3

Here we consider the SCC { 10, 11, 14, 15, 16, 10_var_snapshot, 10* }.

### 10.2.1 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

### 10.2.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 42.

The following invariants are asserted.

 0: − i_0 ≤ 0 1: − i_0 ≤ 0 2: − i_0 ≤ 0 3: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 4: TRUE 5: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 6: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 7: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 8: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 9: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 10: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 11: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 12: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 13: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 14: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 15: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 16: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 17: TRUE 18: TRUE 10: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 11: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 14: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 15: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 16: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 10_var_snapshot: 1 ≤ 0 ∧ 1 + i_0 ≤ 0 10*: 1 ≤ 0 ∧ 1 + i_0 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (18) TRUE 1 (17) TRUE 2 (2) − i_0 ≤ 0 3 (0) − i_0 ≤ 0 5 (1) − i_0 ≤ 0 6 (2) − i_0 ≤ 0 7 (10) 1 ≤ 0 ∧ 1 + i_0 ≤ 0 8 (4) TRUE
• initial node: 0
• cover edges:  6 → 2
• transition edges:  0 27 1 1 26 2 2 3 3 3 0 5 3 1 6 5 24 7 5 25 8

### 10.2.1.1.2 Transition Removal

We remove transition 43 using the following ranking functions, which are bounded by −9.

 10: −1 11: −2 14: −3 15: −4 16: −5 10_var_snapshot: −6 10*: −7

### 10.2.1.1.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

### 10.3 SCC Subproblem 3/3

Here we consider the SCC { 0, 2, 2_var_snapshot, 2* }.

### 10.3.1 Transition Removal

We remove transition 1 using the following ranking functions, which are bounded by 2.

 0: −1 + 4⋅___const_100_0 − 4⋅i_0 2: 1 + 4⋅___const_100_0 − 4⋅i_0 2_var_snapshot: 4⋅___const_100_0 − 4⋅i_0 2*: 2 + 4⋅___const_100_0 − 4⋅i_0

### 10.3.2 Transition Removal

We remove transitions 29, 31, 3 using the following ranking functions, which are bounded by −3.

 0: −3 2: −1 2_var_snapshot: −2 2*: 0

### 10.3.3 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

### 10.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 28.

### 10.3.3.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

T2Cert

• version: 1.0