WORST_CASE(Omega(0),?)

Initial ITS
Start location: l6
   0: l0 -> l1 : length_16^0'=length_16^post0, temp0_18^0'=temp0_18^post0, head_19^0'=head_19^post0, tmp_21^0'=tmp_21^post0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0, rcd_47^0'=rcd_47^post0, i_83^0'=i_83^post0, temp0_14^0'=temp0_14^post0, head_15^0'=head_15^post0, result_11^0'=result_11^post0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post0, i_17^0'=i_17^post0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post0, rcd_77^0'=rcd_77^post0, (0 == 0 /\ result_dot_nondet_sdv_special_RETURN_VALUE_13^post0-length_16^post0 <= 0 /\ -temp0_14^post0+temp0_14^0 == 0 /\ temp0_18^0-temp0_18^post0 == 0 /\ -head_15^post0+head_15^0 == 0 /\ -temp_24^post0+temp_24^0 == 0 /\ -nondet_12^10+result_dot_nondet_sdv_special_RETURN_VALUE_13^post0 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 <= 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 == 0 /\ result_11^0-result_11^post0 == 0 /\ head_19^post0 <= 0 /\ head_19^post0 == 0 /\ tmp_21^0-tmp_21^post0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0 == 0 /\ -rcd_77^post0+rcd_77^0 == 0 /\ -i_17^post0 <= 0 /\ i_17^post0 <= 0 /\ i_17^post0 == 0 /\ i_83^0-i_83^post0 == 0 /\ -rcd_47^post0+rcd_47^0 == 0 /\ -head_19^post0 <= 0), cost: 1
   6: l1 -> l3 : length_16^0'=length_16^post6, temp0_18^0'=temp0_18^post6, head_19^0'=head_19^post6, tmp_21^0'=tmp_21^post6, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post6, rcd_47^0'=rcd_47^post6, i_83^0'=i_83^post6, temp0_14^0'=temp0_14^post6, head_15^0'=head_15^post6, result_11^0'=result_11^post6, nondet_12^0'=nondet_12^post6, temp_24^0'=temp_24^post6, i_17^0'=i_17^post6, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post6, rcd_77^0'=rcd_77^post6, (0 == 0 /\ -rcd_77^post6+rcd_77^0 == 0 /\ length_16^0-i_17^0 <= 0 /\ nondet_12^0-nondet_12^post6 == 0 /\ -head_19^0+temp0_18^120 == 0 /\ head_15^post6-result_11^12 == 0 /\ result_dot_nondet_sdv_special_RETURN_VALUE_13^post6 <= 0 /\ rcd_47^0-rcd_47^post6 == 0 /\ result_11^12-temp0_18^120 == 0 /\ result_11^post6-temp0_14^0 == 0 /\ i_83^0-i_83^post6 == 0 /\ temp0_14^0-temp0_14^post6 == 0), cost: 1
   7: l1 -> l2 : length_16^0'=length_16^post7, temp0_18^0'=temp0_18^post7, head_19^0'=head_19^post7, tmp_21^0'=tmp_21^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7, rcd_47^0'=rcd_47^post7, i_83^0'=i_83^post7, temp0_14^0'=temp0_14^post7, head_15^0'=head_15^post7, result_11^0'=result_11^post7, nondet_12^0'=nondet_12^post7, temp_24^0'=temp_24^post7, i_17^0'=i_17^post7, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post7, rcd_77^0'=rcd_77^post7, (0 == 0 /\ -i_83^post7+i_83^0 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+head_19^post7 <= 0 /\ result_11^0-result_11^post7 == 0 /\ temp0_18^0-temp0_18^post7 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-head_19^post7 <= 0 /\ 1-i_17^post7 <= 0 /\ -1+i_17^post7 <= 0 /\ -rcd_77^post7+rcd_77^0 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -temp0_14^post7+temp0_14^0 == 0 /\ -temp_24^0+tmp_21^post7 == 0 /\ -tmp_21^post7+head_19^post7 <= 0 /\ -tmp_21^post7+head_19^post7 == 0 /\ -nondet_12^post7+nondet_12^0 == 0 /\ -1+i_17^post7-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-tmp_21^post7 <= 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ tmp_21^post7-head_19^post7 <= 0 /\ rcd_47^0-rcd_47^post7 == 0 /\ 1-length_16^0 <= 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+tmp_21^post7 <= 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ length_16^0-length_16^post7 == 0 /\ head_15^0-head_15^post7 == 0), cost: 1
   1: l2 -> l3 : length_16^0'=length_16^post1, temp0_18^0'=temp0_18^post1, head_19^0'=head_19^post1, tmp_21^0'=tmp_21^post1, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post1, rcd_47^0'=rcd_47^post1, i_83^0'=i_83^post1, temp0_14^0'=temp0_14^post1, head_15^0'=head_15^post1, result_11^0'=result_11^post1, nondet_12^0'=nondet_12^post1, temp_24^0'=temp_24^post1, i_17^0'=i_17^post1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post1, rcd_77^0'=rcd_77^post1, (0 == 0 /\ -rcd_77^post1+rcd_77^0 == 0 /\ length_16^0-i_17^0 <= 0 /\ -rcd_47^post1+rcd_47^0 == 0 /\ -nondet_12^post1+nondet_12^0 == 0 /\ -temp0_18^10+result_11^10 == 0 /\ 1-result_dot_nondet_sdv_special_RETURN_VALUE_13^post1 <= 0 /\ -1+result_dot_nondet_sdv_special_RETURN_VALUE_13^post1 <= 0 /\ -head_19^0+temp0_18^10 == 0 /\ -temp0_14^post1+temp0_14^0 == 0 /\ -result_11^10+head_15^post1 == 0 /\ result_11^post1-temp0_14^0 == 0 /\ i_83^0-i_83^post1 == 0), cost: 1
   2: l2 -> l4 : length_16^0'=length_16^post2, temp0_18^0'=temp0_18^post2, head_19^0'=head_19^post2, tmp_21^0'=tmp_21^post2, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2, rcd_47^0'=rcd_47^post2, i_83^0'=i_83^post2, temp0_14^0'=temp0_14^post2, head_15^0'=head_15^post2, result_11^0'=result_11^post2, nondet_12^0'=nondet_12^post2, temp_24^0'=temp_24^post2, i_17^0'=i_17^post2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post2, rcd_77^0'=rcd_77^post2, (0 == 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ -2+i_17^post2 <= 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ result_11^0-result_11^post2 == 0 /\ tmp_21^post2-temp_24^0 == 0 /\ -nondet_12^post2+nondet_12^0 == 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ 1-length_16^0+i_17^0 <= 0 /\ temp0_18^0-temp0_18^post2 == 0 /\ -1+i_17^post2-i_17^0 == 0 /\ head_15^0-head_15^post2 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-head_19^post2 <= 0 /\ 2-length_16^0 <= 0 /\ 2-i_17^post2 <= 0 /\ head_19^post2-tmp_21^post2 <= 0 /\ head_19^post2-tmp_21^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+tmp_21^post2 <= 0 /\ -length_16^post2+length_16^0 == 0 /\ i_83^0-i_83^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+head_19^post2 <= 0 /\ -head_19^post2+tmp_21^post2 <= 0 /\ 1-length_16^0 <= 0 /\ -rcd_77^post2+rcd_77^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-tmp_21^post2 <= 0), cost: 1
   3: l4 -> l3 : length_16^0'=length_16^post3, temp0_18^0'=temp0_18^post3, head_19^0'=head_19^post3, tmp_21^0'=tmp_21^post3, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post3, rcd_47^0'=rcd_47^post3, i_83^0'=i_83^post3, temp0_14^0'=temp0_14^post3, head_15^0'=head_15^post3, result_11^0'=result_11^post3, nondet_12^0'=nondet_12^post3, temp_24^0'=temp_24^post3, i_17^0'=i_17^post3, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post3, rcd_77^0'=rcd_77^post3, (0 == 0 /\ -rcd_47^post3+rcd_47^0 == 0 /\ -result_11^11+head_15^post3 == 0 /\ i_83^0-i_83^post3 == 0 /\ -nondet_12^post3+nondet_12^0 == 0 /\ length_16^0-i_17^0 <= 0 /\ result_dot_nondet_sdv_special_RETURN_VALUE_13^post3-i_17^post3 <= 0 /\ -i_17^0 <= 0 /\ -temp0_18^110+result_11^11 == 0 /\ -rcd_77^post3+rcd_77^0 == 0 /\ -temp0_14^0+result_11^post3 == 0 /\ 2-result_dot_nondet_sdv_special_RETURN_VALUE_13^post3 <= 0 /\ temp0_14^0-temp0_14^post3 == 0 /\ -head_19^0+temp0_18^110 == 0 /\ 1-result_dot_nondet_sdv_special_RETURN_VALUE_13^post3 <= 0), cost: 1
   4: l4 -> l5 : length_16^0'=length_16^post4, temp0_18^0'=temp0_18^post4, head_19^0'=head_19^post4, tmp_21^0'=tmp_21^post4, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4, rcd_47^0'=rcd_47^post4, i_83^0'=i_83^post4, temp0_14^0'=temp0_14^post4, head_15^0'=head_15^post4, result_11^0'=result_11^post4, nondet_12^0'=nondet_12^post4, temp_24^0'=temp_24^post4, i_17^0'=i_17^post4, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post4, rcd_77^0'=rcd_77^post4, (0 == 0 /\ length_16^0-length_16^post4 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post4+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ -1-i_83^post4+i_17^post4 <= 0 /\ -rcd_47^post4+rcd_47^0 == 0 /\ -i_17^0 <= 0 /\ -tmp_21^post4+head_19^post4 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -result_11^post4+result_11^0 == 0 /\ tmp_21^post4-temp_24^0 == 0 /\ temp0_18^0-temp0_18^post4 == 0 /\ temp0_14^0-temp0_14^post4 == 0 /\ 1-length_16^0+i_83^post4 <= 0 /\ 1+i_83^post4-i_17^post4 <= 0 /\ nondet_12^0-nondet_12^post4 == 0 /\ -1+i_17^post4-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4 == 0 /\ -head_15^post4+head_15^0 == 0), cost: 1
   5: l5 -> l4 : length_16^0'=length_16^post5, temp0_18^0'=temp0_18^post5, head_19^0'=head_19^post5, tmp_21^0'=tmp_21^post5, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5, rcd_47^0'=rcd_47^post5, i_83^0'=i_83^post5, temp0_14^0'=temp0_14^post5, head_15^0'=head_15^post5, result_11^0'=result_11^post5, nondet_12^0'=nondet_12^post5, temp_24^0'=temp_24^post5, i_17^0'=i_17^post5, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post5, rcd_77^0'=rcd_77^post5, (head_15^0-head_15^post5 == 0 /\ temp_24^0-temp_24^post5 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post5+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ rcd_47^0-rcd_47^post5 == 0 /\ -nondet_12^post5+nondet_12^0 == 0 /\ length_16^0-length_16^post5 == 0 /\ temp0_14^0-temp0_14^post5 == 0 /\ -i_17^post5+i_17^0 == 0 /\ -result_11^post5+result_11^0 == 0 /\ temp0_18^0-temp0_18^post5 == 0 /\ tmp_21^0-tmp_21^post5 == 0 /\ -rcd_77^post5+rcd_77^0 == 0 /\ -i_83^post5+i_83^0 == 0 /\ head_19^0-head_19^post5 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5 == 0), cost: 1
   8: l6 -> l0 : length_16^0'=length_16^post8, temp0_18^0'=temp0_18^post8, head_19^0'=head_19^post8, tmp_21^0'=tmp_21^post8, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8, rcd_47^0'=rcd_47^post8, i_83^0'=i_83^post8, temp0_14^0'=temp0_14^post8, head_15^0'=head_15^post8, result_11^0'=result_11^post8, nondet_12^0'=nondet_12^post8, temp_24^0'=temp_24^post8, i_17^0'=i_17^post8, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post8, rcd_77^0'=rcd_77^post8, (i_17^0-i_17^post8 == 0 /\ head_19^0-head_19^post8 == 0 /\ -rcd_77^post8+rcd_77^0 == 0 /\ -head_15^post8+head_15^0 == 0 /\ length_16^0-length_16^post8 == 0 /\ -temp0_14^post8+temp0_14^0 == 0 /\ -nondet_12^post8+nondet_12^0 == 0 /\ -temp_24^post8+temp_24^0 == 0 /\ -rcd_47^post8+rcd_47^0 == 0 /\ result_11^0-result_11^post8 == 0 /\ i_83^0-i_83^post8 == 0 /\ temp0_18^0-temp0_18^post8 == 0 /\ tmp_21^0-tmp_21^post8 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post8+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l6
   0: l0 -> l1 : length_16^0'=length_16^post0, temp0_18^0'=temp0_18^post0, head_19^0'=head_19^post0, tmp_21^0'=tmp_21^post0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0, rcd_47^0'=rcd_47^post0, i_83^0'=i_83^post0, temp0_14^0'=temp0_14^post0, head_15^0'=head_15^post0, result_11^0'=result_11^post0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post0, i_17^0'=i_17^post0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post0, rcd_77^0'=rcd_77^post0, (0 == 0 /\ result_dot_nondet_sdv_special_RETURN_VALUE_13^post0-length_16^post0 <= 0 /\ -temp0_14^post0+temp0_14^0 == 0 /\ temp0_18^0-temp0_18^post0 == 0 /\ -head_15^post0+head_15^0 == 0 /\ -temp_24^post0+temp_24^0 == 0 /\ -nondet_12^10+result_dot_nondet_sdv_special_RETURN_VALUE_13^post0 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 <= 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 == 0 /\ result_11^0-result_11^post0 == 0 /\ head_19^post0 <= 0 /\ head_19^post0 == 0 /\ tmp_21^0-tmp_21^post0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0 == 0 /\ -rcd_77^post0+rcd_77^0 == 0 /\ -i_17^post0 <= 0 /\ i_17^post0 <= 0 /\ i_17^post0 == 0 /\ i_83^0-i_83^post0 == 0 /\ -rcd_47^post0+rcd_47^0 == 0 /\ -head_19^post0 <= 0), cost: 1
   7: l1 -> l2 : length_16^0'=length_16^post7, temp0_18^0'=temp0_18^post7, head_19^0'=head_19^post7, tmp_21^0'=tmp_21^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7, rcd_47^0'=rcd_47^post7, i_83^0'=i_83^post7, temp0_14^0'=temp0_14^post7, head_15^0'=head_15^post7, result_11^0'=result_11^post7, nondet_12^0'=nondet_12^post7, temp_24^0'=temp_24^post7, i_17^0'=i_17^post7, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post7, rcd_77^0'=rcd_77^post7, (0 == 0 /\ -i_83^post7+i_83^0 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+head_19^post7 <= 0 /\ result_11^0-result_11^post7 == 0 /\ temp0_18^0-temp0_18^post7 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-head_19^post7 <= 0 /\ 1-i_17^post7 <= 0 /\ -1+i_17^post7 <= 0 /\ -rcd_77^post7+rcd_77^0 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -temp0_14^post7+temp0_14^0 == 0 /\ -temp_24^0+tmp_21^post7 == 0 /\ -tmp_21^post7+head_19^post7 <= 0 /\ -tmp_21^post7+head_19^post7 == 0 /\ -nondet_12^post7+nondet_12^0 == 0 /\ -1+i_17^post7-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-tmp_21^post7 <= 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ tmp_21^post7-head_19^post7 <= 0 /\ rcd_47^0-rcd_47^post7 == 0 /\ 1-length_16^0 <= 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+tmp_21^post7 <= 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ length_16^0-length_16^post7 == 0 /\ head_15^0-head_15^post7 == 0), cost: 1
   2: l2 -> l4 : length_16^0'=length_16^post2, temp0_18^0'=temp0_18^post2, head_19^0'=head_19^post2, tmp_21^0'=tmp_21^post2, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2, rcd_47^0'=rcd_47^post2, i_83^0'=i_83^post2, temp0_14^0'=temp0_14^post2, head_15^0'=head_15^post2, result_11^0'=result_11^post2, nondet_12^0'=nondet_12^post2, temp_24^0'=temp_24^post2, i_17^0'=i_17^post2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post2, rcd_77^0'=rcd_77^post2, (0 == 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ -2+i_17^post2 <= 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ result_11^0-result_11^post2 == 0 /\ tmp_21^post2-temp_24^0 == 0 /\ -nondet_12^post2+nondet_12^0 == 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ 1-length_16^0+i_17^0 <= 0 /\ temp0_18^0-temp0_18^post2 == 0 /\ -1+i_17^post2-i_17^0 == 0 /\ head_15^0-head_15^post2 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-head_19^post2 <= 0 /\ 2-length_16^0 <= 0 /\ 2-i_17^post2 <= 0 /\ head_19^post2-tmp_21^post2 <= 0 /\ head_19^post2-tmp_21^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+tmp_21^post2 <= 0 /\ -length_16^post2+length_16^0 == 0 /\ i_83^0-i_83^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+head_19^post2 <= 0 /\ -head_19^post2+tmp_21^post2 <= 0 /\ 1-length_16^0 <= 0 /\ -rcd_77^post2+rcd_77^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-tmp_21^post2 <= 0), cost: 1
   4: l4 -> l5 : length_16^0'=length_16^post4, temp0_18^0'=temp0_18^post4, head_19^0'=head_19^post4, tmp_21^0'=tmp_21^post4, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4, rcd_47^0'=rcd_47^post4, i_83^0'=i_83^post4, temp0_14^0'=temp0_14^post4, head_15^0'=head_15^post4, result_11^0'=result_11^post4, nondet_12^0'=nondet_12^post4, temp_24^0'=temp_24^post4, i_17^0'=i_17^post4, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post4, rcd_77^0'=rcd_77^post4, (0 == 0 /\ length_16^0-length_16^post4 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post4+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ -1-i_83^post4+i_17^post4 <= 0 /\ -rcd_47^post4+rcd_47^0 == 0 /\ -i_17^0 <= 0 /\ -tmp_21^post4+head_19^post4 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -result_11^post4+result_11^0 == 0 /\ tmp_21^post4-temp_24^0 == 0 /\ temp0_18^0-temp0_18^post4 == 0 /\ temp0_14^0-temp0_14^post4 == 0 /\ 1-length_16^0+i_83^post4 <= 0 /\ 1+i_83^post4-i_17^post4 <= 0 /\ nondet_12^0-nondet_12^post4 == 0 /\ -1+i_17^post4-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4 == 0 /\ -head_15^post4+head_15^0 == 0), cost: 1
   5: l5 -> l4 : length_16^0'=length_16^post5, temp0_18^0'=temp0_18^post5, head_19^0'=head_19^post5, tmp_21^0'=tmp_21^post5, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5, rcd_47^0'=rcd_47^post5, i_83^0'=i_83^post5, temp0_14^0'=temp0_14^post5, head_15^0'=head_15^post5, result_11^0'=result_11^post5, nondet_12^0'=nondet_12^post5, temp_24^0'=temp_24^post5, i_17^0'=i_17^post5, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post5, rcd_77^0'=rcd_77^post5, (head_15^0-head_15^post5 == 0 /\ temp_24^0-temp_24^post5 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post5+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ rcd_47^0-rcd_47^post5 == 0 /\ -nondet_12^post5+nondet_12^0 == 0 /\ length_16^0-length_16^post5 == 0 /\ temp0_14^0-temp0_14^post5 == 0 /\ -i_17^post5+i_17^0 == 0 /\ -result_11^post5+result_11^0 == 0 /\ temp0_18^0-temp0_18^post5 == 0 /\ tmp_21^0-tmp_21^post5 == 0 /\ -rcd_77^post5+rcd_77^0 == 0 /\ -i_83^post5+i_83^0 == 0 /\ head_19^0-head_19^post5 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5 == 0), cost: 1
   8: l6 -> l0 : length_16^0'=length_16^post8, temp0_18^0'=temp0_18^post8, head_19^0'=head_19^post8, tmp_21^0'=tmp_21^post8, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8, rcd_47^0'=rcd_47^post8, i_83^0'=i_83^post8, temp0_14^0'=temp0_14^post8, head_15^0'=head_15^post8, result_11^0'=result_11^post8, nondet_12^0'=nondet_12^post8, temp_24^0'=temp_24^post8, i_17^0'=i_17^post8, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post8, rcd_77^0'=rcd_77^post8, (i_17^0-i_17^post8 == 0 /\ head_19^0-head_19^post8 == 0 /\ -rcd_77^post8+rcd_77^0 == 0 /\ -head_15^post8+head_15^0 == 0 /\ length_16^0-length_16^post8 == 0 /\ -temp0_14^post8+temp0_14^0 == 0 /\ -nondet_12^post8+nondet_12^0 == 0 /\ -temp_24^post8+temp_24^0 == 0 /\ -rcd_47^post8+rcd_47^0 == 0 /\ result_11^0-result_11^post8 == 0 /\ i_83^0-i_83^post8 == 0 /\ temp0_18^0-temp0_18^post8 == 0 /\ tmp_21^0-tmp_21^post8 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post8+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : length_16^0'=length_16^post0, temp0_18^0'=temp0_18^post0, head_19^0'=head_19^post0, tmp_21^0'=tmp_21^post0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0, rcd_47^0'=rcd_47^post0, i_83^0'=i_83^post0, temp0_14^0'=temp0_14^post0, head_15^0'=head_15^post0, result_11^0'=result_11^post0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post0, i_17^0'=i_17^post0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post0, rcd_77^0'=rcd_77^post0, (0 == 0 /\ result_dot_nondet_sdv_special_RETURN_VALUE_13^post0-length_16^post0 <= 0 /\ -temp0_14^post0+temp0_14^0 == 0 /\ temp0_18^0-temp0_18^post0 == 0 /\ -head_15^post0+head_15^0 == 0 /\ -temp_24^post0+temp_24^0 == 0 /\ -nondet_12^10+result_dot_nondet_sdv_special_RETURN_VALUE_13^post0 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 <= 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post0+length_16^post0 == 0 /\ result_11^0-result_11^post0 == 0 /\ head_19^post0 <= 0 /\ head_19^post0 == 0 /\ tmp_21^0-tmp_21^post0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post0 == 0 /\ -rcd_77^post0+rcd_77^0 == 0 /\ -i_17^post0 <= 0 /\ i_17^post0 <= 0 /\ i_17^post0 == 0 /\ i_83^0-i_83^post0 == 0 /\ -rcd_47^post0+rcd_47^0 == 0 /\ -head_19^post0 <= 0), cost: 1
