LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 18

Transitions: (pre-variables and post-variables)

0	0	1:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
2	1	3:	arraySize_0 − i_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
2	2	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_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_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
5	3	6:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
7	4	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i17_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_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
7	5	8:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i17_0 ≤ 0 ∧ −1 − i17_0 + i17_post ≤ 0 ∧ 1 + i17_0 − i17_post ≤ 0 ∧ i17_0 − i17_post ≤ 0 ∧ − i17_0 + i17_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
9	6	10:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
11	7	8:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i15_0 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0 ∧ i17_post ≤ 0 ∧ − i17_post ≤ 0 ∧ i17_0 − i17_post ≤ 0 ∧ − i17_0 + i17_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
11	8	12:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i15_0 ≤ 0 ∧ −1 − i15_0 + i15_post ≤ 0 ∧ 1 + i15_0 − i15_post ≤ 0 ∧ i15_0 − i15_post ≤ 0 ∧ − i15_0 + i15_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
13	9	14:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
15	10	12:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i13_0 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i15_post ≤ 0 ∧ − i15_post ≤ 0 ∧ i15_0 − i15_post ≤ 0 ∧ − i15_0 + i15_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
15	11	16:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i13_0 ≤ 0 ∧ −1 − i13_0 + i13_post ≤ 0 ∧ 1 + i13_0 − i13_post ≤ 0 ∧ i13_0 − i13_post ≤ 0 ∧ − i13_0 + i13_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
16	12	15:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
14	13	16:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i13_post ≤ 0 ∧ − i13_post ≤ 0 ∧ i13_0 − i13_post ≤ 0 ∧ − i13_0 + i13_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
14	14	13:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_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_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
12	15	11:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
10	16	13:	0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i11_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_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
10	17	9:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i11_0 ≤ 0 ∧ −1 − i11_0 + i11_post ≤ 0 ∧ 1 + i11_0 − i11_post ≤ 0 ∧ i11_0 − i11_post ≤ 0 ∧ − i11_0 + i11_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
8	18	7:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
6	19	9:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i11_post ≤ 0 ∧ − i11_post ≤ 0 ∧ i11_0 − i11_post ≤ 0 ∧ − i11_0 + i11_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
6	20	5:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i9_0 ≤ 0 ∧ −1 − i9_0 + i9_post ≤ 0 ∧ 1 + i9_0 − i9_post ≤ 0 ∧ i9_0 − i9_post ≤ 0 ∧ − i9_0 + i9_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
4	21	2:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
1	22	5:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arraySize_0 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i9_post ≤ 0 ∧ − i9_post ≤ 0 ∧ i9_0 − i9_post ≤ 0 ∧ − i9_0 + i9_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
1	23	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arraySize_0 + i7_0 ≤ 0 ∧ −1 − i7_0 + i7_post ≤ 0 ∧ 1 + i7_0 − i7_post ≤ 0 ∧ i7_0 − i7_post ≤ 0 ∧ − i7_0 + i7_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
17	24	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i7_post ≤ 0 ∧ − i7_post ≤ 0 ∧ i7_0 − i7_post ≤ 0 ∧ − i7_0 + i7_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ tmp___0_0 − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_post ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
18	25	17:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
1:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
2:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
3:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
4:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
5:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
6:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
7:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
8:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
9:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
10:	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
11:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0
12:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0
13:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
14:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
15:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
16:	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
17:	TRUE
18:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
1	(1)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
2	(2)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
3	(3)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
4	(4)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
5	(5)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
6	(6)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
7	(7)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
8	(8)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0 ∧ i17_1 ≤ 0 ∧ − i17_1 ≤ 0
9	(9)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
10	(10)	i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
11	(11)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0
12	(12)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i15_1 ≤ 0 ∧ − i15_1 ≤ 0
13	(13)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
14	(14)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
15	(15)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
16	(16)	i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
17	(17)	TRUE
18	(18)	TRUE

initial node: 18
cover edges:

