NO Initial ITS Start location: l6 Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0 0: l0 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (-___retres1_9^post1+___retres1_9^0 == 0 /\ i_5^0-i_5^post1 == 0 /\ -___cil_tmp4_8^post1+___cil_tmp4_8^0 == 0 /\ -d_6^post1+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post1 == 0 /\ -result_4^post1+result_4^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post1 == 0), cost: 1 4: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1 5: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1 1: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1 2: l2 -> l4 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 6: l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1 3: l4 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (-___retres1_9^post4+___retres1_9^0 == 0 /\ -d_6^post4+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post4 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^0 == 0 /\ -i_5^post4+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post4 == 0 /\ -result_4^post4+result_4^0 == 0), cost: 1 7: l6 -> l0 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0 4: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1 5: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1 1: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1 9: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 6: l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1 8: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l6 -> l0 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1 Second rule: l0 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (-___retres1_9^post1+___retres1_9^0 == 0 /\ i_5^0-i_5^post1 == 0 /\ -___cil_tmp4_8^post1+___cil_tmp4_8^0 == 0 /\ -d_6^post1+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post1 == 0 /\ -result_4^post1+result_4^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post1 == 0), cost: 1 New rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1 Applied deletion Removed the following rules: 0 7 Eliminating location l4 by chaining: Applied chaining First rule: l2 -> l4 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 Second rule: l4 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (-___retres1_9^post4+___retres1_9^0 == 0 /\ -d_6^post4+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post4 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^0 == 0 /\ -i_5^post4+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post4 == 0 /\ -result_4^post4+result_4^0 == 0), cost: 1 New rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 Applied deletion Removed the following rules: 2 3 Simplified Transitions Start location: l6 Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0 11: l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1 12: l1 -> l2 : 1+d_6^0 <= 0, cost: 1 10: l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1 15: l2 -> l2 : i_5^0'=i_5^0-d_6^0, -i_5^0 <= 0, cost: 1 13: l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1 14: l6 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1 New rule: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ 1+i_5^0 <= 0), cost: 1 propagated equality ___cil_tmp4_8^post2 = result_4^post2 propagated equality i_5^post2 = i_5^0 propagated equality ___cil_tmp2_10^post2 = ___cil_tmp2_10^0 propagated equality ___retres3_7^post2 = 0 propagated equality d_6^post2 = d_6^0 propagated equality ___retres1_9^post2 = ___retres1_9^0 propagated equality result_4^post2 = 0 Simplified Guard Original rule: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ 1+i_5^0 <= 0), cost: 1 New rule: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1 New rule: l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1 New rule: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ -d_6^0 <= 0), cost: 1 propagated equality ___retres1_9^post5 = ___retres1_9^0 propagated equality ___cil_tmp4_8^post5 = ___retres3_7^post5 propagated equality d_6^post5 = d_6^0 propagated equality ___cil_tmp2_10^post5 = ___cil_tmp2_10^0 propagated equality i_5^post5 = i_5^0 propagated equality ___retres3_7^post5 = result_4^post5 propagated equality result_4^post5 = 0 Simplified Guard Original rule: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ -d_6^0 <= 0), cost: 1 New rule: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, -d_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, -d_6^0 <= 0, cost: 1 New rule: l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1 New rule: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, (0 == 0 /\ 1+d_6^0 <= 0), cost: 1 propagated equality result_4^post6 = result_4^0 propagated equality d_6^post6 = d_6^0 propagated equality ___cil_tmp2_10^post6 = ___cil_tmp2_10^0 propagated equality i_5^post6 = i_5^0 propagated equality ___retres3_7^post6 = ___retres3_7^0 propagated equality ___retres1_9^post6 = ___retres1_9^0 propagated equality ___cil_tmp4_8^post6 = ___cil_tmp4_8^0 Simplified Guard Original rule: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, (0 == 0 /\ 1+d_6^0 <= 0), cost: 1 New rule: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 1+d_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 1+d_6^0 <= 0, cost: 1 New rule: l1 -> l2 : 1+d_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1 New rule: l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 0 == 0, cost: 1 propagated equality ___retres1_9^post7 = 0 propagated equality ___cil_tmp4_8^post7 = ___cil_tmp4_8^0 propagated equality ___retres3_7^post7 = ___retres3_7^0 propagated equality d_6^post7 = d_6^0 propagated equality ___cil_tmp2_10^post7 = result_4^post7 propagated equality result_4^post7 = 0 propagated equality i_5^post7 = i_5^0 Simplified Guard Original rule: l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 0 == 0, cost: 1 New rule: l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, T, cost: 1 New rule: l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1 Propagated Equalities Original rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1 New rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (0 == 0 /\ i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1 propagated equality ___retres1_9^post1 = ___retres1_9^post8 propagated equality ___cil_tmp2_10^post1 = ___cil_tmp2_10^post8 propagated equality i_5^post1 = i_5^post8 propagated equality result_4^post1 = result_4^post8 propagated equality d_6^post1 = d_6^post8 propagated equality ___cil_tmp4_8^post1 = ___cil_tmp4_8^post8 propagated equality ___retres3_7^post1 = ___retres3_7^post8 Propagated Equalities Original rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (0 == 0 /\ i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1 New rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 0 == 0, cost: 1 propagated equality i_5^post8 = i_5^0 propagated equality d_6^post8 = d_6^0 propagated equality ___cil_tmp4_8^post8 = ___cil_tmp4_8^0 propagated equality ___retres1_9^post8 = ___retres1_9^0 propagated equality ___retres3_7^post8 = ___retres3_7^0 propagated equality ___cil_tmp2_10^post8 = ___cil_tmp2_10^0 propagated equality result_4^post8 = result_4^0 Simplified Guard Original rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 0 == 0, cost: 1 New rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, T, cost: 1 New rule: l6 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 New rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 propagated equality ___retres3_7^post4 = ___retres3_7^post3 propagated equality ___cil_tmp2_10^post4 = ___cil_tmp2_10^post3 propagated equality i_5^post4 = i_5^post3 propagated equality ___cil_tmp4_8^post4 = ___cil_tmp4_8^post3 propagated equality ___retres1_9^post4 = ___retres1_9^post3 propagated equality d_6^post4 = d_6^post3 propagated equality result_4^post4 = result_4^post3 Propagated Equalities Original rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ i_5^post3-i_5^0+d_6^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1 New rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0-d_6^0, result_4^0'=result_4^0, (0 == 0 /\ -i_5^0 <= 0), cost: 1 propagated equality ___cil_tmp2_10^post3 = ___cil_tmp2_10^0 propagated equality ___cil_tmp4_8^post3 = ___cil_tmp4_8^0 propagated equality ___retres1_9^post3 = ___retres1_9^0 propagated equality result_4^post3 = result_4^0 propagated equality i_5^post3 = i_5^0-d_6^0 propagated equality d_6^post3 = d_6^0 propagated equality ___retres3_7^post3 = ___retres3_7^0 Simplified Guard Original rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0-d_6^0, result_4^0'=result_4^0, (0 == 0 /\ -i_5^0 <= 0), cost: 1 New rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0-d_6^0, result_4^0'=result_4^0, -i_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0-d_6^0, result_4^0'=result_4^0, -i_5^0 <= 0, cost: 1 New rule: l2 -> l2 : i_5^0'=i_5^0-d_6^0, -i_5^0 <= 0, cost: 1 Step with 14 Trace 14[T] Blocked [{}, {}] Step with 11 Trace 14[T], 11[(-d_6^0 <= 0)] Blocked [{}, {}, {}] Step with 13 Trace 14[T], 11[(-d_6^0 <= 0)], 13[T] Blocked [{}, {}, {}, {}] Backtrack Trace 14[T], 11[(-d_6^0 <= 0)] Blocked [{}, {}, {13[T]}] Backtrack Trace 14[T] Blocked [{}, {11[T]}] Step with 12 Trace 14[T], 12[(1+d_6^0 <= 0)] Blocked [{}, {11[T]}, {}] Step with 10 Trace 14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)] Blocked [{}, {11[T]}, {}, {}] Step with 13 Trace 14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)], 13[T] Blocked [{}, {11[T]}, {}, {}, {}] Backtrack Trace 14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)] Blocked [{}, {11[T]}, {}, {13[T]}] Backtrack Trace 14[T], 12[(1+d_6^0 <= 0)] Blocked [{}, {11[T]}, {10[T]}] Step with 15 Trace 14[T], 12[(1+d_6^0 <= 0)], 15[(-i_5^0 <= 0)] Blocked [{}, {11[T]}, {10[T]}, {}] Nonterm Start location: l6 Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0 11: l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1 12: l1 -> l2 : 1+d_6^0 <= 0, cost: 1 10: l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1 15: l2 -> l2 : i_5^0'=i_5^0-d_6^0, -i_5^0 <= 0, cost: 1 16: l2 -> LoAT_sink : (i_5^0 >= 0 /\ d_6^0 <= 0), cost: NONTERM 17: l2 -> l2 : i_5^0'=-n*d_6^0+i_5^0, (-1+n >= 0 /\ i_5^0 >= 0 /\ -(-1+n)*d_6^0+i_5^0 >= 0), cost: 1 13: l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1 14: l6 -> l1 : T, cost: 1 Certificate of Non-Termination Original rule: l2 -> l2 : i_5^0'=i_5^0-d_6^0, (-i_5^0 <= 0), cost: 1 New rule: l2 -> LoAT_sink : (i_5^0 >= 0 /\ d_6^0 <= 0), cost: NONTERM i_5^0 >= 0 [0]: eventual decrease yields (i_5^0 >= 0 /\ -(-1+n)*d_6^0+i_5^0 >= 0) i_5^0 >= 0 [1]: eventual increase yields (i_5^0 >= 0 /\ d_6^0 <= 0) Replacement map: {i_5^0 >= 0 -> (i_5^0 >= 0 /\ d_6^0 <= 0)} Loop Acceleration Original rule: l2 -> l2 : i_5^0'=i_5^0-d_6^0, (-i_5^0 <= 0), cost: 1 New rule: l2 -> l2 : i_5^0'=-n*d_6^0+i_5^0, (-1+n >= 0 /\ i_5^0 >= 0 /\ -(-1+n)*d_6^0+i_5^0 >= 0), cost: 1 i_5^0 >= 0 [0]: eventual decrease yields (i_5^0 >= 0 /\ -(-1+n)*d_6^0+i_5^0 >= 0) i_5^0 >= 0 [1]: eventual increase yields (i_5^0 >= 0 /\ d_6^0 <= 0) Replacement map: {i_5^0 >= 0 -> (i_5^0 >= 0 /\ -(-1+n)*d_6^0+i_5^0 >= 0)} Step with 16 Trace 14[T], 12[(1+d_6^0 <= 0)], 16[(i_5^0 >= 0 /\ d_6^0 <= 0)] Blocked [{}, {11[T]}, {10[T]}, {16[T]}] Refute Counterexample [ ___cil_tmp2_10^0=0 ___cil_tmp4_8^0=0 ___retres1_9^0=0 ___retres3_7^0=0 d_6^0=-1 i_5^0=0 result_4^0=0 ] 14 [ ___cil_tmp2_10^0=0 ___cil_tmp4_8^0=0 ___retres1_9^0=0 ___retres3_7^0=0 d_6^0=-1 i_5^0=0 result_4^0=0 ] 12 [ ___cil_tmp2_10^0=0 ___cil_tmp4_8^0=0 ___retres1_9^0=0 ___retres3_7^0=0 d_6^0=-1 i_5^0=0 result_4^0=0 ] 16 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b