LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
12 82 12: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0
21 89 21: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0
24 96 24: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0
30 103 30: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 29, 30, 31, 34, 36, 37, 38, 39, 40, 41, 42, 44, 45, 46, 47, 48, 49, 50, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 73, 74, 75, 76, 77, 78, 79, 80, 81 using the following ranking functions, which are bounded by −105.

50: 0
49: 0
8: 0
9: 0
33: 0
34: 0
32: 0
29: 0
27: 0
28: 0
26: 0
21: 0
22: 0
10: 0
23: 0
20: 0
18: 0
19: 0
17: 0
16: 0
14: 0
15: 0
13: 0
11: 0
12: 0
7: 0
6: 0
5: 0
2: 0
3: 0
0: 0
1: 0
47: 0
48: 0
46: 0
24: 0
25: 0
4: 0
45: 0
44: 0
42: 0
43: 0
41: 0
40: 0
38: 0
39: 0
37: 0
30: 0
31: 0
35: 0
36: 0
50: −48
49: −49
8: −50
9: −51
33: −52
34: −53
32: −54
29: −55
27: −56
28: −57
26: −58
21: −59
22: −59
21_var_snapshot: −59
21*: −59
10: −62
23: −63
20: −64
18: −65
19: −66
17: −67
16: −68
14: −69
15: −70
13: −71
11: −72
12: −72
12_var_snapshot: −72
12*: −72
7: −75
6: −76
5: −77
2: −78
3: −79
0: −80
1: −81
47: −82
48: −83
46: −84
24: −85
25: −85
24_var_snapshot: −85
24*: −85
4: −88
45: −89
44: −90
42: −91
43: −92
41: −93
40: −94
38: −95
39: −96
37: −97
30: −98
31: −98
30_var_snapshot: −98
30*: −98
35: −102
36: −103

3 Location Addition

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

12* 85 12: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

4 Location Addition

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

12 83 12_var_snapshot: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

5 Location Addition

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

21* 92 21: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

6 Location Addition

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

21 90 21_var_snapshot: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

7 Location Addition

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

24* 99 24: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

8 Location Addition

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

24 97 24_var_snapshot: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

9 Location Addition

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

30* 106 30: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

10 Location Addition

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

30 104 30_var_snapshot: − tmp___08_post + tmp___08_post ≤ 0 ∧ tmp___08_post − tmp___08_post ≤ 0 ∧ − tmp___08_0 + tmp___08_0 ≤ 0 ∧ tmp___08_0 − tmp___08_0 ≤ 0 ∧ − tmp___050_post + tmp___050_post ≤ 0 ∧ tmp___050_post − tmp___050_post ≤ 0 ∧ − tmp___050_0 + tmp___050_0 ≤ 0 ∧ tmp___050_0 − tmp___050_0 ≤ 0 ∧ − tmp___036_post + tmp___036_post ≤ 0 ∧ tmp___036_post − tmp___036_post ≤ 0 ∧ − tmp___036_0 + tmp___036_0 ≤ 0 ∧ tmp___036_0 − tmp___036_0 ≤ 0 ∧ − tmp___022_post + tmp___022_post ≤ 0 ∧ tmp___022_post − tmp___022_post ≤ 0 ∧ − tmp___022_0 + tmp___022_0 ≤ 0 ∧ tmp___022_0 − tmp___022_0 ≤ 0 ∧ − tmp7_post + tmp7_post ≤ 0 ∧ tmp7_post − tmp7_post ≤ 0 ∧ − tmp7_0 + tmp7_0 ≤ 0 ∧ tmp7_0 − tmp7_0 ≤ 0 ∧ − tmp49_post + tmp49_post ≤ 0 ∧ tmp49_post − tmp49_post ≤ 0 ∧ − tmp49_0 + tmp49_0 ≤ 0 ∧ tmp49_0 − tmp49_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp21_post + tmp21_post ≤ 0 ∧ tmp21_post − tmp21_post ≤ 0 ∧ − tmp21_0 + tmp21_0 ≤ 0 ∧ tmp21_0 − tmp21_0 ≤ 0 ∧ − ret_check852_post + ret_check852_post ≤ 0 ∧ ret_check852_post − ret_check852_post ≤ 0 ∧ − ret_check852_0 + ret_check852_0 ≤ 0 ∧ ret_check852_0 − ret_check852_0 ≤ 0 ∧ − ret_check838_post + ret_check838_post ≤ 0 ∧ ret_check838_post − ret_check838_post ≤ 0 ∧ − ret_check838_0 + ret_check838_0 ≤ 0 ∧ ret_check838_0 − ret_check838_0 ≤ 0 ∧ − ret_check824_post + ret_check824_post ≤ 0 ∧ ret_check824_post − ret_check824_post ≤ 0 ∧ − ret_check824_0 + ret_check824_0 ≤ 0 ∧ ret_check824_0 − ret_check824_0 ≤ 0 ∧ − ret_check810_post + ret_check810_post ≤ 0 ∧ ret_check810_post − ret_check810_post ≤ 0 ∧ − ret_check810_0 + ret_check810_0 ≤ 0 ∧ ret_check810_0 − ret_check810_0 ≤ 0 ∧ − ret_check1054_post + ret_check1054_post ≤ 0 ∧ ret_check1054_post − ret_check1054_post ≤ 0 ∧ − ret_check1054_0 + ret_check1054_0 ≤ 0 ∧ ret_check1054_0 − ret_check1054_0 ≤ 0 ∧ − ret_check1040_post + ret_check1040_post ≤ 0 ∧ ret_check1040_post − ret_check1040_post ≤ 0 ∧ − ret_check1040_0 + ret_check1040_0 ≤ 0 ∧ ret_check1040_0 − ret_check1040_0 ≤ 0 ∧ − ret_check1026_post + ret_check1026_post ≤ 0 ∧ ret_check1026_post − ret_check1026_post ≤ 0 ∧ − ret_check1026_0 + ret_check1026_0 ≤ 0 ∧ ret_check1026_0 − ret_check1026_0 ≤ 0 ∧ − ret_check1012_post + ret_check1012_post ≤ 0 ∧ ret_check1012_post − ret_check1012_post ≤ 0 ∧ − ret_check1012_0 + ret_check1012_0 ≤ 0 ∧ ret_check1012_0 − ret_check1012_0 ≤ 0 ∧ − n5_post + n5_post ≤ 0 ∧ n5_post − n5_post ≤ 0 ∧ − n5_0 + n5_0 ≤ 0 ∧ n5_0 − n5_0 ≤ 0 ∧ − n47_post + n47_post ≤ 0 ∧ n47_post − n47_post ≤ 0 ∧ − n47_0 + n47_0 ≤ 0 ∧ n47_0 − n47_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n19_post + n19_post ≤ 0 ∧ n19_post − n19_post ≤ 0 ∧ − n19_0 + n19_0 ≤ 0 ∧ n19_0 − n19_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i48_post + i48_post ≤ 0 ∧ i48_post − i48_post ≤ 0 ∧ − i48_0 + i48_0 ≤ 0 ∧ i48_0 − i48_0 ≤ 0 ∧ − i34_post + i34_post ≤ 0 ∧ i34_post − i34_post ≤ 0 ∧ − i34_0 + i34_0 ≤ 0 ∧ i34_0 − i34_0 ≤ 0 ∧ − i20_post + i20_post ≤ 0 ∧ i20_post − i20_post ≤ 0 ∧ − i20_0 + i20_0 ≤ 0 ∧ i20_0 − i20_0 ≤ 0