transition edges:

0	0 1
1	22 5
1	23 0
2	1 3
2	2 4
4	21 2
5	3 6
6	19 9
6	20 5
7	4 4
7	5 8
8	18 7
9	6 10
10	16 13
10	17 9
11	7 8
11	8 12
12	15 11
13	9 14
14	13 16
14	14 13
15	10 12
15	11 16
16	12 15
17	24 0
18	25 17

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

0	26	0:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
4	33	4:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
5	40	5:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
8	47	8:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
9	54	9:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
12	61	12:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
13	68	13:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0
16	75	16:	− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 1, 4, 7, 10, 13, 16, 19, 22, 24, 25 using the following ranking functions, which are bounded by −41.

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

4 Location Addition

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

0* 29 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

5 Location Addition

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

0 27 0_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

6 Location Addition

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

4* 36 4: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

7 Location Addition

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

4 34 4_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

8 Location Addition

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

5* 43 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

9 Location Addition

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

5 41 5_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

10 Location Addition

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

8* 50 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

11 Location Addition

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

8 48 8_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

12 Location Addition

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

9* 57 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

13 Location Addition

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

9 55 9_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

14 Location Addition

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

12* 64 12: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

15 Location Addition

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

12 62 12_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

16 Location Addition

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

13* 71 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

17 Location Addition

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

13 69 13_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

18 Location Addition

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

16* 78 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

19 Location Addition

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

16 76 16_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i17_post + i17_post ≤ 0 ∧ i17_post − i17_post ≤ 0 ∧ − i17_1 + i17_1 ≤ 0 ∧ i17_1 − i17_1 ≤ 0 ∧ − i17_0 + i17_0 ≤ 0 ∧ i17_0 − i17_0 ≤ 0 ∧ − i15_post + i15_post ≤ 0 ∧ i15_post − i15_post ≤ 0 ∧ − i15_1 + i15_1 ≤ 0 ∧ i15_1 − i15_1 ≤ 0 ∧ − i15_0 + i15_0 ≤ 0 ∧ i15_0 − i15_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − arraySize_0 + arraySize_0 ≤ 0 ∧ arraySize_0 − arraySize_0 ≤ 0

20 SCC Decomposition

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

20.1 SCC Subproblem 1/8

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

20.1.1 Transition Removal

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

2:	−1 + 4⋅arraySize_0 − 4⋅i_0
4:	1 + 4⋅arraySize_0 − 4⋅i_0
4_var_snapshot:	4⋅arraySize_0 − 4⋅i_0
4*:	2 + 4⋅arraySize_0 − 4⋅i_0

20.1.2 Transition Removal

We remove transitions 34, 36, 21 using the following ranking functions, which are bounded by −1.

2:	−1
4:	1
4_var_snapshot:	0
4*:	2

20.1.3 Splitting Cut-Point Transitions

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

20.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 33.

20.1.3.1.1 Splitting Cut-Point Transitions

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

20.2 SCC Subproblem 2/8

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

20.2.1 Transition Removal

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

7:	−1 + 4⋅arraySize_0 − 4⋅i17_0
8:	1 + 4⋅arraySize_0 − 4⋅i17_0
8_var_snapshot:	4⋅arraySize_0 − 4⋅i17_0
8*:	2 + 4⋅arraySize_0 − 4⋅i17_0

20.2.2 Transition Removal

We remove transitions 48, 50, 18 using the following ranking functions, which are bounded by −1.

7:	−1
8:	1
8_var_snapshot:	0
8*:	2

20.2.3 Splitting Cut-Point Transitions

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

20.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 47.

20.2.3.1.1 Splitting Cut-Point Transitions

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

20.3 SCC Subproblem 3/8

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

20.3.1 Transition Removal

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

11:	−1 + 4⋅arraySize_0 − 4⋅i15_0
12:	1 + 4⋅arraySize_0 − 4⋅i15_0
12_var_snapshot:	4⋅arraySize_0 − 4⋅i15_0
12*:	2 + 4⋅arraySize_0 − 4⋅i15_0

