by T2Cert
0 | 0 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + ___const_100_0 − i_5_0 ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ ___cil_tmp4_8_post − ___retres3_7_post ≤ 0 ∧ − ___cil_tmp4_8_post + ___retres3_7_post ≤ 0 ∧ Result_4_post − ___cil_tmp4_8_post ≤ 0 ∧ − Result_4_post + ___cil_tmp4_8_post ≤ 0 ∧ Result_4_0 − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_post ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_post ≤ 0 ∧ − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 | |
0 | 1 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_100_0 + i_5_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 ∧ −1 − i_5_0 + i_5_post ≤ 0 ∧ 1 + i_5_0 − i_5_post ≤ 0 ∧ i_5_0 − i_5_post ≤ 0 ∧ − i_5_0 + i_5_post ≤ 0 ∧ − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 | |
2 | 2 | 0: | − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 | |
3 | 3 | 4: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_5_post ≤ 0 ∧ − i_5_post ≤ 0 ∧ i_5_0 − i_5_post ≤ 0 ∧ − i_5_0 + i_5_post ≤ 0 ∧ − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 | |
4 | 4 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_100_0 + i_5_0 ≤ 0 ∧ x_6_0 ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ ___cil_tmp4_8_post − ___retres3_7_post ≤ 0 ∧ − ___cil_tmp4_8_post + ___retres3_7_post ≤ 0 ∧ Result_4_post − ___cil_tmp4_8_post ≤ 0 ∧ − Result_4_post + ___cil_tmp4_8_post ≤ 0 ∧ Result_4_0 − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_post ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_post ≤ 0 ∧ − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 | |
4 | 5 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_100_0 + i_5_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 ∧ −1 − i_5_0 + i_5_post ≤ 0 ∧ 1 + i_5_0 − i_5_post ≤ 0 ∧ i_5_0 − i_5_post ≤ 0 ∧ − i_5_0 + i_5_post ≤ 0 ∧ − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 | |
5 | 6 | 3: | − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 |
The following invariants are asserted.
0: | − ___const_100_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 |
1: | Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ − ___const_100_0 ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 |
2: | − ___const_100_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 |
3: | TRUE |
4: | i_5_post ≤ 0 ∧ − i_5_post ≤ 0 ∧ i_5_0 ≤ 0 ∧ − i_5_0 ≤ 0 |
5: | TRUE |
The invariants are proved as follows.
0 | (0) | − ___const_100_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 | ||
1 | (1) | Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ − ___const_100_0 ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 | ||
2 | (2) | − ___const_100_0 ≤ 0 ∧ 1 − x_6_0 ≤ 0 | ||
3 | (3) | TRUE | ||
4 | (4) | i_5_post ≤ 0 ∧ − i_5_post ≤ 0 ∧ i_5_0 ≤ 0 ∧ − i_5_0 ≤ 0 | ||
5 | (5) | TRUE |
0 | 0 1 | |
0 | 1 2 | |
2 | 2 0 | |
3 | 3 4 | |
4 | 4 1 | |
4 | 5 0 | |
5 | 6 3 |
0 | 7 | : | − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 |
We remove transitions
, , , , using the following ranking functions, which are bounded by −15.5: | 0 |
3: | 0 |
4: | 0 |
0: | 0 |
2: | 0 |
1: | 0 |
: | −6 |
: | −7 |
: | −8 |
: | −9 |
: | −9 |
: | −9 |
: | −9 |
: | −13 |
8 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
10 : − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
8 : − x_6_0 + x_6_0 ≤ 0 ∧ x_6_0 − x_6_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
, , , }.We remove transition
using the following ranking functions, which are bounded by −3.: | −1 + 4⋅___const_100_0 − 4⋅i_5_0 |
: | 1 + 4⋅___const_100_0 − 4⋅i_5_0 |
: | −2 + 4⋅___const_100_0 − 4⋅i_5_0 |
: | 4⋅___const_100_0 − 4⋅i_5_0 |
8 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
10 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
We remove transitions 8, using the following ranking functions, which are bounded by −1.
: | 0 |
: | 2⋅x_6_0 |
: | −1 |
: | x_6_0 |
8 | lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
10 | lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
lexStrict[ [0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
We remove transition 10 using the following ranking functions, which are bounded by 0.
: | 0 |
: | 0 |
: | 0 |
: | 1 |
10 | lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
We consider 1 subproblems corresponding to sets of cut-point transitions as follows.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
T2Cert