11 SCC Decomposition

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

11.1 SCC Subproblem 1/4

Here we consider the SCC { 21, 22, 21_var_snapshot, 21* }.

11.1.1 Transition Removal

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

21: 1 − 4⋅i6_0 + 4⋅n5_0
22: −1 − 4⋅i6_0 + 4⋅n5_0
21_var_snapshot: −4⋅i6_0 + 4⋅n5_0
21*: 2 − 4⋅i6_0 + 4⋅n5_0

11.1.2 Transition Removal

We remove transitions 90, 92, 28 using the following ranking functions, which are bounded by −2.

21: 0
22: −2
21_var_snapshot: −1
21*: 1

11.1.3 Splitting Cut-Point Transitions

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

11.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 89.

11.1.3.1.1 Splitting Cut-Point Transitions

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

11.2 SCC Subproblem 2/4

Here we consider the SCC { 11, 12, 12_var_snapshot, 12* }.

11.2.1 Transition Removal

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

11: −1 − 4⋅i20_0 + 4⋅n19_0
12: 1 − 4⋅i20_0 + 4⋅n19_0
12_var_snapshot: −4⋅i20_0 + 4⋅n19_0
12*: 2 − 4⋅i20_0 + 4⋅n19_0

11.2.2 Transition Removal

We remove transitions 83, 85, 32 using the following ranking functions, which are bounded by −3.

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

11.2.3 Splitting Cut-Point Transitions

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

11.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 82.

11.2.3.1.1 Splitting Cut-Point Transitions

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

11.3 SCC Subproblem 3/4

Here we consider the SCC { 24, 25, 24_var_snapshot, 24* }.

11.3.1 Transition Removal

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

24: 1 − 4⋅i34_0 + 4⋅n33_0
25: −1 − 4⋅i34_0 + 4⋅n33_0
24_var_snapshot: −4⋅i34_0 + 4⋅n33_0
24*: 2 − 4⋅i34_0 + 4⋅n33_0

11.3.2 Transition Removal

We remove transitions 97, 99, 33 using the following ranking functions, which are bounded by −3.

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

11.3.3 Splitting Cut-Point Transitions

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

11.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 96.

11.3.3.1.1 Splitting Cut-Point Transitions

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

11.4 SCC Subproblem 4/4

Here we consider the SCC { 30, 31, 30_var_snapshot, 30* }.

11.4.1 Transition Removal

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

30: 1 − 4⋅i48_0 + 4⋅n47_0
31: −1 − 4⋅i48_0 + 4⋅n47_0
30_var_snapshot: −4⋅i48_0 + 4⋅n47_0
30*: 2 − 4⋅i48_0 + 4⋅n47_0

11.4.2 Transition Removal

We remove transitions 104, 106, 43 using the following ranking functions, which are bounded by −3.

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

11.4.3 Splitting Cut-Point Transitions

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

11.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 103.

11.4.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert