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