New rule:
l0 -> l1 : length_16^0'=nondet_12^10, head_19^0'=0, nondet_12^0'=nondet_12^post0, i_17^0'=0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : length_16^0'=length_16^post2, temp0_18^0'=temp0_18^post2, head_19^0'=head_19^post2, tmp_21^0'=tmp_21^post2, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2, rcd_47^0'=rcd_47^post2, i_83^0'=i_83^post2, temp0_14^0'=temp0_14^post2, head_15^0'=head_15^post2, result_11^0'=result_11^post2, nondet_12^0'=nondet_12^post2, temp_24^0'=temp_24^post2, i_17^0'=i_17^post2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post2, rcd_77^0'=rcd_77^post2, (0 == 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ -2+i_17^post2 <= 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ result_11^0-result_11^post2 == 0 /\ tmp_21^post2-temp_24^0 == 0 /\ -nondet_12^post2+nondet_12^0 == 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post2 <= 0 /\ 1-length_16^0+i_17^0 <= 0 /\ temp0_18^0-temp0_18^post2 == 0 /\ -1+i_17^post2-i_17^0 == 0 /\ head_15^0-head_15^post2 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-head_19^post2 <= 0 /\ 2-length_16^0 <= 0 /\ 2-i_17^post2 <= 0 /\ head_19^post2-tmp_21^post2 <= 0 /\ head_19^post2-tmp_21^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+tmp_21^post2 <= 0 /\ -length_16^post2+length_16^0 == 0 /\ i_83^0-i_83^post2 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2+head_19^post2 <= 0 /\ -head_19^post2+tmp_21^post2 <= 0 /\ 1-length_16^0 <= 0 /\ -rcd_77^post2+rcd_77^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post2-tmp_21^post2 <= 0), cost: 1
New rule:
l2 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, rcd_47^0'=rcd_47^post2, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (-2+length_16^0 >= 0 /\ -1+i_17^0 == 0), cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : length_16^0'=length_16^post4, temp0_18^0'=temp0_18^post4, head_19^0'=head_19^post4, tmp_21^0'=tmp_21^post4, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4, rcd_47^0'=rcd_47^post4, i_83^0'=i_83^post4, temp0_14^0'=temp0_14^post4, head_15^0'=head_15^post4, result_11^0'=result_11^post4, nondet_12^0'=nondet_12^post4, temp_24^0'=temp_24^post4, i_17^0'=i_17^post4, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post4, rcd_77^0'=rcd_77^post4, (0 == 0 /\ length_16^0-length_16^post4 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post4+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ -1-i_83^post4+i_17^post4 <= 0 /\ -rcd_47^post4+rcd_47^0 == 0 /\ -i_17^0 <= 0 /\ -tmp_21^post4+head_19^post4 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -result_11^post4+result_11^0 == 0 /\ tmp_21^post4-temp_24^0 == 0 /\ temp0_18^0-temp0_18^post4 == 0 /\ temp0_14^0-temp0_14^post4 == 0 /\ 1-length_16^0+i_83^post4 <= 0 /\ 1+i_83^post4-i_17^post4 <= 0 /\ nondet_12^0-nondet_12^post4 == 0 /\ -1+i_17^post4-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post4 == 0 /\ -head_15^post4+head_15^0 == 0), cost: 1
New rule:
l4 -> l5 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l5 -> l4 : length_16^0'=length_16^post5, temp0_18^0'=temp0_18^post5, head_19^0'=head_19^post5, tmp_21^0'=tmp_21^post5, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5, rcd_47^0'=rcd_47^post5, i_83^0'=i_83^post5, temp0_14^0'=temp0_14^post5, head_15^0'=head_15^post5, result_11^0'=result_11^post5, nondet_12^0'=nondet_12^post5, temp_24^0'=temp_24^post5, i_17^0'=i_17^post5, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post5, rcd_77^0'=rcd_77^post5, (head_15^0-head_15^post5 == 0 /\ temp_24^0-temp_24^post5 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post5+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0 /\ rcd_47^0-rcd_47^post5 == 0 /\ -nondet_12^post5+nondet_12^0 == 0 /\ length_16^0-length_16^post5 == 0 /\ temp0_14^0-temp0_14^post5 == 0 /\ -i_17^post5+i_17^0 == 0 /\ -result_11^post5+result_11^0 == 0 /\ temp0_18^0-temp0_18^post5 == 0 /\ tmp_21^0-tmp_21^post5 == 0 /\ -rcd_77^post5+rcd_77^0 == 0 /\ -i_83^post5+i_83^0 == 0 /\ head_19^0-head_19^post5 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post5 == 0), cost: 1
New rule:
l5 -> l4 : TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : length_16^0'=length_16^post7, temp0_18^0'=temp0_18^post7, head_19^0'=head_19^post7, tmp_21^0'=tmp_21^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7, rcd_47^0'=rcd_47^post7, i_83^0'=i_83^post7, temp0_14^0'=temp0_14^post7, head_15^0'=head_15^post7, result_11^0'=result_11^post7, nondet_12^0'=nondet_12^post7, temp_24^0'=temp_24^post7, i_17^0'=i_17^post7, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post7, rcd_77^0'=rcd_77^post7, (0 == 0 /\ -i_83^post7+i_83^0 == 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+head_19^post7 <= 0 /\ result_11^0-result_11^post7 == 0 /\ temp0_18^0-temp0_18^post7 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-head_19^post7 <= 0 /\ 1-i_17^post7 <= 0 /\ -1+i_17^post7 <= 0 /\ -rcd_77^post7+rcd_77^0 == 0 /\ 1-length_16^0+i_17^0 <= 0 /\ -temp0_14^post7+temp0_14^0 == 0 /\ -temp_24^0+tmp_21^post7 == 0 /\ -tmp_21^post7+head_19^post7 <= 0 /\ -tmp_21^post7+head_19^post7 == 0 /\ -nondet_12^post7+nondet_12^0 == 0 /\ -1+i_17^post7-i_17^0 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7-tmp_21^post7 <= 0 /\ length_16^0-result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ tmp_21^post7-head_19^post7 <= 0 /\ rcd_47^0-rcd_47^post7 == 0 /\ 1-length_16^0 <= 0 /\ -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post7+tmp_21^post7 <= 0 /\ -length_16^0+result_dot_nondet_sdv_special_RETURN_VALUE_13^post7 <= 0 /\ length_16^0-length_16^post7 == 0 /\ head_15^0-head_15^post7 == 0), cost: 1
New rule:
l1 -> l2 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (i_17^0 == 0 /\ -1+length_16^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l6 -> l0 : length_16^0'=length_16^post8, temp0_18^0'=temp0_18^post8, head_19^0'=head_19^post8, tmp_21^0'=tmp_21^post8, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8, rcd_47^0'=rcd_47^post8, i_83^0'=i_83^post8, temp0_14^0'=temp0_14^post8, head_15^0'=head_15^post8, result_11^0'=result_11^post8, nondet_12^0'=nondet_12^post8, temp_24^0'=temp_24^post8, i_17^0'=i_17^post8, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=result_dot_nondet_sdv_special_RETURN_VALUE_13^post8, rcd_77^0'=rcd_77^post8, (i_17^0-i_17^post8 == 0 /\ head_19^0-head_19^post8 == 0 /\ -rcd_77^post8+rcd_77^0 == 0 /\ -head_15^post8+head_15^0 == 0 /\ length_16^0-length_16^post8 == 0 /\ -temp0_14^post8+temp0_14^0 == 0 /\ -nondet_12^post8+nondet_12^0 == 0 /\ -temp_24^post8+temp_24^0 == 0 /\ -rcd_47^post8+rcd_47^0 == 0 /\ result_11^0-result_11^post8 == 0 /\ i_83^0-i_83^post8 == 0 /\ temp0_18^0-temp0_18^post8 == 0 /\ tmp_21^0-tmp_21^post8 == 0 /\ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0-result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^post8 == 0 /\ -result_dot_nondet_sdv_special_RETURN_VALUE_13^post8+result_dot_nondet_sdv_special_RETURN_VALUE_13^0 == 0), cost: 1
New rule:
l6 -> l0 : TRUE, cost: 1

Simplified rules
Start location: l6
   9: l0 -> l1 : length_16^0'=nondet_12^10, head_19^0'=0, nondet_12^0'=nondet_12^post0, i_17^0'=0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, 0 == 0, cost: 1
  13: l1 -> l2 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (i_17^0 == 0 /\ -1+length_16^0 >= 0), cost: 1
  10: l2 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, rcd_47^0'=rcd_47^post2, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (-2+length_16^0 >= 0 /\ -1+i_17^0 == 0), cost: 1
  11: l4 -> l5 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 1
  12: l5 -> l4 : TRUE, cost: 1
  14: l6 -> l0 : TRUE, cost: 1


Eliminating location l0 by chaining:

Applied chaining
First rule:
l6 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : length_16^0'=nondet_12^10, head_19^0'=0, nondet_12^0'=nondet_12^post0, i_17^0'=0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, 0 == 0, cost: 1
New rule:
l6 -> l1 : length_16^0'=nondet_12^10, head_19^0'=0, nondet_12^0'=nondet_12^post0, i_17^0'=0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 9 14

Eliminating location l1 by chaining:

Applied chaining
First rule:
l6 -> l1 : length_16^0'=nondet_12^10, head_19^0'=0, nondet_12^0'=nondet_12^post0, i_17^0'=0, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, 0 == 0, cost: 2
Second rule:
l1 -> l2 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (i_17^0 == 0 /\ -1+length_16^0 >= 0), cost: 1
New rule:
l6 -> l2 : length_16^0'=nondet_12^10, head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, (0 == 0 /\ -1+nondet_12^10 >= 0), cost: 3

Applied simplification
Original rule:
l6 -> l2 : length_16^0'=nondet_12^10, head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, (0 == 0 /\ -1+nondet_12^10 >= 0), cost: 3
New rule:
l6 -> l2 : length_16^0'=nondet_12^10, head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -1+nondet_12^10 >= 0, cost: 3

Applied deletion
Removed the following rules: 13 15

Eliminating location l2 by chaining:

Applied chaining
First rule:
l6 -> l2 : length_16^0'=nondet_12^10, head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post7, i_17^0'=1, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -1+nondet_12^10 >= 0, cost: 3
Second rule:
l2 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^0, rcd_47^0'=rcd_47^post2, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=length_16^0, (-2+length_16^0 >= 0 /\ -1+i_17^0 == 0), cost: 1
New rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, (0 == 0 /\ -2+nondet_12^10 >= 0 /\ -1+nondet_12^10 >= 0), cost: 4

Applied simplification
Original rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, (0 == 0 /\ -2+nondet_12^10 >= 0 /\ -1+nondet_12^10 >= 0), cost: 4
New rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4

Applied deletion
Removed the following rules: 10 16

Eliminating location l5 by chaining:

Applied chaining
First rule:
l4 -> l5 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 1
Second rule:
l5 -> l4 : TRUE, cost: 1
New rule:
l4 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 11 12

Eliminated locations on linear paths
Start location: l6
  18: l4 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 2
  17: l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4


Applied acceleration
Original rule:
l4 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 2
New rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+n+i_17^0, temp_24^0'=temp_24^post4, i_17^0'=n+i_17^0, rcd_77^0'=rcd_77^post4, (-2+n >= 0 /\ length_16^0-n-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_ccBKcD.txt

Applied instantiation
Original rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+n+i_17^0, temp_24^0'=temp_24^post4, i_17^0'=n+i_17^0, rcd_77^0'=rcd_77^post4, (-2+n >= 0 /\ length_16^0-n-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*n
New rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+length_16^0, temp_24^0'=temp_24^post4, i_17^0'=length_16^0, rcd_77^0'=rcd_77^post4, (0 >= 0 /\ -2+length_16^0-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*length_16^0-2*i_17^0

Applied simplification
Original rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+length_16^0, temp_24^0'=temp_24^post4, i_17^0'=length_16^0, rcd_77^0'=rcd_77^post4, (0 >= 0 /\ -2+length_16^0-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*length_16^0-2*i_17^0
New rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+length_16^0, temp_24^0'=temp_24^post4, i_17^0'=length_16^0, rcd_77^0'=rcd_77^post4, (-2+length_16^0-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*length_16^0-2*i_17^0

Accelerated simple loops
Start location: l6
  18: l4 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 2
  20: l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+length_16^0, temp_24^0'=temp_24^post4, i_17^0'=length_16^0, rcd_77^0'=rcd_77^post4, (-2+length_16^0-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*length_16^0-2*i_17^0
  17: l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4


Applied chaining
First rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4
Second rule:
l4 -> l4 : head_19^0'=temp_24^0, tmp_21^0'=temp_24^0, i_83^0'=i_17^0, temp_24^0'=temp_24^post4, i_17^0'=1+i_17^0, rcd_77^0'=rcd_77^post4, (1-length_16^0+i_17^0 <= 0 /\ i_17^0 >= 0), cost: 2
New rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post2, tmp_21^0'=temp_24^post2, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, i_83^0'=2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post4, i_17^0'=3, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, rcd_77^0'=rcd_77^post4, -3+nondet_12^10 >= 0, cost: 6

Applied chaining
First rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4
Second rule:
l4 -> l4 : head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, i_83^0'=-1+length_16^0, temp_24^0'=temp_24^post4, i_17^0'=length_16^0, rcd_77^0'=rcd_77^post4, (-2+length_16^0-i_17^0 >= 0 /\ i_17^0 >= 0), cost: 2*length_16^0-2*i_17^0
New rule:
l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, i_83^0'=-1+nondet_12^10, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post4, i_17^0'=nondet_12^10, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, rcd_77^0'=rcd_77^post4, -4+nondet_12^10 >= 0, cost: 2*nondet_12^10

Applied deletion
Removed the following rules: 18 20

Chained accelerated rules with incoming rules
Start location: l6
  17: l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post7, tmp_21^0'=temp_24^post7, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post2, i_17^0'=2, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, -2+nondet_12^10 >= 0, cost: 4
  21: l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post2, tmp_21^0'=temp_24^post2, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, i_83^0'=2, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post4, i_17^0'=3, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, rcd_77^0'=rcd_77^post4, -3+nondet_12^10 >= 0, cost: 6
  22: l6 -> l4 : length_16^0'=nondet_12^10, head_19^0'=temp_24^post4, tmp_21^0'=temp_24^post4, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_20^0'=temp_24^post7, rcd_47^0'=rcd_47^post2, i_83^0'=-1+nondet_12^10, nondet_12^0'=nondet_12^post0, temp_24^0'=temp_24^post4, i_17^0'=nondet_12^10, result_dot_nondet_sdv_special_RETURN_VALUE_13^0'=nondet_12^10, rcd_77^0'=rcd_77^post4, -4+nondet_12^10 >= 0, cost: 2*nondet_12^10


Removed unreachable locations and irrelevant leafs
Start location: l6
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0