WORST_CASE(Omega(0),?)

Initial ITS
Start location: l8
   0: l0 -> l1 : cnt_122^0'=cnt_122^post0, lt_40^0'=lt_40^post0, loop_max_13^0'=loop_max_13^post0, nPacketsOld_9^0'=nPacketsOld_9^post0, lt_48^0'=lt_48^post0, ___cil_tmp6_20^0'=___cil_tmp6_20^post0, tmp___1_17^0'=tmp___1_17^post0, lt_21^0'=lt_21^post0, i_12^0'=i_12^post0, lt_45^0'=lt_45^post0, lt_42^0'=lt_42^post0, request_8^0'=request_8^post0, lt_50^0'=lt_50^post0, cnt_198^0'=cnt_198^post0, cnt_117^0'=cnt_117^post0, lt_39^0'=lt_39^post0, loop_count_14^0'=loop_count_14^post0, lt_47^0'=lt_47^post0, lt_44^0'=lt_44^post0, Result_4^0'=Result_4^post0, tmp___0_16^0'=tmp___0_16^post0, lt_90^0'=lt_90^post0, devExt_7^0'=devExt_7^post0, cnt_187^0'=cnt_187^post0, lt_41^0'=lt_41^post0, lt_113^0'=lt_113^post0, nPackets_10^0'=nPackets_10^post0, lt_49^0'=lt_49^post0, ___retres5_19^0'=___retres5_19^post0, tmp___2_18^0'=tmp___2_18^post0, lt_38^0'=lt_38^post0, irp_11^0'=irp_11^post0, lt_46^0'=lt_46^post0, lt_43^0'=lt_43^post0, tmp_15^0'=tmp_15^post0, lt_51^0'=lt_51^post0, cnt_94^0'=cnt_94^post0, (0 == 0 /\ -cnt_187^post0+cnt_187^0 == 0 /\ lt_51^10-tmp_15^post0 == 0 /\ -lt_113^post0+lt_113^0 == 0 /\ -tmp_15^post0+lt_50^post0 == 0 /\ -lt_38^post0+lt_38^0 == 0 /\ -lt_21^post0+lt_21^0 == 0 /\ -lt_43^post0+lt_43^0 == 0 /\ -lt_47^post0+lt_47^0 == 0 /\ cnt_117^0-cnt_117^post0 == 0 /\ -lt_49^post0+lt_49^0 == 0 /\ -lt_46^post0+lt_46^0 == 0 /\ -lt_42^post0+lt_42^0 == 0 /\ lt_48^0-lt_48^post0 == 0 /\ -___retres5_19^post0+___retres5_19^0 == 0 /\ -lt_90^post0+lt_90^0 == 0 /\ lt_45^0-lt_45^post0 == 0 /\ cnt_198^0-cnt_198^post0 == 0 /\ lt_44^0-lt_44^post0 == 0 /\ -cnt_94^post0+cnt_94^0 == 0 /\ cnt_122^0-cnt_122^post0 == 0 /\ lt_40^0-lt_40^post0 == 0 /\ lt_41^0-lt_41^post0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post0 == 0 /\ lt_39^0-lt_39^post0 == 0), cost: 1
   1: l1 -> l3 : cnt_122^0'=cnt_122^post1, lt_40^0'=lt_40^post1, loop_max_13^0'=loop_max_13^post1, nPacketsOld_9^0'=nPacketsOld_9^post1, lt_48^0'=lt_48^post1, ___cil_tmp6_20^0'=___cil_tmp6_20^post1, tmp___1_17^0'=tmp___1_17^post1, lt_21^0'=lt_21^post1, i_12^0'=i_12^post1, lt_45^0'=lt_45^post1, lt_42^0'=lt_42^post1, request_8^0'=request_8^post1, lt_50^0'=lt_50^post1, cnt_198^0'=cnt_198^post1, cnt_117^0'=cnt_117^post1, lt_39^0'=lt_39^post1, loop_count_14^0'=loop_count_14^post1, lt_47^0'=lt_47^post1, lt_44^0'=lt_44^post1, Result_4^0'=Result_4^post1, tmp___0_16^0'=tmp___0_16^post1, lt_90^0'=lt_90^post1, devExt_7^0'=devExt_7^post1, cnt_187^0'=cnt_187^post1, lt_41^0'=lt_41^post1, lt_113^0'=lt_113^post1, nPackets_10^0'=nPackets_10^post1, lt_49^0'=lt_49^post1, ___retres5_19^0'=___retres5_19^post1, tmp___2_18^0'=tmp___2_18^post1, lt_38^0'=lt_38^post1, irp_11^0'=irp_11^post1, lt_46^0'=lt_46^post1, lt_43^0'=lt_43^post1, tmp_15^0'=tmp_15^post1, lt_51^0'=lt_51^post1, cnt_94^0'=cnt_94^post1, (0 == 0 /\ -cnt_94^post1+cnt_94^0 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ tmp___0_16^0-tmp___0_16^post1 == 0 /\ -nPackets_10^post1+nPackets_10^0 == 0 /\ -cnt_117^post1+cnt_117^0 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post1 == 0 /\ -tmp_15^post1+tmp_15^0 == 0 /\ 1+lt_45^10-lt_46^10 <= 0 /\ lt_42^0-lt_42^post1 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post1 == 0 /\ cnt_122^0-cnt_122^post1 == 0 /\ lt_49^10-cnt_94^0 == 0 /\ lt_45^10-cnt_117^0 == 0 /\ -cnt_122^0+lt_46^10 == 0 /\ -lt_113^post1+lt_113^0 == 0 /\ -lt_39^post1+lt_39^0 == 0 /\ lt_48^10-tmp___0_16^0 == 0 /\ tmp___2_18^0-tmp___2_18^post1 == 0 /\ -lt_43^post1+lt_43^0 == 0 /\ -lt_90^post1+lt_90^0 == 0 /\ Result_4^0-Result_4^post1 == 0 /\ devExt_7^0-devExt_7^post1 == 0 /\ lt_51^0-lt_51^post1 == 0 /\ -cnt_187^post1+cnt_187^0 == 0 /\ -loop_max_13^post1+loop_max_13^0 == 0 /\ -lt_38^post1+lt_38^0 == 0 /\ lt_47^10-lt_90^0 == 0 /\ i_12^0-i_12^post1 == 0 /\ -___retres5_19^post1+___retres5_19^0 == 0 /\ loop_count_14^0-loop_count_14^post1 == 0 /\ lt_44^post1-lt_113^0 == 0 /\ -irp_11^post1+irp_11^0 == 0 /\ lt_40^0-lt_40^post1 == 0 /\ request_8^0-request_8^post1 == 0 /\ cnt_198^0-cnt_198^post1 == 0 /\ tmp___1_17^0-tmp___1_17^post1 == 0 /\ -lt_41^post1+lt_41^0 == 0), cost: 1
   8: l1 -> l7 : cnt_122^0'=cnt_122^post8, lt_40^0'=lt_40^post8, loop_max_13^0'=loop_max_13^post8, nPacketsOld_9^0'=nPacketsOld_9^post8, lt_48^0'=lt_48^post8, ___cil_tmp6_20^0'=___cil_tmp6_20^post8, tmp___1_17^0'=tmp___1_17^post8, lt_21^0'=lt_21^post8, i_12^0'=i_12^post8, lt_45^0'=lt_45^post8, lt_42^0'=lt_42^post8, request_8^0'=request_8^post8, lt_50^0'=lt_50^post8, cnt_198^0'=cnt_198^post8, cnt_117^0'=cnt_117^post8, lt_39^0'=lt_39^post8, loop_count_14^0'=loop_count_14^post8, lt_47^0'=lt_47^post8, lt_44^0'=lt_44^post8, Result_4^0'=Result_4^post8, tmp___0_16^0'=tmp___0_16^post8, lt_90^0'=lt_90^post8, devExt_7^0'=devExt_7^post8, cnt_187^0'=cnt_187^post8, lt_41^0'=lt_41^post8, lt_113^0'=lt_113^post8, nPackets_10^0'=nPackets_10^post8, lt_49^0'=lt_49^post8, ___retres5_19^0'=___retres5_19^post8, tmp___2_18^0'=tmp___2_18^post8, lt_38^0'=lt_38^post8, irp_11^0'=irp_11^post8, lt_46^0'=lt_46^post8, lt_43^0'=lt_43^post8, tmp_15^0'=tmp_15^post8, lt_51^0'=lt_51^post8, cnt_94^0'=cnt_94^post8, (0 == 0 /\ -i_12^post8+i_12^0 == 0 /\ -cnt_94^post8+cnt_94^0 == 0 /\ lt_45^110-cnt_117^0 == 0 /\ ___retres5_19^post8 == 0 /\ -lt_51^post8+lt_51^0 == 0 /\ -cnt_122^0+lt_46^110 == 0 /\ -lt_90^0+lt_47^110 == 0 /\ -lt_41^post8+lt_41^0 == 0 /\ lt_39^0-lt_39^post8 == 0 /\ -tmp___0_16^0+lt_48^110 == 0 /\ -lt_45^110+lt_46^110 <= 0 /\ -tmp_15^post8+tmp_15^0 == 0 /\ -lt_43^post8+lt_43^0 == 0 /\ -tmp___0_16^post8+tmp___0_16^0 == 0 /\ -lt_113^post8+lt_113^0 == 0 /\ -lt_38^post8+lt_38^0 == 0 /\ -lt_90^0+lt_21^10 == 0 /\ -loop_count_14^post8+loop_count_14^0 == 0 /\ -lt_42^post8+lt_42^0 == 0 /\ -tmp___2_18^post8+tmp___2_18^0 == 0 /\ cnt_122^0-cnt_122^post8 == 0 /\ -irp_11^post8+irp_11^0 == 0 /\ request_8^0-request_8^post8 == 0 /\ lt_44^0-lt_44^post8 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post8 == 0 /\ loop_max_13^0-loop_max_13^post8 == 0 /\ nPackets_10^0-nPackets_10^post8 == 0 /\ cnt_117^0-cnt_117^post8 == 0 /\ -tmp___1_17^post8+tmp___1_17^0 == 0 /\ lt_40^0-lt_40^post8 == 0 /\ cnt_187^0-cnt_187^post8 == 0 /\ lt_49^110-cnt_94^0 == 0 /\ -devExt_7^post8+devExt_7^0 == 0 /\ Result_4^post8-___cil_tmp6_20^post8 == 0 /\ -___retres5_19^post8+___cil_tmp6_20^post8 == 0 /\ cnt_198^0-cnt_198^post8 == 0 /\ lt_90^0-lt_90^post8 == 0), cost: 1
   2: l3 -> l4 : cnt_122^0'=cnt_122^post2, lt_40^0'=lt_40^post2, loop_max_13^0'=loop_max_13^post2, nPacketsOld_9^0'=nPacketsOld_9^post2, lt_48^0'=lt_48^post2, ___cil_tmp6_20^0'=___cil_tmp6_20^post2, tmp___1_17^0'=tmp___1_17^post2, lt_21^0'=lt_21^post2, i_12^0'=i_12^post2, lt_45^0'=lt_45^post2, lt_42^0'=lt_42^post2, request_8^0'=request_8^post2, lt_50^0'=lt_50^post2, cnt_198^0'=cnt_198^post2, cnt_117^0'=cnt_117^post2, lt_39^0'=lt_39^post2, loop_count_14^0'=loop_count_14^post2, lt_47^0'=lt_47^post2, lt_44^0'=lt_44^post2, Result_4^0'=Result_4^post2, tmp___0_16^0'=tmp___0_16^post2, lt_90^0'=lt_90^post2, devExt_7^0'=devExt_7^post2, cnt_187^0'=cnt_187^post2, lt_41^0'=lt_41^post2, lt_113^0'=lt_113^post2, nPackets_10^0'=nPackets_10^post2, lt_49^0'=lt_49^post2, ___retres5_19^0'=___retres5_19^post2, tmp___2_18^0'=tmp___2_18^post2, lt_38^0'=lt_38^post2, irp_11^0'=irp_11^post2, lt_46^0'=lt_46^post2, lt_43^0'=lt_43^post2, tmp_15^0'=tmp_15^post2, lt_51^0'=lt_51^post2, cnt_94^0'=cnt_94^post2, (-cnt_187^post2+cnt_187^0 == 0 /\ tmp___1_17^0-tmp___1_17^post2 == 0 /\ -lt_44^post2+lt_44^0 == 0 /\ -lt_38^post2+lt_38^0 == 0 /\ 1+lt_44^0 <= 0 /\ -___retres5_19^post2+___retres5_19^0 == 0 /\ tmp___0_16^0-tmp___0_16^post2 == 0 /\ devExt_7^0-devExt_7^post2 == 0 /\ -lt_41^post2+lt_41^0 == 0 /\ -tmp___2_18^post2+tmp___2_18^0 == 0 /\ -irp_11^post2+irp_11^0 == 0 /\ -lt_51^post2+lt_51^0 == 0 /\ -cnt_94^post2+cnt_94^0 == 0 /\ lt_48^0-lt_48^post2 == 0 /\ lt_40^0-lt_40^post2 == 0 /\ -cnt_117^post2+cnt_117^0 == 0 /\ -request_8^post2+request_8^0 == 0 /\ i_12^0-i_12^post2 == 0 /\ -tmp_15^post2+tmp_15^0 == 0 /\ -lt_113^post2+lt_113^0 == 0 /\ -lt_43^post2+lt_43^0 == 0 /\ -lt_49^post2+lt_49^0 == 0 /\ -lt_39^post2+lt_39^0 == 0 /\ lt_50^0-lt_50^post2 == 0 /\ cnt_198^0-cnt_198^post2 == 0 /\ loop_max_13^0-loop_max_13^post2 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ cnt_122^0-cnt_122^post2 == 0 /\ lt_45^0-lt_45^post2 == 0 /\ -nPackets_10^post2+nPackets_10^0 == 0 /\ -nPacketsOld_9^post2+nPacketsOld_9^0 == 0 /\ -lt_42^post2+lt_42^0 == 0 /\ -lt_90^post2+lt_90^0 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -lt_46^post2+lt_46^0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post2 == 0 /\ lt_47^0-lt_47^post2 == 0 /\ -loop_count_14^post2+loop_count_14^0 == 0), cost: 1
   3: l3 -> l4 : cnt_122^0'=cnt_122^post3, lt_40^0'=lt_40^post3, loop_max_13^0'=loop_max_13^post3, nPacketsOld_9^0'=nPacketsOld_9^post3, lt_48^0'=lt_48^post3, ___cil_tmp6_20^0'=___cil_tmp6_20^post3, tmp___1_17^0'=tmp___1_17^post3, lt_21^0'=lt_21^post3, i_12^0'=i_12^post3, lt_45^0'=lt_45^post3, lt_42^0'=lt_42^post3, request_8^0'=request_8^post3, lt_50^0'=lt_50^post3, cnt_198^0'=cnt_198^post3, cnt_117^0'=cnt_117^post3, lt_39^0'=lt_39^post3, loop_count_14^0'=loop_count_14^post3, lt_47^0'=lt_47^post3, lt_44^0'=lt_44^post3, Result_4^0'=Result_4^post3, tmp___0_16^0'=tmp___0_16^post3, lt_90^0'=lt_90^post3, devExt_7^0'=devExt_7^post3, cnt_187^0'=cnt_187^post3, lt_41^0'=lt_41^post3, lt_113^0'=lt_113^post3, nPackets_10^0'=nPackets_10^post3, lt_49^0'=lt_49^post3, ___retres5_19^0'=___retres5_19^post3, tmp___2_18^0'=tmp___2_18^post3, lt_38^0'=lt_38^post3, irp_11^0'=irp_11^post3, lt_46^0'=lt_46^post3, lt_43^0'=lt_43^post3, tmp_15^0'=tmp_15^post3, lt_51^0'=lt_51^post3, cnt_94^0'=cnt_94^post3, (lt_40^0-lt_40^post3 == 0 /\ irp_11^0-irp_11^post3 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post3 == 0 /\ -lt_38^post3+lt_38^0 == 0 /\ tmp___1_17^0-tmp___1_17^post3 == 0 /\ -cnt_94^post3+cnt_94^0 == 0 /\ lt_113^0-lt_113^post3 == 0 /\ loop_count_14^0-loop_count_14^post3 == 0 /\ -lt_45^post3+lt_45^0 == 0 /\ lt_90^0-lt_90^post3 == 0 /\ cnt_187^0-cnt_187^post3 == 0 /\ -tmp___0_16^post3+tmp___0_16^0 == 0 /\ -lt_43^post3+lt_43^0 == 0 /\ -tmp_15^post3+tmp_15^0 == 0 /\ -lt_49^post3+lt_49^0 == 0 /\ lt_21^0-lt_21^post3 == 0 /\ -lt_50^post3+lt_50^0 == 0 /\ -tmp___2_18^post3+tmp___2_18^0 == 0 /\ -___retres5_19^post3+___retres5_19^0 == 0 /\ -lt_47^post3+lt_47^0 == 0 /\ request_8^0-request_8^post3 == 0 /\ cnt_122^0-cnt_122^post3 == 0 /\ lt_48^0-lt_48^post3 == 0 /\ loop_max_13^0-loop_max_13^post3 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post3 == 0 /\ i_12^0-i_12^post3 == 0 /\ -devExt_7^post3+devExt_7^0 == 0 /\ lt_42^0-lt_42^post3 == 0 /\ cnt_117^0-cnt_117^post3 == 0 /\ -nPackets_10^post3+nPackets_10^0 == 0 /\ -lt_51^post3+lt_51^0 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ lt_41^0-lt_41^post3 == 0 /\ lt_46^0-lt_46^post3 == 0 /\ lt_44^0-lt_44^post3 == 0 /\ 1-lt_44^0 <= 0 /\ lt_39^0-lt_39^post3 == 0 /\ -cnt_198^post3+cnt_198^0 == 0), cost: 1
   4: l4 -> l5 : cnt_122^0'=cnt_122^post4, lt_40^0'=lt_40^post4, loop_max_13^0'=loop_max_13^post4, nPacketsOld_9^0'=nPacketsOld_9^post4, lt_48^0'=lt_48^post4, ___cil_tmp6_20^0'=___cil_tmp6_20^post4, tmp___1_17^0'=tmp___1_17^post4, lt_21^0'=lt_21^post4, i_12^0'=i_12^post4, lt_45^0'=lt_45^post4, lt_42^0'=lt_42^post4, request_8^0'=request_8^post4, lt_50^0'=lt_50^post4, cnt_198^0'=cnt_198^post4, cnt_117^0'=cnt_117^post4, lt_39^0'=lt_39^post4, loop_count_14^0'=loop_count_14^post4, lt_47^0'=lt_47^post4, lt_44^0'=lt_44^post4, Result_4^0'=Result_4^post4, tmp___0_16^0'=tmp___0_16^post4, lt_90^0'=lt_90^post4, devExt_7^0'=devExt_7^post4, cnt_187^0'=cnt_187^post4, lt_41^0'=lt_41^post4, lt_113^0'=lt_113^post4, nPackets_10^0'=nPackets_10^post4, lt_49^0'=lt_49^post4, ___retres5_19^0'=___retres5_19^post4, tmp___2_18^0'=tmp___2_18^post4, lt_38^0'=lt_38^post4, irp_11^0'=irp_11^post4, lt_46^0'=lt_46^post4, lt_43^0'=lt_43^post4, tmp_15^0'=tmp_15^post4, lt_51^0'=lt_51^post4, cnt_94^0'=cnt_94^post4, (0 == 0 /\ i_12^0-i_12^post4 == 0 /\ -lt_51^post4+lt_51^0 == 0 /\ -tmp_15^post4+tmp_15^0 == 0 /\ -lt_39^post4+lt_39^0 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post4 == 0 /\ -lt_41^post4+lt_41^0 == 0 /\ devExt_7^0-devExt_7^post4 == 0 /\ -lt_38^post4+lt_38^0 == 0 /\ tmp___1_17^0-tmp___1_17^post4 == 0 /\ lt_43^post4-cnt_187^0 == 0 /\ -cnt_94^post4+cnt_94^0 == 0 /\ ___retres5_19^0-___retres5_19^post4 == 0 /\ cnt_198^0-cnt_198^post4 == 0 /\ -lt_46^post4+lt_46^0 == 0 /\ -loop_count_14^post4+loop_count_14^0 == 0 /\ lt_45^0-lt_45^post4 == 0 /\ -irp_11^post4+irp_11^0 == 0 /\ tmp___0_16^0-tmp___0_16^post4 == 0 /\ lt_50^0-lt_50^post4 == 0 /\ -lt_90^post4+lt_90^0 == 0 /\ -lt_113^post4+lt_113^0 == 0 /\ lt_49^0-lt_49^post4 == 0 /\ lt_48^0-lt_48^post4 == 0 /\ -tmp___2_18^post4+tmp___2_18^0 == 0 /\ lt_40^0-lt_40^post4 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post4 == 0 /\ lt_47^0-lt_47^post4 == 0 /\ -cnt_122^post4+cnt_122^0 == 0 /\ -nPackets_10^post4+nPackets_10^0 == 0 /\ -request_8^post4+request_8^0 == 0 /\ -lt_113^0+lt_42^post4 == 0 /\ -cnt_117^post4+cnt_117^0 == 0 /\ -cnt_187^post4+cnt_187^0 == 0 /\ loop_max_13^0-loop_max_13^post4 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ lt_21^0-lt_21^post4 == 0), cost: 1
   5: l5 -> l6 : cnt_122^0'=cnt_122^post5, lt_40^0'=lt_40^post5, loop_max_13^0'=loop_max_13^post5, nPacketsOld_9^0'=nPacketsOld_9^post5, lt_48^0'=lt_48^post5, ___cil_tmp6_20^0'=___cil_tmp6_20^post5, tmp___1_17^0'=tmp___1_17^post5, lt_21^0'=lt_21^post5, i_12^0'=i_12^post5, lt_45^0'=lt_45^post5, lt_42^0'=lt_42^post5, request_8^0'=request_8^post5, lt_50^0'=lt_50^post5, cnt_198^0'=cnt_198^post5, cnt_117^0'=cnt_117^post5, lt_39^0'=lt_39^post5, loop_count_14^0'=loop_count_14^post5, lt_47^0'=lt_47^post5, lt_44^0'=lt_44^post5, Result_4^0'=Result_4^post5, tmp___0_16^0'=tmp___0_16^post5, lt_90^0'=lt_90^post5, devExt_7^0'=devExt_7^post5, cnt_187^0'=cnt_187^post5, lt_41^0'=lt_41^post5, lt_113^0'=lt_113^post5, nPackets_10^0'=nPackets_10^post5, lt_49^0'=lt_49^post5, ___retres5_19^0'=___retres5_19^post5, tmp___2_18^0'=tmp___2_18^post5, lt_38^0'=lt_38^post5, irp_11^0'=irp_11^post5, lt_46^0'=lt_46^post5, lt_43^0'=lt_43^post5, tmp_15^0'=tmp_15^post5, lt_51^0'=lt_51^post5, cnt_94^0'=cnt_94^post5, (cnt_122^0-cnt_122^post5 == 0 /\ -lt_46^post5+lt_46^0 == 0 /\ lt_39^0-lt_39^post5 == 0 /\ lt_48^0-lt_48^post5 == 0 /\ irp_11^0-irp_11^post5 == 0 /\ loop_max_13^0-loop_max_13^post5 == 0 /\ lt_90^0-lt_90^post5 == 0 /\ lt_45^0-lt_45^post5 == 0 /\ -lt_47^post5+lt_47^0 == 0 /\ -lt_49^post5+lt_49^0 == 0 /\ -lt_113^post5+lt_113^0 == 0 /\ lt_42^0-lt_42^post5 == 0 /\ -lt_50^post5+lt_50^0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post5 == 0 /\ -tmp___0_16^post5+tmp___0_16^0 == 0 /\ -cnt_198^post5+cnt_198^0 == 0 /\ lt_41^0-lt_41^post5 == 0 /\ -lt_38^post5+lt_38^0 == 0 /\ -cnt_94^post5+cnt_94^0 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ lt_40^0-lt_40^post5 == 0 /\ -i_12^post5+i_12^0 == 0 /\ loop_count_14^0-loop_count_14^post5 == 0 /\ lt_44^0-lt_44^post5 == 0 /\ tmp___1_17^0-tmp___1_17^post5 == 0 /\ cnt_117^0-cnt_117^post5 == 0 /\ -nPackets_10^post5+nPackets_10^0 == 0 /\ -cnt_187^post5+cnt_187^0 == 0 /\ -devExt_7^post5+devExt_7^0 == 0 /\ -lt_51^post5+lt_51^0 == 0 /\ -tmp_15^post5+tmp_15^0 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post5 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ 1+lt_43^0 <= 0 /\ -___retres5_19^post5+___retres5_19^0 == 0 /\ -tmp___2_18^post5+tmp___2_18^0 == 0 /\ -lt_43^post5+lt_43^0 == 0 /\ request_8^0-request_8^post5 == 0), cost: 1
   6: l5 -> l6 : cnt_122^0'=cnt_122^post6, lt_40^0'=lt_40^post6, loop_max_13^0'=loop_max_13^post6, nPacketsOld_9^0'=nPacketsOld_9^post6, lt_48^0'=lt_48^post6, ___cil_tmp6_20^0'=___cil_tmp6_20^post6, tmp___1_17^0'=tmp___1_17^post6, lt_21^0'=lt_21^post6, i_12^0'=i_12^post6, lt_45^0'=lt_45^post6, lt_42^0'=lt_42^post6, request_8^0'=request_8^post6, lt_50^0'=lt_50^post6, cnt_198^0'=cnt_198^post6, cnt_117^0'=cnt_117^post6, lt_39^0'=lt_39^post6, loop_count_14^0'=loop_count_14^post6, lt_47^0'=lt_47^post6, lt_44^0'=lt_44^post6, Result_4^0'=Result_4^post6, tmp___0_16^0'=tmp___0_16^post6, lt_90^0'=lt_90^post6, devExt_7^0'=devExt_7^post6, cnt_187^0'=cnt_187^post6, lt_41^0'=lt_41^post6, lt_113^0'=lt_113^post6, nPackets_10^0'=nPackets_10^post6, lt_49^0'=lt_49^post6, ___retres5_19^0'=___retres5_19^post6, tmp___2_18^0'=tmp___2_18^post6, lt_38^0'=lt_38^post6, irp_11^0'=irp_11^post6, lt_46^0'=lt_46^post6, lt_43^0'=lt_43^post6, tmp_15^0'=tmp_15^post6, lt_51^0'=lt_51^post6, cnt_94^0'=cnt_94^post6, (-lt_46^post6+lt_46^0 == 0 /\ lt_42^0-lt_42^post6 == 0 /\ request_8^0-request_8^post6 == 0 /\ -lt_50^post6+lt_50^0 == 0 /\ -lt_90^post6+lt_90^0 == 0 /\ cnt_198^0-cnt_198^post6 == 0 /\ lt_40^0-lt_40^post6 == 0 /\ -___retres5_19^post6+___retres5_19^0 == 0 /\ 1-lt_43^0 <= 0 /\ -lt_47^post6+lt_47^0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post6 == 0 /\ -Result_4^post6+Result_4^0 == 0 /\ lt_44^0-lt_44^post6 == 0 /\ -cnt_94^post6+cnt_94^0 == 0 /\ lt_48^0-lt_48^post6 == 0 /\ -lt_51^post6+lt_51^0 == 0 /\ -cnt_117^post6+cnt_117^0 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ -irp_11^post6+irp_11^0 == 0 /\ -lt_39^post6+lt_39^0 == 0 /\ cnt_187^0-cnt_187^post6 == 0 /\ i_12^0-i_12^post6 == 0 /\ -tmp_15^post6+tmp_15^0 == 0 /\ -lt_45^post6+lt_45^0 == 0 /\ tmp___0_16^0-tmp___0_16^post6 == 0 /\ loop_max_13^0-loop_max_13^post6 == 0 /\ -lt_38^post6+lt_38^0 == 0 /\ loop_count_14^0-loop_count_14^post6 == 0 /\ devExt_7^0-devExt_7^post6 == 0 /\ -lt_113^post6+lt_113^0 == 0 /\ -lt_43^post6+lt_43^0 == 0 /\ tmp___1_17^0-tmp___1_17^post6 == 0 /\ -tmp___2_18^post6+tmp___2_18^0 == 0 /\ -lt_41^post6+lt_41^0 == 0 /\ lt_49^0-lt_49^post6 == 0 /\ cnt_122^0-cnt_122^post6 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post6 == 0 /\ -nPackets_10^post6+nPackets_10^0 == 0), cost: 1
   7: l6 -> l2 : cnt_122^0'=cnt_122^post7, lt_40^0'=lt_40^post7, loop_max_13^0'=loop_max_13^post7, nPacketsOld_9^0'=nPacketsOld_9^post7, lt_48^0'=lt_48^post7, ___cil_tmp6_20^0'=___cil_tmp6_20^post7, tmp___1_17^0'=tmp___1_17^post7, lt_21^0'=lt_21^post7, i_12^0'=i_12^post7, lt_45^0'=lt_45^post7, lt_42^0'=lt_42^post7, request_8^0'=request_8^post7, lt_50^0'=lt_50^post7, cnt_198^0'=cnt_198^post7, cnt_117^0'=cnt_117^post7, lt_39^0'=lt_39^post7, loop_count_14^0'=loop_count_14^post7, lt_47^0'=lt_47^post7, lt_44^0'=lt_44^post7, Result_4^0'=Result_4^post7, tmp___0_16^0'=tmp___0_16^post7, lt_90^0'=lt_90^post7, devExt_7^0'=devExt_7^post7, cnt_187^0'=cnt_187^post7, lt_41^0'=lt_41^post7, lt_113^0'=lt_113^post7, nPackets_10^0'=nPackets_10^post7, lt_49^0'=lt_49^post7, ___retres5_19^0'=___retres5_19^post7, tmp___2_18^0'=tmp___2_18^post7, lt_38^0'=lt_38^post7, irp_11^0'=irp_11^post7, lt_46^0'=lt_46^post7, lt_43^0'=lt_43^post7, tmp_15^0'=tmp_15^post7, lt_51^0'=lt_51^post7, cnt_94^0'=cnt_94^post7, (0 == 0 /\ cnt_117^0-cnt_117^post7 == 0 /\ -lt_46^post7+lt_46^0 == 0 /\ tmp___1_17^0-tmp___1_17^post7 == 0 /\ -tmp_15^post7+tmp_15^0 == 0 /\ -nPackets_10^post7+nPackets_10^0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post7 == 0 /\ -irp_11^post7+irp_11^0 == 0 /\ -devExt_7^post7+devExt_7^0 == 0 /\ -request_8^post7+request_8^0 == 0 /\ -lt_51^post7+lt_51^0 == 0 /\ lt_45^0-lt_45^post7 == 0 /\ cnt_187^0-cnt_187^post7 == 0 /\ lt_48^0-lt_48^post7 == 0 /\ -lt_90^0+lt_41^10 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post7 == 0 /\ lt_47^0-lt_47^post7 == 0 /\ loop_count_14^0-loop_count_14^post7 == 0 /\ -tmp___2_18^post7+tmp___2_18^0 == 0 /\ lt_90^0-lt_90^post7 == 0 /\ -cnt_94^post7+cnt_94^0 == 0 /\ lt_39^10-lt_113^0 == 0 /\ -cnt_198^post7+cnt_198^0 == 0 /\ lt_50^0-lt_50^post7 == 0 /\ -cnt_198^0+lt_40^10 == 0 /\ lt_21^0-lt_21^post7 == 0 /\ -lt_49^post7+lt_49^0 == 0 /\ cnt_122^0-cnt_122^post7 == 0 /\ lt_44^0-lt_44^post7 == 0 /\ -___retres5_19^post7+___retres5_19^0 == 0 /\ -tmp___0_16^post7+tmp___0_16^0 == 0 /\ -lt_90^0+lt_38^post7 == 0 /\ i_12^0-i_12^post7 == 0 /\ lt_113^0-lt_113^post7 == 0 /\ loop_max_13^0-loop_max_13^post7 == 0), cost: 1
   9: l8 -> l0 : cnt_122^0'=cnt_122^post9, lt_40^0'=lt_40^post9, loop_max_13^0'=loop_max_13^post9, nPacketsOld_9^0'=nPacketsOld_9^post9, lt_48^0'=lt_48^post9, ___cil_tmp6_20^0'=___cil_tmp6_20^post9, tmp___1_17^0'=tmp___1_17^post9, lt_21^0'=lt_21^post9, i_12^0'=i_12^post9, lt_45^0'=lt_45^post9, lt_42^0'=lt_42^post9, request_8^0'=request_8^post9, lt_50^0'=lt_50^post9, cnt_198^0'=cnt_198^post9, cnt_117^0'=cnt_117^post9, lt_39^0'=lt_39^post9, loop_count_14^0'=loop_count_14^post9, lt_47^0'=lt_47^post9, lt_44^0'=lt_44^post9, Result_4^0'=Result_4^post9, tmp___0_16^0'=tmp___0_16^post9, lt_90^0'=lt_90^post9, devExt_7^0'=devExt_7^post9, cnt_187^0'=cnt_187^post9, lt_41^0'=lt_41^post9, lt_113^0'=lt_113^post9, nPackets_10^0'=nPackets_10^post9, lt_49^0'=lt_49^post9, ___retres5_19^0'=___retres5_19^post9, tmp___2_18^0'=tmp___2_18^post9, lt_38^0'=lt_38^post9, irp_11^0'=irp_11^post9, lt_46^0'=lt_46^post9, lt_43^0'=lt_43^post9, tmp_15^0'=tmp_15^post9, lt_51^0'=lt_51^post9, cnt_94^0'=cnt_94^post9, (-lt_39^post9+lt_39^0 == 0 /\ i_12^0-i_12^post9 == 0 /\ lt_48^0-lt_48^post9 == 0 /\ -lt_38^post9+lt_38^0 == 0 /\ loop_max_13^0-loop_max_13^post9 == 0 /\ -tmp___2_18^post9+tmp___2_18^0 == 0 /\ -lt_41^post9+lt_41^0 == 0 /\ lt_42^0-lt_42^post9 == 0 /\ tmp___1_17^0-tmp___1_17^post9 == 0 /\ lt_44^0-lt_44^post9 == 0 /\ -cnt_94^post9+cnt_94^0 == 0 /\ -irp_11^post9+irp_11^0 == 0 /\ -___retres5_19^post9+___retres5_19^0 == 0 /\ cnt_198^0-cnt_198^post9 == 0 /\ -lt_51^post9+lt_51^0 == 0 /\ -lt_90^post9+lt_90^0 == 0 /\ cnt_122^0-cnt_122^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ -tmp_15^post9+tmp_15^0 == 0 /\ -loop_count_14^post9+loop_count_14^0 == 0 /\ lt_45^0-lt_45^post9 == 0 /\ nPacketsOld_9^0-nPacketsOld_9^post9 == 0 /\ -lt_113^post9+lt_113^0 == 0 /\ -lt_46^post9+lt_46^0 == 0 /\ devExt_7^0-devExt_7^post9 == 0 /\ lt_49^0-lt_49^post9 == 0 /\ lt_40^0-lt_40^post9 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post9 == 0 /\ tmp___0_16^0-tmp___0_16^post9 == 0 /\ -lt_43^post9+lt_43^0 == 0 /\ lt_47^0-lt_47^post9 == 0 /\ -nPackets_10^post9+nPackets_10^0 == 0 /\ cnt_187^0-cnt_187^post9 == 0 /\ lt_50^0-lt_50^post9 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ -request_8^post9+request_8^0 == 0 /\ -cnt_117^post9+cnt_117^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l8
  <empty>


Computing asymptotic complexity

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

Solved cost: 0
Rule cost:   0