20.3.2 Transition Removal

We remove transitions 62, 64, 15 using the following ranking functions, which are bounded by −2.

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

20.3.3 Splitting Cut-Point Transitions

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

20.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 61.

20.3.3.1.1 Splitting Cut-Point Transitions

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

20.4 SCC Subproblem 4/8

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

20.4.1 Transition Removal

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

15:	−1 + 4⋅arraySize_0 − 4⋅i13_0
16:	1 + 4⋅arraySize_0 − 4⋅i13_0
16_var_snapshot:	4⋅arraySize_0 − 4⋅i13_0
16*:	2 + 4⋅arraySize_0 − 4⋅i13_0

20.4.2 Transition Removal

We remove transitions 76, 78, 12 using the following ranking functions, which are bounded by −3.

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

20.4.3 Splitting Cut-Point Transitions

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

20.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 75.

20.4.3.1.1 Splitting Cut-Point Transitions

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

20.5 SCC Subproblem 5/8

Here we consider the SCC { 13, 14, 13_var_snapshot, 13* }.

20.5.1 Transition Removal

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

13:	1 + 3⋅arraySize_0 − 3⋅i_0
14:	3⋅arraySize_0 − 3⋅i_0
13_var_snapshot:	1 + 3⋅arraySize_0 − 3⋅i_0
13*:	2 + 3⋅arraySize_0 − 3⋅i_0

20.5.2 Transition Removal

We remove transitions 69, 71, 9 using the following ranking functions, which are bounded by −1.

13:	1
14:	−1
13_var_snapshot:	0
13*:	2

20.5.3 Splitting Cut-Point Transitions

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

20.5.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 68.

20.5.3.1.1 Splitting Cut-Point Transitions

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

20.6 SCC Subproblem 6/8

Here we consider the SCC { 9, 10, 9_var_snapshot, 9* }.

20.6.1 Transition Removal

We remove transition 17 using the following ranking functions, which are bounded by 3.

9:	2 + 4⋅arraySize_0 − 4⋅i11_0
10:	4⋅arraySize_0 − 4⋅i11_0
9_var_snapshot:	1 + 4⋅arraySize_0 − 4⋅i11_0
9*:	3 + 4⋅arraySize_0 − 4⋅i11_0

20.6.2 Transition Removal

We remove transitions 55, 57, 6 using the following ranking functions, which are bounded by −2.

9:	0
10:	−2
9_var_snapshot:	−1
9*:	1

20.6.3 Splitting Cut-Point Transitions

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

20.6.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 54.

20.6.3.1.1 Splitting Cut-Point Transitions

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

20.7 SCC Subproblem 7/8

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

20.7.1 Transition Removal

We remove transition 20 using the following ranking functions, which are bounded by 3.

5:	2 + 4⋅arraySize_0 − 4⋅i9_0
6:	4⋅arraySize_0 − 4⋅i9_0
5_var_snapshot:	1 + 4⋅arraySize_0 − 4⋅i9_0
5*:	3 + 4⋅arraySize_0 − 4⋅i9_0

20.7.2 Transition Removal

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

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

20.7.3 Splitting Cut-Point Transitions

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

20.7.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 40.

20.7.3.1.1 Splitting Cut-Point Transitions

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

20.8 SCC Subproblem 8/8

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

20.8.1 Transition Removal

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

0:	1 + 3⋅arraySize_0 − 3⋅i7_0
1:	3⋅arraySize_0 − 3⋅i7_0
0_var_snapshot:	1 + 3⋅arraySize_0 − 3⋅i7_0
0*:	2 + 3⋅arraySize_0 − 3⋅i7_0

20.8.2 Transition Removal

We remove transitions 27, 29, 0 using the following ranking functions, which are bounded by −1.

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

20.8.3 Splitting Cut-Point Transitions

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

20.8.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 26.

20.8.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0