unknown

Initial ITS

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

Chained Linear Paths

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

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l8 -> l0 : ___cil_tmp6_20^0'=___cil_tmp6_20^post10, ___retres5_19^0'=___retres5_19^post10, cnt_117^0'=cnt_117^post10, cnt_122^0'=cnt_122^post10, cnt_187^0'=cnt_187^post10, cnt_198^0'=cnt_198^post10, cnt_94^0'=cnt_94^post10, devext_7^0'=devext_7^post10, i_12^0'=i_12^post10, irp_11^0'=irp_11^post10, loop_count_14^0'=loop_count_14^post10, loop_max_13^0'=loop_max_13^post10, lt_113^0'=lt_113^post10, lt_21^0'=lt_21^post10, lt_38^0'=lt_38^post10, lt_39^0'=lt_39^post10, lt_40^0'=lt_40^post10, lt_41^0'=lt_41^post10, lt_42^0'=lt_42^post10, lt_43^0'=lt_43^post10, lt_44^0'=lt_44^post10, lt_45^0'=lt_45^post10, lt_46^0'=lt_46^post10, lt_47^0'=lt_47^post10, lt_48^0'=lt_48^post10, lt_49^0'=lt_49^post10, lt_50^0'=lt_50^post10, lt_51^0'=lt_51^post10, lt_90^0'=lt_90^post10, npackets_10^0'=npackets_10^post10, npacketsold_9^0'=npacketsold_9^post10, request_8^0'=request_8^post10, result_4^0'=result_4^post10, tmp_15^0'=tmp_15^post10, tmp___0_16^0'=tmp___0_16^post10, tmp___1_17^0'=tmp___1_17^post10, tmp___2_18^0'=tmp___2_18^post10, (tmp_15^0-tmp_15^post10 == 0 /\ cnt_94^0-cnt_94^post10 == 0 /\ -loop_count_14^post10+loop_count_14^0 == 0 /\ -devext_7^post10+devext_7^0 == 0 /\ -request_8^post10+request_8^0 == 0 /\ cnt_187^0-cnt_187^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ npackets_10^0-npackets_10^post10 == 0 /\ -tmp___1_17^post10+tmp___1_17^0 == 0 /\ lt_45^0-lt_45^post10 == 0 /\ npacketsold_9^0-npacketsold_9^post10 == 0 /\ lt_50^0-lt_50^post10 == 0 /\ -cnt_117^post10+cnt_117^0 == 0 /\ lt_46^0-lt_46^post10 == 0 /\ -___cil_tmp6_20^post10+___cil_tmp6_20^0 == 0 /\ i_12^0-i_12^post10 == 0 /\ lt_51^0-lt_51^post10 == 0 /\ lt_41^0-lt_41^post10 == 0 /\ -lt_44^post10+lt_44^0 == 0 /\ -lt_40^post10+lt_40^0 == 0 /\ lt_42^0-lt_42^post10 == 0 /\ irp_11^0-irp_11^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -lt_39^post10+lt_39^0 == 0 /\ -lt_47^post10+lt_47^0 == 0 /\ lt_48^0-lt_48^post10 == 0 /\ -tmp___2_18^post10+tmp___2_18^0 == 0 /\ loop_max_13^0-loop_max_13^post10 == 0 /\ ___retres5_19^0-___retres5_19^post10 == 0 /\ -lt_113^post10+lt_113^0 == 0 /\ -lt_43^post10+lt_43^0 == 0 /\ -lt_90^post10+lt_90^0 == 0 /\ cnt_122^0-cnt_122^post10 == 0 /\ -cnt_198^post10+cnt_198^0 == 0 /\ result_4^0-result_4^post10 == 0 /\ tmp___0_16^0-tmp___0_16^post10 == 0 /\ lt_49^0-lt_49^post10 == 0), cost: 1
	Second rule:
	l0 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^post1, ___retres5_19^0'=___retres5_19^post1, cnt_117^0'=cnt_117^post1, cnt_122^0'=cnt_122^post1, cnt_187^0'=cnt_187^post1, cnt_198^0'=cnt_198^post1, cnt_94^0'=cnt_94^post1, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^post1, lt_21^0'=lt_21^post1, lt_38^0'=lt_38^post1, lt_39^0'=lt_39^post1, lt_40^0'=lt_40^post1, lt_41^0'=lt_41^post1, lt_42^0'=lt_42^post1, lt_43^0'=lt_43^post1, lt_44^0'=lt_44^post1, lt_45^0'=lt_45^post1, lt_46^0'=lt_46^post1, lt_47^0'=lt_47^post1, lt_48^0'=lt_48^post1, lt_49^0'=lt_49^post1, lt_50^0'=lt_50^post1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^post1, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=tmp_15^post1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, (0 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ lt_50^post1-tmp_15^post1 == 0 /\ -___cil_tmp6_20^post1+___cil_tmp6_20^0 == 0 /\ -lt_45^post1+lt_45^0 == 0 /\ lt_46^0-lt_46^post1 == 0 /\ -lt_47^post1+lt_47^0 == 0 /\ -lt_90^post1+lt_90^0 == 0 /\ cnt_187^0-cnt_187^post1 == 0 /\ -lt_38^post1+lt_38^0 == 0 /\ -lt_113^post1+lt_113^0 == 0 /\ cnt_122^0-cnt_122^post1 == 0 /\ -___retres5_19^post1+___retres5_19^0 == 0 /\ lt_43^0-lt_43^post1 == 0 /\ -cnt_198^post1+cnt_198^0 == 0 /\ lt_49^0-lt_49^post1 == 0 /\ lt_40^0-lt_40^post1 == 0 /\ -cnt_117^post1+cnt_117^0 == 0 /\ lt_51^1-tmp_15^post1 == 0 /\ -lt_42^post1+lt_42^0 == 0 /\ -lt_48^post1+lt_48^0 == 0 /\ -lt_39^post1+lt_39^0 == 0 /\ lt_41^0-lt_41^post1 == 0 /\ cnt_94^0-cnt_94^post1 == 0 /\ -lt_44^post1+lt_44^0 == 0), cost: 1
	New rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^post1, ___retres5_19^0'=___retres5_19^post1, cnt_117^0'=cnt_117^post1, cnt_122^0'=cnt_122^post1, cnt_187^0'=cnt_187^post1, cnt_198^0'=cnt_198^post1, cnt_94^0'=cnt_94^post1, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^post1, lt_21^0'=lt_21^post1, lt_38^0'=lt_38^post1, lt_39^0'=lt_39^post1, lt_40^0'=lt_40^post1, lt_41^0'=lt_41^post1, lt_42^0'=lt_42^post1, lt_43^0'=lt_43^post1, lt_44^0'=lt_44^post1, lt_45^0'=lt_45^post1, lt_46^0'=lt_46^post1, lt_47^0'=lt_47^post1, lt_48^0'=lt_48^post1, lt_49^0'=lt_49^post1, lt_50^0'=lt_50^post1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^post1, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=tmp_15^post1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, (0 == 0 /\ tmp_15^0-tmp_15^post10 == 0 /\ -cnt_198^post1+cnt_198^post10 == 0 /\ lt_47^post10-lt_47^post1 == 0 /\ cnt_94^0-cnt_94^post10 == 0 /\ -lt_48^post1+lt_48^post10 == 0 /\ -loop_count_14^post10+loop_count_14^0 == 0 /\ -devext_7^post10+devext_7^0 == 0 /\ -request_8^post10+request_8^0 == 0 /\ -cnt_117^post1+cnt_117^post10 == 0 /\ cnt_187^0-cnt_187^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ -lt_113^post1+lt_113^post10 == 0 /\ -lt_45^post1+lt_45^post10 == 0 /\ lt_50^post1-tmp_15^post1 == 0 /\ npackets_10^0-npackets_10^post10 == 0 /\ -tmp___1_17^post10+tmp___1_17^0 == 0 /\ lt_41^post10-lt_41^post1 == 0 /\ lt_40^post10-lt_40^post1 == 0 /\ lt_45^0-lt_45^post10 == 0 /\ -cnt_122^post1+cnt_122^post10 == 0 /\ -lt_46^post1+lt_46^post10 == 0 /\ npacketsold_9^0-npacketsold_9^post10 == 0 /\ lt_50^0-lt_50^post10 == 0 /\ -cnt_117^post10+cnt_117^0 == 0 /\ lt_90^post10-lt_90^post1 == 0 /\ lt_46^0-lt_46^post10 == 0 /\ -___cil_tmp6_20^post10+___cil_tmp6_20^0 == 0 /\ ___cil_tmp6_20^post10-___cil_tmp6_20^post1 == 0 /\ i_12^0-i_12^post10 == 0 /\ -___retres5_19^post1+___retres5_19^post10 == 0 /\ lt_51^0-lt_51^post10 == 0 /\ lt_41^0-lt_41^post10 == 0 /\ lt_43^post10-lt_43^post1 == 0 /\ -lt_44^post10+lt_44^0 == 0 /\ -lt_40^post10+lt_40^0 == 0 /\ lt_42^0-lt_42^post10 == 0 /\ irp_11^0-irp_11^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -lt_39^post10+lt_39^0 == 0 /\ -lt_47^post10+lt_47^0 == 0 /\ cnt_187^post10-cnt_187^post1 == 0 /\ lt_44^post10-lt_44^post1 == 0 /\ lt_48^0-lt_48^post10 == 0 /\ -lt_49^post1+lt_49^post10 == 0 /\ -cnt_94^post1+cnt_94^post10 == 0 /\ -tmp___2_18^post10+tmp___2_18^0 == 0 /\ loop_max_13^0-loop_max_13^post10 == 0 /\ ___retres5_19^0-___retres5_19^post10 == 0 /\ -lt_113^post10+lt_113^0 == 0 /\ -lt_43^post10+lt_43^0 == 0 /\ lt_21^post10-lt_21^post1 == 0 /\ lt_51^1-tmp_15^post1 == 0 /\ -lt_90^post10+lt_90^0 == 0 /\ -lt_39^post1+lt_39^post10 == 0 /\ cnt_122^0-cnt_122^post10 == 0 /\ -cnt_198^post10+cnt_198^0 == 0 /\ -lt_42^post1+lt_42^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ tmp___0_16^0-tmp___0_16^post10 == 0 /\ -lt_38^post1+lt_38^post10 == 0 /\ lt_49^0-lt_49^post10 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 9

Simplified Transitions

Start location: l8
Program variables: ___cil_tmp6_20^0 ___retres5_19^0 cnt_117^0 cnt_122^0 cnt_187^0 devext_7^0 i_12^0 irp_11^0 loop_count_14^0 loop_max_13^0 lt_113^0 lt_21^0 lt_38^0 lt_39^0 lt_40^0 lt_41^0 lt_42^0 lt_43^0 lt_44^0 lt_45^0 lt_46^0 lt_47^0 lt_48^0 lt_49^0 lt_50^0 lt_51^0 lt_90^0 npackets_10^0 npacketsold_9^0 request_8^0 result_4^0 tmp_15^0 tmp___0_16^0 tmp___1_17^0 tmp___2_18^0
  11: l1 -> l3 : lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, 1-cnt_122^0+cnt_117^0 <= 0, cost: 1
  18: l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, lt_21^0'=lt_21^post9, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, result_4^0'=0, cnt_122^0-cnt_117^0 <= 0, cost: 1
  12: l3 -> l4 : 1+lt_44^0 <= 0, cost: 1
  13: l3 -> l4 : 1-lt_44^0 <= 0, cost: 1
  14: l4 -> l5 : lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, T, cost: 1
  15: l5 -> l6 : 1+lt_43^0 <= 0, cost: 1
  16: l5 -> l6 : 1-lt_43^0 <= 0, cost: 1
  17: l6 -> l2 : lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, result_4^0'=result_4^post8, T, cost: 1
  19: l8 -> l1 : devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, T, cost: 1

	Propagated Equalities

	Original rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^post2, ___retres5_19^0'=___retres5_19^post2, cnt_117^0'=cnt_117^post2, cnt_122^0'=cnt_122^post2, cnt_187^0'=cnt_187^post2, cnt_198^0'=cnt_198^post2, cnt_94^0'=cnt_94^post2, devext_7^0'=devext_7^post2, i_12^0'=i_12^post2, irp_11^0'=irp_11^post2, loop_count_14^0'=loop_count_14^post2, loop_max_13^0'=loop_max_13^post2, lt_113^0'=lt_113^post2, lt_21^0'=lt_21^post2, lt_38^0'=lt_38^post2, lt_39^0'=lt_39^post2, lt_40^0'=lt_40^post2, lt_41^0'=lt_41^post2, lt_42^0'=lt_42^post2, lt_43^0'=lt_43^post2, lt_44^0'=lt_44^post2, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^post2, lt_90^0'=lt_90^post2, npackets_10^0'=npackets_10^post2, npacketsold_9^0'=npacketsold_9^post2, request_8^0'=request_8^post2, result_4^0'=result_4^post2, tmp_15^0'=tmp_15^post2, tmp___0_16^0'=tmp___0_16^post2, tmp___1_17^0'=tmp___1_17^post2, tmp___2_18^0'=tmp___2_18^post2, (0 == 0 /\ cnt_122^0-cnt_122^post2 == 0 /\ -devext_7^post2+devext_7^0 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ -lt_39^post2+lt_39^0 == 0 /\ lt_90^0-lt_90^post2 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ -lt_42^post2+lt_42^0 == 0 /\ npacketsold_9^0-npacketsold_9^post2 == 0 /\ -lt_113^post2+lt_113^0 == 0 /\ tmp___1_17^0-tmp___1_17^post2 == 0 /\ lt_40^0-lt_40^post2 == 0 /\ lt_44^post2-lt_113^0 == 0 /\ tmp___0_16^0-tmp___0_16^post2 == 0 /\ lt_38^0-lt_38^post2 == 0 /\ loop_max_13^0-loop_max_13^post2 == 0 /\ -lt_51^post2+lt_51^0 == 0 /\ cnt_187^0-cnt_187^post2 == 0 /\ -cnt_198^post2+cnt_198^0 == 0 /\ i_12^0-i_12^post2 == 0 /\ -request_8^post2+request_8^0 == 0 /\ -___retres5_19^post2+___retres5_19^0 == 0 /\ -___cil_tmp6_20^post2+___cil_tmp6_20^0 == 0 /\ -loop_count_14^post2+loop_count_14^0 == 0 /\ -result_4^post2+result_4^0 == 0 /\ -npackets_10^post2+npackets_10^0 == 0 /\ irp_11^0-irp_11^post2 == 0 /\ lt_43^0-lt_43^post2 == 0 /\ cnt_94^0-cnt_94^post2 == 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ lt_41^0-lt_41^post2 == 0 /\ -tmp___2_18^post2+tmp___2_18^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ lt_47^1-lt_90^0 == 0 /\ tmp_15^0-tmp_15^post2 == 0 /\ -cnt_117^post2+cnt_117^0 == 0 /\ 1+lt_45^1-lt_46^1 <= 0), cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ lt_47^1-lt_90^0 == 0 /\ 1+lt_45^1-lt_46^1 <= 0), cost: 1
	
		propagated equality cnt_122^post2 = cnt_122^0
		
		propagated equality devext_7^post2 = devext_7^0
		
		propagated equality lt_21^post2 = lt_21^0
		
		propagated equality lt_39^post2 = lt_39^0
		
		propagated equality lt_90^post2 = lt_90^0
		
		propagated equality lt_42^post2 = lt_42^0
		
		propagated equality npacketsold_9^post2 = npacketsold_9^0
		
		propagated equality lt_113^post2 = lt_113^0
		
		propagated equality tmp___1_17^post2 = tmp___1_17^0
		
		propagated equality lt_40^post2 = lt_40^0
		
		propagated equality lt_44^post2 = lt_113^0
		
		propagated equality tmp___0_16^post2 = tmp___0_16^0
		
		propagated equality lt_38^post2 = lt_38^0
		
		propagated equality loop_max_13^post2 = loop_max_13^0
		
		propagated equality lt_51^post2 = lt_51^0
		
		propagated equality cnt_187^post2 = cnt_187^0
		
		propagated equality cnt_198^post2 = cnt_198^0
		
		propagated equality i_12^post2 = i_12^0
		
		propagated equality request_8^post2 = request_8^0
		
		propagated equality ___retres5_19^post2 = ___retres5_19^0
		
		propagated equality ___cil_tmp6_20^post2 = ___cil_tmp6_20^0
		
		propagated equality loop_count_14^post2 = loop_count_14^0
		
		propagated equality result_4^post2 = result_4^0
		
		propagated equality npackets_10^post2 = npackets_10^0
		
		propagated equality irp_11^post2 = irp_11^0
		
		propagated equality lt_43^post2 = lt_43^0
		
		propagated equality cnt_94^post2 = cnt_94^0
		
		propagated equality lt_41^post2 = lt_41^0
		
		propagated equality tmp___2_18^post2 = tmp___2_18^0
		
		propagated equality tmp_15^post2 = tmp_15^0
		
		propagated equality cnt_117^post2 = cnt_117^0
		
	Propagated Equalities

	Original rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ lt_47^1-lt_90^0 == 0 /\ 1+lt_45^1-lt_46^1 <= 0), cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-cnt_122^0+cnt_117^0 <= 0), cost: 1
	
		propagated equality lt_49^1 = cnt_94^0
		
		propagated equality lt_46^1 = cnt_122^0
		
		propagated equality lt_45^1 = cnt_117^0
		
		propagated equality lt_48^1 = tmp___0_16^0
		
		propagated equality lt_47^1 = lt_90^0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-cnt_122^0+cnt_117^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-cnt_122^0+cnt_117^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-cnt_122^0+cnt_117^0 <= 0, cost: 1
	New rule:
	l1 -> l3 : lt_44^0'=lt_113^0, lt_45^0'=lt_45^post2, lt_46^0'=lt_46^post2, lt_47^0'=lt_47^post2, lt_48^0'=lt_48^post2, lt_49^0'=lt_49^post2, lt_50^0'=lt_50^post2, 1-cnt_122^0+cnt_117^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^post3, ___retres5_19^0'=___retres5_19^post3, cnt_117^0'=cnt_117^post3, cnt_122^0'=cnt_122^post3, cnt_187^0'=cnt_187^post3, cnt_198^0'=cnt_198^post3, cnt_94^0'=cnt_94^post3, devext_7^0'=devext_7^post3, i_12^0'=i_12^post3, irp_11^0'=irp_11^post3, loop_count_14^0'=loop_count_14^post3, loop_max_13^0'=loop_max_13^post3, lt_113^0'=lt_113^post3, lt_21^0'=lt_21^post3, lt_38^0'=lt_38^post3, lt_39^0'=lt_39^post3, lt_40^0'=lt_40^post3, lt_41^0'=lt_41^post3, lt_42^0'=lt_42^post3, lt_43^0'=lt_43^post3, lt_44^0'=lt_44^post3, lt_45^0'=lt_45^post3, lt_46^0'=lt_46^post3, lt_47^0'=lt_47^post3, lt_48^0'=lt_48^post3, lt_49^0'=lt_49^post3, lt_50^0'=lt_50^post3, lt_51^0'=lt_51^post3, lt_90^0'=lt_90^post3, npackets_10^0'=npackets_10^post3, npacketsold_9^0'=npacketsold_9^post3, request_8^0'=request_8^post3, result_4^0'=result_4^post3, tmp_15^0'=tmp_15^post3, tmp___0_16^0'=tmp___0_16^post3, tmp___1_17^0'=tmp___1_17^post3, tmp___2_18^0'=tmp___2_18^post3, (loop_max_13^0-loop_max_13^post3 == 0 /\ -___cil_tmp6_20^post3+___cil_tmp6_20^0 == 0 /\ -lt_45^post3+lt_45^0 == 0 /\ -lt_47^post3+lt_47^0 == 0 /\ lt_41^0-lt_41^post3 == 0 /\ 1+lt_44^0 <= 0 /\ lt_46^0-lt_46^post3 == 0 /\ lt_38^0-lt_38^post3 == 0 /\ npacketsold_9^0-npacketsold_9^post3 == 0 /\ lt_50^0-lt_50^post3 == 0 /\ -lt_113^post3+lt_113^0 == 0 /\ -lt_40^post3+lt_40^0 == 0 /\ lt_48^0-lt_48^post3 == 0 /\ -cnt_198^post3+cnt_198^0 == 0 /\ -cnt_122^post3+cnt_122^0 == 0 /\ lt_43^0-lt_43^post3 == 0 /\ -cnt_117^post3+cnt_117^0 == 0 /\ i_12^0-i_12^post3 == 0 /\ lt_49^0-lt_49^post3 == 0 /\ tmp___1_17^0-tmp___1_17^post3 == 0 /\ -lt_90^post3+lt_90^0 == 0 /\ npackets_10^0-npackets_10^post3 == 0 /\ -devext_7^post3+devext_7^0 == 0 /\ -cnt_94^post3+cnt_94^0 == 0 /\ -tmp___2_18^post3+tmp___2_18^0 == 0 /\ -request_8^post3+request_8^0 == 0 /\ tmp___0_16^0-tmp___0_16^post3 == 0 /\ ___retres5_19^0-___retres5_19^post3 == 0 /\ result_4^0-result_4^post3 == 0 /\ cnt_187^0-cnt_187^post3 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -lt_39^post3+lt_39^0 == 0 /\ tmp_15^0-tmp_15^post3 == 0 /\ -lt_44^post3+lt_44^0 == 0 /\ -loop_count_14^post3+loop_count_14^0 == 0 /\ -lt_42^post3+lt_42^0 == 0 /\ -irp_11^post3+irp_11^0 == 0 /\ lt_51^0-lt_51^post3 == 0), cost: 1
	New rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1+lt_44^0 <= 0), cost: 1
	
		propagated equality loop_max_13^post3 = loop_max_13^0
		
		propagated equality ___cil_tmp6_20^post3 = ___cil_tmp6_20^0
		
		propagated equality lt_45^post3 = lt_45^0
		
		propagated equality lt_47^post3 = lt_47^0
		
		propagated equality lt_41^post3 = lt_41^0
		
		propagated equality lt_46^post3 = lt_46^0
		
		propagated equality lt_38^post3 = lt_38^0
		
		propagated equality npacketsold_9^post3 = npacketsold_9^0
		
		propagated equality lt_50^post3 = lt_50^0
		
		propagated equality lt_113^post3 = lt_113^0
		
		propagated equality lt_40^post3 = lt_40^0
		
		propagated equality lt_48^post3 = lt_48^0
		
		propagated equality cnt_198^post3 = cnt_198^0
		
		propagated equality cnt_122^post3 = cnt_122^0
		
		propagated equality lt_43^post3 = lt_43^0
		
		propagated equality cnt_117^post3 = cnt_117^0
		
		propagated equality i_12^post3 = i_12^0
		
		propagated equality lt_49^post3 = lt_49^0
		
		propagated equality tmp___1_17^post3 = tmp___1_17^0
		
		propagated equality lt_90^post3 = lt_90^0
		
		propagated equality npackets_10^post3 = npackets_10^0
		
		propagated equality devext_7^post3 = devext_7^0
		
		propagated equality cnt_94^post3 = cnt_94^0
		
		propagated equality tmp___2_18^post3 = tmp___2_18^0
		
		propagated equality request_8^post3 = request_8^0
		
		propagated equality tmp___0_16^post3 = tmp___0_16^0
		
		propagated equality ___retres5_19^post3 = ___retres5_19^0
		
		propagated equality result_4^post3 = result_4^0
		
		propagated equality cnt_187^post3 = cnt_187^0
		
		propagated equality lt_21^post3 = lt_21^0
		
		propagated equality lt_39^post3 = lt_39^0
		
		propagated equality tmp_15^post3 = tmp_15^0
		
		propagated equality lt_44^post3 = lt_44^0
		
		propagated equality loop_count_14^post3 = loop_count_14^0
		
		propagated equality lt_42^post3 = lt_42^0
		
		propagated equality irp_11^post3 = irp_11^0
		
		propagated equality lt_51^post3 = lt_51^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1+lt_44^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1+lt_44^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1+lt_44^0 <= 0, cost: 1
	New rule:
	l3 -> l4 : 1+lt_44^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^post4, ___retres5_19^0'=___retres5_19^post4, cnt_117^0'=cnt_117^post4, cnt_122^0'=cnt_122^post4, cnt_187^0'=cnt_187^post4, cnt_198^0'=cnt_198^post4, cnt_94^0'=cnt_94^post4, devext_7^0'=devext_7^post4, i_12^0'=i_12^post4, irp_11^0'=irp_11^post4, loop_count_14^0'=loop_count_14^post4, loop_max_13^0'=loop_max_13^post4, lt_113^0'=lt_113^post4, lt_21^0'=lt_21^post4, lt_38^0'=lt_38^post4, lt_39^0'=lt_39^post4, lt_40^0'=lt_40^post4, lt_41^0'=lt_41^post4, lt_42^0'=lt_42^post4, lt_43^0'=lt_43^post4, lt_44^0'=lt_44^post4, lt_45^0'=lt_45^post4, lt_46^0'=lt_46^post4, lt_47^0'=lt_47^post4, lt_48^0'=lt_48^post4, lt_49^0'=lt_49^post4, lt_50^0'=lt_50^post4, lt_51^0'=lt_51^post4, lt_90^0'=lt_90^post4, npackets_10^0'=npackets_10^post4, npacketsold_9^0'=npacketsold_9^post4, request_8^0'=request_8^post4, result_4^0'=result_4^post4, tmp_15^0'=tmp_15^post4, tmp___0_16^0'=tmp___0_16^post4, tmp___1_17^0'=tmp___1_17^post4, tmp___2_18^0'=tmp___2_18^post4, (-tmp___2_18^post4+tmp___2_18^0 == 0 /\ lt_46^0-lt_46^post4 == 0 /\ -___cil_tmp6_20^post4+___cil_tmp6_20^0 == 0 /\ -cnt_117^post4+cnt_117^0 == 0 /\ -cnt_122^post4+cnt_122^0 == 0 /\ -lt_90^post4+lt_90^0 == 0 /\ lt_41^0-lt_41^post4 == 0 /\ lt_48^0-lt_48^post4 == 0 /\ -cnt_94^post4+cnt_94^0 == 0 /\ ___retres5_19^0-___retres5_19^post4 == 0 /\ request_8^0-request_8^post4 == 0 /\ tmp_15^0-tmp_15^post4 == 0 /\ -loop_count_14^post4+loop_count_14^0 == 0 /\ lt_38^0-lt_38^post4 == 0 /\ -lt_44^post4+lt_44^0 == 0 /\ -lt_42^post4+lt_42^0 == 0 /\ lt_49^0-lt_49^post4 == 0 /\ -lt_40^post4+lt_40^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -irp_11^post4+irp_11^0 == 0 /\ cnt_187^0-cnt_187^post4 == 0 /\ tmp___0_16^0-tmp___0_16^post4 == 0 /\ -lt_51^post4+lt_51^0 == 0 /\ -lt_47^post4+lt_47^0 == 0 /\ -devext_7^post4+devext_7^0 == 0 /\ loop_max_13^0-loop_max_13^post4 == 0 /\ lt_43^0-lt_43^post4 == 0 /\ -lt_50^post4+lt_50^0 == 0 /\ -lt_21^post4+lt_21^0 == 0 /\ npacketsold_9^0-npacketsold_9^post4 == 0 /\ -tmp___1_17^post4+tmp___1_17^0 == 0 /\ i_12^0-i_12^post4 == 0 /\ cnt_198^0-cnt_198^post4 == 0 /\ -lt_39^post4+lt_39^0 == 0 /\ 1-lt_44^0 <= 0 /\ lt_45^0-lt_45^post4 == 0 /\ -npackets_10^post4+npackets_10^0 == 0 /\ -lt_113^post4+lt_113^0 == 0), cost: 1
	New rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-lt_44^0 <= 0), cost: 1
	
		propagated equality tmp___2_18^post4 = tmp___2_18^0
		
		propagated equality lt_46^post4 = lt_46^0
		
		propagated equality ___cil_tmp6_20^post4 = ___cil_tmp6_20^0
		
		propagated equality cnt_117^post4 = cnt_117^0
		
		propagated equality cnt_122^post4 = cnt_122^0
		
		propagated equality lt_90^post4 = lt_90^0
		
		propagated equality lt_41^post4 = lt_41^0
		
		propagated equality lt_48^post4 = lt_48^0
		
		propagated equality cnt_94^post4 = cnt_94^0
		
		propagated equality ___retres5_19^post4 = ___retres5_19^0
		
		propagated equality request_8^post4 = request_8^0
		
		propagated equality tmp_15^post4 = tmp_15^0
		
		propagated equality loop_count_14^post4 = loop_count_14^0
		
		propagated equality lt_38^post4 = lt_38^0
		
		propagated equality lt_44^post4 = lt_44^0
		
		propagated equality lt_42^post4 = lt_42^0
		
		propagated equality lt_49^post4 = lt_49^0
		
		propagated equality lt_40^post4 = lt_40^0
		
		propagated equality result_4^post4 = result_4^0
		
		propagated equality irp_11^post4 = irp_11^0
		
		propagated equality cnt_187^post4 = cnt_187^0
		
		propagated equality tmp___0_16^post4 = tmp___0_16^0
		
		propagated equality lt_51^post4 = lt_51^0
		
		propagated equality lt_47^post4 = lt_47^0
		
		propagated equality devext_7^post4 = devext_7^0
		
		propagated equality loop_max_13^post4 = loop_max_13^0
		
		propagated equality lt_43^post4 = lt_43^0
		
		propagated equality lt_50^post4 = lt_50^0
		
		propagated equality lt_21^post4 = lt_21^0
		
		propagated equality npacketsold_9^post4 = npacketsold_9^0
		
		propagated equality tmp___1_17^post4 = tmp___1_17^0
		
		propagated equality i_12^post4 = i_12^0
		
		propagated equality cnt_198^post4 = cnt_198^0
		
		propagated equality lt_39^post4 = lt_39^0
		
		propagated equality lt_45^post4 = lt_45^0
		
		propagated equality npackets_10^post4 = npackets_10^0
		
		propagated equality lt_113^post4 = lt_113^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-lt_44^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-lt_44^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-lt_44^0 <= 0, cost: 1
	New rule:
	l3 -> l4 : 1-lt_44^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l5 : ___cil_tmp6_20^0'=___cil_tmp6_20^post5, ___retres5_19^0'=___retres5_19^post5, cnt_117^0'=cnt_117^post5, cnt_122^0'=cnt_122^post5, cnt_187^0'=cnt_187^post5, cnt_198^0'=cnt_198^post5, cnt_94^0'=cnt_94^post5, devext_7^0'=devext_7^post5, i_12^0'=i_12^post5, irp_11^0'=irp_11^post5, loop_count_14^0'=loop_count_14^post5, loop_max_13^0'=loop_max_13^post5, lt_113^0'=lt_113^post5, lt_21^0'=lt_21^post5, lt_38^0'=lt_38^post5, lt_39^0'=lt_39^post5, lt_40^0'=lt_40^post5, lt_41^0'=lt_41^post5, lt_42^0'=lt_42^post5, lt_43^0'=lt_43^post5, lt_44^0'=lt_44^post5, lt_45^0'=lt_45^post5, lt_46^0'=lt_46^post5, lt_47^0'=lt_47^post5, lt_48^0'=lt_48^post5, lt_49^0'=lt_49^post5, lt_50^0'=lt_50^post5, lt_51^0'=lt_51^post5, lt_90^0'=lt_90^post5, npackets_10^0'=npackets_10^post5, npacketsold_9^0'=npacketsold_9^post5, request_8^0'=request_8^post5, result_4^0'=result_4^post5, tmp_15^0'=tmp_15^post5, tmp___0_16^0'=tmp___0_16^post5, tmp___1_17^0'=tmp___1_17^post5, tmp___2_18^0'=tmp___2_18^post5, (0 == 0 /\ lt_41^0-lt_41^post5 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post5 == 0 /\ loop_count_14^0-loop_count_14^post5 == 0 /\ -lt_90^post5+lt_90^0 == 0 /\ tmp_15^0-tmp_15^post5 == 0 /\ loop_max_13^0-loop_max_13^post5 == 0 /\ lt_48^0-lt_48^post5 == 0 /\ -request_8^post5+request_8^0 == 0 /\ -cnt_187^post5+cnt_187^0 == 0 /\ lt_42^post5-lt_113^0 == 0 /\ -npackets_10^post5+npackets_10^0 == 0 /\ cnt_122^0-cnt_122^post5 == 0 /\ -cnt_117^post5+cnt_117^0 == 0 /\ -lt_45^post5+lt_45^0 == 0 /\ irp_11^0-irp_11^post5 == 0 /\ lt_40^0-lt_40^post5 == 0 /\ -cnt_187^0+lt_43^post5 == 0 /\ lt_49^0-lt_49^post5 == 0 /\ -devext_7^post5+devext_7^0 == 0 /\ -tmp___1_17^post5+tmp___1_17^0 == 0 /\ npacketsold_9^0-npacketsold_9^post5 == 0 /\ result_4^0-result_4^post5 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ cnt_94^0-cnt_94^post5 == 0 /\ -lt_113^post5+lt_113^0 == 0 /\ -lt_51^post5+lt_51^0 == 0 /\ -lt_39^post5+lt_39^0 == 0 /\ lt_38^0-lt_38^post5 == 0 /\ -lt_50^post5+lt_50^0 == 0 /\ -cnt_198^post5+cnt_198^0 == 0 /\ -___retres5_19^post5+___retres5_19^0 == 0 /\ i_12^0-i_12^post5 == 0 /\ lt_46^0-lt_46^post5 == 0 /\ -tmp___2_18^post5+tmp___2_18^0 == 0 /\ lt_47^0-lt_47^post5 == 0 /\ tmp___0_16^0-tmp___0_16^post5 == 0), cost: 1
	New rule:
	l4 -> l5 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 0 == 0, cost: 1
	
		propagated equality lt_41^post5 = lt_41^0
		
		propagated equality ___cil_tmp6_20^post5 = ___cil_tmp6_20^0
		
		propagated equality loop_count_14^post5 = loop_count_14^0
		
		propagated equality lt_90^post5 = lt_90^0
		
		propagated equality tmp_15^post5 = tmp_15^0
		
		propagated equality loop_max_13^post5 = loop_max_13^0
		
		propagated equality lt_48^post5 = lt_48^0
		
		propagated equality request_8^post5 = request_8^0
		
		propagated equality cnt_187^post5 = cnt_187^0
		
		propagated equality lt_42^post5 = lt_113^0
		
		propagated equality npackets_10^post5 = npackets_10^0
		
		propagated equality cnt_122^post5 = cnt_122^0
		
		propagated equality cnt_117^post5 = cnt_117^0
		
		propagated equality lt_45^post5 = lt_45^0
		
		propagated equality irp_11^post5 = irp_11^0
		
		propagated equality lt_40^post5 = lt_40^0
		
		propagated equality lt_43^post5 = cnt_187^0
		
		propagated equality lt_49^post5 = lt_49^0
		
		propagated equality devext_7^post5 = devext_7^0
		
		propagated equality tmp___1_17^post5 = tmp___1_17^0
		
		propagated equality npacketsold_9^post5 = npacketsold_9^0
		
		propagated equality result_4^post5 = result_4^0
		
		propagated equality lt_21^post5 = lt_21^0
		
		propagated equality cnt_94^post5 = cnt_94^0
		
		propagated equality lt_113^post5 = lt_113^0
		
		propagated equality lt_51^post5 = lt_51^0
		
		propagated equality lt_39^post5 = lt_39^0
		
		propagated equality lt_38^post5 = lt_38^0
		
		propagated equality lt_50^post5 = lt_50^0
		
		propagated equality cnt_198^post5 = cnt_198^0
		
		propagated equality ___retres5_19^post5 = ___retres5_19^0
		
		propagated equality i_12^post5 = i_12^0
		
		propagated equality lt_46^post5 = lt_46^0
		
		propagated equality tmp___2_18^post5 = tmp___2_18^0
		
		propagated equality lt_47^post5 = lt_47^0
		
		propagated equality tmp___0_16^post5 = tmp___0_16^0
		
	Simplified Guard

	Original rule:
	l4 -> l5 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 0 == 0, cost: 1
	New rule:
	l4 -> l5 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l5 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, T, cost: 1
	New rule:
	l4 -> l5 : lt_42^0'=lt_113^0, lt_43^0'=cnt_187^0, lt_44^0'=lt_44^post5, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^post6, ___retres5_19^0'=___retres5_19^post6, cnt_117^0'=cnt_117^post6, cnt_122^0'=cnt_122^post6, cnt_187^0'=cnt_187^post6, cnt_198^0'=cnt_198^post6, cnt_94^0'=cnt_94^post6, devext_7^0'=devext_7^post6, i_12^0'=i_12^post6, irp_11^0'=irp_11^post6, loop_count_14^0'=loop_count_14^post6, loop_max_13^0'=loop_max_13^post6, lt_113^0'=lt_113^post6, lt_21^0'=lt_21^post6, lt_38^0'=lt_38^post6, lt_39^0'=lt_39^post6, lt_40^0'=lt_40^post6, lt_41^0'=lt_41^post6, lt_42^0'=lt_42^post6, lt_43^0'=lt_43^post6, lt_44^0'=lt_44^post6, lt_45^0'=lt_45^post6, lt_46^0'=lt_46^post6, lt_47^0'=lt_47^post6, lt_48^0'=lt_48^post6, lt_49^0'=lt_49^post6, lt_50^0'=lt_50^post6, lt_51^0'=lt_51^post6, lt_90^0'=lt_90^post6, npackets_10^0'=npackets_10^post6, npacketsold_9^0'=npacketsold_9^post6, request_8^0'=request_8^post6, result_4^0'=result_4^post6, tmp_15^0'=tmp_15^post6, tmp___0_16^0'=tmp___0_16^post6, tmp___1_17^0'=tmp___1_17^post6, tmp___2_18^0'=tmp___2_18^post6, (-lt_113^post6+lt_113^0 == 0 /\ lt_49^0-lt_49^post6 == 0 /\ npackets_10^0-npackets_10^post6 == 0 /\ lt_43^0-lt_43^post6 == 0 /\ lt_40^0-lt_40^post6 == 0 /\ -___retres5_19^post6+___retres5_19^0 == 0 /\ ___cil_tmp6_20^0-___cil_tmp6_20^post6 == 0 /\ -cnt_117^post6+cnt_117^0 == 0 /\ lt_41^0-lt_41^post6 == 0 /\ -lt_42^post6+lt_42^0 == 0 /\ 1+lt_43^0 <= 0 /\ lt_38^0-lt_38^post6 == 0 /\ tmp___1_17^0-tmp___1_17^post6 == 0 /\ -lt_90^post6+lt_90^0 == 0 /\ -lt_51^post6+lt_51^0 == 0 /\ -devext_7^post6+devext_7^0 == 0 /\ -lt_45^post6+lt_45^0 == 0 /\ cnt_94^0-cnt_94^post6 == 0 /\ loop_max_13^0-loop_max_13^post6 == 0 /\ tmp_15^0-tmp_15^post6 == 0 /\ i_12^0-i_12^post6 == 0 /\ -request_8^post6+request_8^0 == 0 /\ -cnt_198^post6+cnt_198^0 == 0 /\ npacketsold_9^0-npacketsold_9^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ lt_50^0-lt_50^post6 == 0 /\ -loop_count_14^post6+loop_count_14^0 == 0 /\ result_4^0-result_4^post6 == 0 /\ -tmp___2_18^post6+tmp___2_18^0 == 0 /\ irp_11^0-irp_11^post6 == 0 /\ cnt_187^0-cnt_187^post6 == 0 /\ -lt_39^post6+lt_39^0 == 0 /\ tmp___0_16^0-tmp___0_16^post6 == 0 /\ lt_46^0-lt_46^post6 == 0 /\ cnt_122^0-cnt_122^post6 == 0 /\ -lt_44^post6+lt_44^0 == 0 /\ -lt_48^post6+lt_48^0 == 0 /\ lt_47^0-lt_47^post6 == 0), cost: 1
	New rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1+lt_43^0 <= 0), cost: 1
	
		propagated equality lt_113^post6 = lt_113^0
		
		propagated equality lt_49^post6 = lt_49^0
		
		propagated equality npackets_10^post6 = npackets_10^0
		
		propagated equality lt_43^post6 = lt_43^0
		
		propagated equality lt_40^post6 = lt_40^0
		
		propagated equality ___retres5_19^post6 = ___retres5_19^0
		
		propagated equality ___cil_tmp6_20^post6 = ___cil_tmp6_20^0
		
		propagated equality cnt_117^post6 = cnt_117^0
		
		propagated equality lt_41^post6 = lt_41^0
		
		propagated equality lt_42^post6 = lt_42^0
		
		propagated equality lt_38^post6 = lt_38^0
		
		propagated equality tmp___1_17^post6 = tmp___1_17^0
		
		propagated equality lt_90^post6 = lt_90^0
		
		propagated equality lt_51^post6 = lt_51^0
		
		propagated equality devext_7^post6 = devext_7^0
		
		propagated equality lt_45^post6 = lt_45^0
		
		propagated equality cnt_94^post6 = cnt_94^0
		
		propagated equality loop_max_13^post6 = loop_max_13^0
		
		propagated equality tmp_15^post6 = tmp_15^0
		
		propagated equality i_12^post6 = i_12^0
		
		propagated equality request_8^post6 = request_8^0
		
		propagated equality cnt_198^post6 = cnt_198^0
		
		propagated equality npacketsold_9^post6 = npacketsold_9^0
		
		propagated equality lt_21^post6 = lt_21^0
		
		propagated equality lt_50^post6 = lt_50^0
		
		propagated equality loop_count_14^post6 = loop_count_14^0
		
		propagated equality result_4^post6 = result_4^0
		
		propagated equality tmp___2_18^post6 = tmp___2_18^0
		
		propagated equality irp_11^post6 = irp_11^0
		
		propagated equality cnt_187^post6 = cnt_187^0
		
		propagated equality lt_39^post6 = lt_39^0
		
		propagated equality tmp___0_16^post6 = tmp___0_16^0
		
		propagated equality lt_46^post6 = lt_46^0
		
		propagated equality cnt_122^post6 = cnt_122^0
		
		propagated equality lt_44^post6 = lt_44^0
		
		propagated equality lt_48^post6 = lt_48^0
		
		propagated equality lt_47^post6 = lt_47^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1+lt_43^0 <= 0), cost: 1
	New rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1+lt_43^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1+lt_43^0 <= 0, cost: 1
	New rule:
	l5 -> l6 : 1+lt_43^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^post7, ___retres5_19^0'=___retres5_19^post7, cnt_117^0'=cnt_117^post7, cnt_122^0'=cnt_122^post7, cnt_187^0'=cnt_187^post7, cnt_198^0'=cnt_198^post7, cnt_94^0'=cnt_94^post7, devext_7^0'=devext_7^post7, i_12^0'=i_12^post7, irp_11^0'=irp_11^post7, loop_count_14^0'=loop_count_14^post7, loop_max_13^0'=loop_max_13^post7, lt_113^0'=lt_113^post7, lt_21^0'=lt_21^post7, lt_38^0'=lt_38^post7, lt_39^0'=lt_39^post7, lt_40^0'=lt_40^post7, lt_41^0'=lt_41^post7, lt_42^0'=lt_42^post7, lt_43^0'=lt_43^post7, lt_44^0'=lt_44^post7, lt_45^0'=lt_45^post7, lt_46^0'=lt_46^post7, lt_47^0'=lt_47^post7, lt_48^0'=lt_48^post7, lt_49^0'=lt_49^post7, lt_50^0'=lt_50^post7, lt_51^0'=lt_51^post7, lt_90^0'=lt_90^post7, npackets_10^0'=npackets_10^post7, npacketsold_9^0'=npacketsold_9^post7, request_8^0'=request_8^post7, result_4^0'=result_4^post7, tmp_15^0'=tmp_15^post7, tmp___0_16^0'=tmp___0_16^post7, tmp___1_17^0'=tmp___1_17^post7, tmp___2_18^0'=tmp___2_18^post7, (loop_max_13^0-loop_max_13^post7 == 0 /\ -lt_38^post7+lt_38^0 == 0 /\ -lt_41^post7+lt_41^0 == 0 /\ -lt_39^post7+lt_39^0 == 0 /\ tmp_15^0-tmp_15^post7 == 0 /\ lt_43^0-lt_43^post7 == 0 /\ -cnt_122^post7+cnt_122^0 == 0 /\ result_4^0-result_4^post7 == 0 /\ -lt_42^post7+lt_42^0 == 0 /\ -lt_44^post7+lt_44^0 == 0 /\ tmp___2_18^0-tmp___2_18^post7 == 0 /\ ___retres5_19^0-___retres5_19^post7 == 0 /\ -lt_48^post7+lt_48^0 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ 1-lt_43^0 <= 0 /\ tmp___1_17^0-tmp___1_17^post7 == 0 /\ lt_46^0-lt_46^post7 == 0 /\ -devext_7^post7+devext_7^0 == 0 /\ -request_8^post7+request_8^0 == 0 /\ npacketsold_9^0-npacketsold_9^post7 == 0 /\ tmp___0_16^0-tmp___0_16^post7 == 0 /\ lt_40^0-lt_40^post7 == 0 /\ lt_47^0-lt_47^post7 == 0 /\ -lt_113^post7+lt_113^0 == 0 /\ i_12^0-i_12^post7 == 0 /\ -irp_11^post7+irp_11^0 == 0 /\ npackets_10^0-npackets_10^post7 == 0 /\ cnt_198^0-cnt_198^post7 == 0 /\ lt_49^0-lt_49^post7 == 0 /\ -lt_90^post7+lt_90^0 == 0 /\ -lt_51^post7+lt_51^0 == 0 /\ cnt_187^0-cnt_187^post7 == 0 /\ -lt_45^post7+lt_45^0 == 0 /\ -cnt_117^post7+cnt_117^0 == 0 /\ -loop_count_14^post7+loop_count_14^0 == 0 /\ -cnt_94^post7+cnt_94^0 == 0 /\ -___cil_tmp6_20^post7+___cil_tmp6_20^0 == 0 /\ lt_50^0-lt_50^post7 == 0), cost: 1
	New rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-lt_43^0 <= 0), cost: 1
	
		propagated equality loop_max_13^post7 = loop_max_13^0
		
		propagated equality lt_38^post7 = lt_38^0
		
		propagated equality lt_41^post7 = lt_41^0
		
		propagated equality lt_39^post7 = lt_39^0
		
		propagated equality tmp_15^post7 = tmp_15^0
		
		propagated equality lt_43^post7 = lt_43^0
		
		propagated equality cnt_122^post7 = cnt_122^0
		
		propagated equality result_4^post7 = result_4^0
		
		propagated equality lt_42^post7 = lt_42^0
		
		propagated equality lt_44^post7 = lt_44^0
		
		propagated equality tmp___2_18^post7 = tmp___2_18^0
		
		propagated equality ___retres5_19^post7 = ___retres5_19^0
		
		propagated equality lt_48^post7 = lt_48^0
		
		propagated equality lt_21^post7 = lt_21^0
		
		propagated equality tmp___1_17^post7 = tmp___1_17^0
		
		propagated equality lt_46^post7 = lt_46^0
		
		propagated equality devext_7^post7 = devext_7^0
		
		propagated equality request_8^post7 = request_8^0
		
		propagated equality npacketsold_9^post7 = npacketsold_9^0
		
		propagated equality tmp___0_16^post7 = tmp___0_16^0
		
		propagated equality lt_40^post7 = lt_40^0
		
		propagated equality lt_47^post7 = lt_47^0
		
		propagated equality lt_113^post7 = lt_113^0
		
		propagated equality i_12^post7 = i_12^0
		
		propagated equality irp_11^post7 = irp_11^0
		
		propagated equality npackets_10^post7 = npackets_10^0
		
		propagated equality cnt_198^post7 = cnt_198^0
		
		propagated equality lt_49^post7 = lt_49^0
		
		propagated equality lt_90^post7 = lt_90^0
		
		propagated equality lt_51^post7 = lt_51^0
		
		propagated equality cnt_187^post7 = cnt_187^0
		
		propagated equality lt_45^post7 = lt_45^0
		
		propagated equality cnt_117^post7 = cnt_117^0
		
		propagated equality loop_count_14^post7 = loop_count_14^0
		
		propagated equality cnt_94^post7 = cnt_94^0
		
		propagated equality ___cil_tmp6_20^post7 = ___cil_tmp6_20^0
		
		propagated equality lt_50^post7 = lt_50^0
		
	Simplified Guard

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ 1-lt_43^0 <= 0), cost: 1
	New rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-lt_43^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l6 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 1-lt_43^0 <= 0, cost: 1
	New rule:
	l5 -> l6 : 1-lt_43^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^post8, ___retres5_19^0'=___retres5_19^post8, cnt_117^0'=cnt_117^post8, cnt_122^0'=cnt_122^post8, cnt_187^0'=cnt_187^post8, cnt_198^0'=cnt_198^post8, cnt_94^0'=cnt_94^post8, devext_7^0'=devext_7^post8, i_12^0'=i_12^post8, irp_11^0'=irp_11^post8, loop_count_14^0'=loop_count_14^post8, loop_max_13^0'=loop_max_13^post8, lt_113^0'=lt_113^post8, lt_21^0'=lt_21^post8, lt_38^0'=lt_38^post8, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^post8, lt_45^0'=lt_45^post8, lt_46^0'=lt_46^post8, lt_47^0'=lt_47^post8, lt_48^0'=lt_48^post8, lt_49^0'=lt_49^post8, lt_50^0'=lt_50^post8, lt_51^0'=lt_51^post8, lt_90^0'=lt_90^post8, npackets_10^0'=npackets_10^post8, npacketsold_9^0'=npacketsold_9^post8, request_8^0'=request_8^post8, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^post8, tmp___0_16^0'=tmp___0_16^post8, tmp___1_17^0'=tmp___1_17^post8, tmp___2_18^0'=tmp___2_18^post8, (0 == 0 /\ request_8^0-request_8^post8 == 0 /\ ___retres5_19^0-___retres5_19^post8 == 0 /\ lt_90^0-lt_90^post8 == 0 /\ npacketsold_9^0-npacketsold_9^post8 == 0 /\ -loop_count_14^post8+loop_count_14^0 == 0 /\ -lt_50^post8+lt_50^0 == 0 /\ -lt_90^0+lt_41^1 == 0 /\ cnt_94^0-cnt_94^post8 == 0 /\ cnt_187^0-cnt_187^post8 == 0 /\ -lt_46^post8+lt_46^0 == 0 /\ i_12^0-i_12^post8 == 0 /\ -tmp___1_17^post8+tmp___1_17^0 == 0 /\ tmp___0_16^0-tmp___0_16^post8 == 0 /\ -lt_45^post8+lt_45^0 == 0 /\ -npackets_10^post8+npackets_10^0 == 0 /\ -lt_113^post8+lt_113^0 == 0 /\ tmp_15^0-tmp_15^post8 == 0 /\ -cnt_117^post8+cnt_117^0 == 0 /\ -cnt_198^post8+cnt_198^0 == 0 /\ -cnt_122^post8+cnt_122^0 == 0 /\ lt_39^1-lt_113^0 == 0 /\ lt_40^1-cnt_198^0 == 0 /\ -___cil_tmp6_20^post8+___cil_tmp6_20^0 == 0 /\ lt_38^post8-lt_90^0 == 0 /\ loop_max_13^0-loop_max_13^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -tmp___2_18^post8+tmp___2_18^0 == 0 /\ -lt_51^post8+lt_51^0 == 0 /\ lt_48^0-lt_48^post8 == 0 /\ -lt_47^post8+lt_47^0 == 0 /\ lt_49^0-lt_49^post8 == 0 /\ -devext_7^post8+devext_7^0 == 0 /\ -lt_44^post8+lt_44^0 == 0 /\ irp_11^0-irp_11^post8 == 0), cost: 1
	New rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ -lt_90^0+lt_41^1 == 0 /\ lt_39^1-lt_113^0 == 0 /\ lt_40^1-cnt_198^0 == 0), cost: 1
	
		propagated equality request_8^post8 = request_8^0
		
		propagated equality ___retres5_19^post8 = ___retres5_19^0
		
		propagated equality lt_90^post8 = lt_90^0
		
		propagated equality npacketsold_9^post8 = npacketsold_9^0
		
		propagated equality loop_count_14^post8 = loop_count_14^0
		
		propagated equality lt_50^post8 = lt_50^0
		
		propagated equality cnt_94^post8 = cnt_94^0
		
		propagated equality cnt_187^post8 = cnt_187^0
		
		propagated equality lt_46^post8 = lt_46^0
		
		propagated equality i_12^post8 = i_12^0
		
		propagated equality tmp___1_17^post8 = tmp___1_17^0
		
		propagated equality tmp___0_16^post8 = tmp___0_16^0
		
		propagated equality lt_45^post8 = lt_45^0
		
		propagated equality npackets_10^post8 = npackets_10^0
		
		propagated equality lt_113^post8 = lt_113^0
		
		propagated equality tmp_15^post8 = tmp_15^0
		
		propagated equality cnt_117^post8 = cnt_117^0
		
		propagated equality cnt_198^post8 = cnt_198^0
		
		propagated equality cnt_122^post8 = cnt_122^0
		
		propagated equality ___cil_tmp6_20^post8 = ___cil_tmp6_20^0
		
		propagated equality lt_38^post8 = lt_90^0
		
		propagated equality loop_max_13^post8 = loop_max_13^0
		
		propagated equality lt_21^post8 = lt_21^0
		
		propagated equality tmp___2_18^post8 = tmp___2_18^0
		
		propagated equality lt_51^post8 = lt_51^0
		
		propagated equality lt_48^post8 = lt_48^0
		
		propagated equality lt_47^post8 = lt_47^0
		
		propagated equality lt_49^post8 = lt_49^0
		
		propagated equality devext_7^post8 = devext_7^0
		
		propagated equality lt_44^post8 = lt_44^0
		
		propagated equality irp_11^post8 = irp_11^0
		
	Propagated Equalities

	Original rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ -lt_90^0+lt_41^1 == 0 /\ lt_39^1-lt_113^0 == 0 /\ lt_40^1-cnt_198^0 == 0), cost: 1
	New rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 0 == 0, cost: 1
	
		propagated equality lt_41^1 = lt_90^0
		
		propagated equality lt_39^1 = lt_113^0
		
		propagated equality lt_40^1 = cnt_198^0
		
	Simplified Guard

	Original rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, 0 == 0, cost: 1
	New rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l2 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_50^0, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=result_4^post8, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, T, cost: 1
	New rule:
	l6 -> l2 : lt_38^0'=lt_90^0, lt_39^0'=lt_39^post8, lt_40^0'=lt_40^post8, lt_41^0'=lt_41^post8, lt_42^0'=lt_42^post8, lt_43^0'=lt_43^post8, result_4^0'=result_4^post8, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l7 : ___cil_tmp6_20^0'=___cil_tmp6_20^post9, ___retres5_19^0'=___retres5_19^post9, cnt_117^0'=cnt_117^post9, cnt_122^0'=cnt_122^post9, cnt_187^0'=cnt_187^post9, cnt_198^0'=cnt_198^post9, cnt_94^0'=cnt_94^post9, devext_7^0'=devext_7^post9, i_12^0'=i_12^post9, irp_11^0'=irp_11^post9, loop_count_14^0'=loop_count_14^post9, loop_max_13^0'=loop_max_13^post9, lt_113^0'=lt_113^post9, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^post9, lt_39^0'=lt_39^post9, lt_40^0'=lt_40^post9, lt_41^0'=lt_41^post9, lt_42^0'=lt_42^post9, lt_43^0'=lt_43^post9, lt_44^0'=lt_44^post9, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^post9, lt_90^0'=lt_90^post9, npackets_10^0'=npackets_10^post9, npacketsold_9^0'=npacketsold_9^post9, request_8^0'=request_8^post9, result_4^0'=result_4^post9, tmp_15^0'=tmp_15^post9, tmp___0_16^0'=tmp___0_16^post9, tmp___1_17^0'=tmp___1_17^post9, tmp___2_18^0'=tmp___2_18^post9, (0 == 0 /\ cnt_187^0-cnt_187^post9 == 0 /\ lt_38^0-lt_38^post9 == 0 /\ -cnt_198^post9+cnt_198^0 == 0 /\ npacketsold_9^0-npacketsold_9^post9 == 0 /\ -loop_count_14^post9+loop_count_14^0 == 0 /\ -cnt_117^post9+cnt_117^0 == 0 /\ -cnt_122^post9+cnt_122^0 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ -tmp___2_18^post9+tmp___2_18^0 == 0 /\ -lt_90^post9+lt_90^0 == 0 /\ cnt_94^0-cnt_94^post9 == 0 /\ -lt_44^post9+lt_44^0 == 0 /\ -loop_max_13^post9+loop_max_13^0 == 0 /\ -lt_42^post9+lt_42^0 == 0 /\ lt_43^0-lt_43^post9 == 0 /\ -irp_11^post9+irp_11^0 == 0 /\ -lt_113^post9+lt_113^0 == 0 /\ lt_21^1-lt_90^0 == 0 /\ lt_40^0-lt_40^post9 == 0 /\ result_4^post9-___cil_tmp6_20^post9 == 0 /\ -lt_45^1+lt_46^1 <= 0 /\ lt_41^0-lt_41^post9 == 0 /\ tmp_15^0-tmp_15^post9 == 0 /\ -lt_51^post9+lt_51^0 == 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ -tmp___1_17^post9+tmp___1_17^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ -lt_39^post9+lt_39^0 == 0 /\ -devext_7^post9+devext_7^0 == 0 /\ lt_47^1-lt_90^0 == 0 /\ ___cil_tmp6_20^post9-___retres5_19^post9 == 0 /\ -request_8^post9+request_8^0 == 0 /\ -tmp___0_16^post9+tmp___0_16^0 == 0 /\ ___retres5_19^post9 == 0 /\ npackets_10^0-npackets_10^post9 == 0 /\ -i_12^post9+i_12^0 == 0), cost: 1
	New rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ lt_21^1-lt_90^0 == 0 /\ -lt_45^1+lt_46^1 <= 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ lt_47^1-lt_90^0 == 0), cost: 1
	
		propagated equality cnt_187^post9 = cnt_187^0
		
		propagated equality lt_38^post9 = lt_38^0
		
		propagated equality cnt_198^post9 = cnt_198^0
		
		propagated equality npacketsold_9^post9 = npacketsold_9^0
		
		propagated equality loop_count_14^post9 = loop_count_14^0
		
		propagated equality cnt_117^post9 = cnt_117^0
		
		propagated equality cnt_122^post9 = cnt_122^0
		
		propagated equality tmp___2_18^post9 = tmp___2_18^0
		
		propagated equality lt_90^post9 = lt_90^0
		
		propagated equality cnt_94^post9 = cnt_94^0
		
		propagated equality lt_44^post9 = lt_44^0
		
		propagated equality loop_max_13^post9 = loop_max_13^0
		
		propagated equality lt_42^post9 = lt_42^0
		
		propagated equality lt_43^post9 = lt_43^0
		
		propagated equality irp_11^post9 = irp_11^0
		
		propagated equality lt_113^post9 = lt_113^0
		
		propagated equality lt_40^post9 = lt_40^0
		
		propagated equality ___cil_tmp6_20^post9 = result_4^post9
		
		propagated equality lt_41^post9 = lt_41^0
		
		propagated equality tmp_15^post9 = tmp_15^0
		
		propagated equality lt_51^post9 = lt_51^0
		
		propagated equality tmp___1_17^post9 = tmp___1_17^0
		
		propagated equality lt_39^post9 = lt_39^0
		
		propagated equality devext_7^post9 = devext_7^0
		
		propagated equality ___retres5_19^post9 = result_4^post9
		
		propagated equality request_8^post9 = request_8^0
		
		propagated equality tmp___0_16^post9 = tmp___0_16^0
		
		propagated equality result_4^post9 = 0
		
		propagated equality npackets_10^post9 = npackets_10^0
		
		propagated equality i_12^post9 = i_12^0
		
	Propagated Equalities

	Original rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ lt_49^1-cnt_94^0 == 0 /\ lt_21^1-lt_90^0 == 0 /\ -lt_45^1+lt_46^1 <= 0 /\ lt_46^1-cnt_122^0 == 0 /\ lt_45^1-cnt_117^0 == 0 /\ -tmp___0_16^0+lt_48^1 == 0 /\ lt_47^1-lt_90^0 == 0), cost: 1
	New rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ cnt_122^0-cnt_117^0 <= 0), cost: 1
	
		propagated equality lt_49^1 = cnt_94^0
		
		propagated equality lt_21^1 = lt_90^0
		
		propagated equality lt_46^1 = cnt_122^0
		
		propagated equality lt_45^1 = cnt_117^0
		
		propagated equality lt_48^1 = tmp___0_16^0
		
		propagated equality lt_47^1 = lt_90^0
		
	Simplified Guard

	Original rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, (0 == 0 /\ cnt_122^0-cnt_117^0 <= 0), cost: 1
	New rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, cnt_122^0-cnt_117^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^0, i_12^0'=i_12^0, irp_11^0'=irp_11^0, loop_count_14^0'=loop_count_14^0, loop_max_13^0'=loop_max_13^0, lt_113^0'=lt_113^0, lt_21^0'=lt_21^post9, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, lt_51^0'=lt_51^0, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^0, npacketsold_9^0'=npacketsold_9^0, request_8^0'=request_8^0, result_4^0'=0, tmp_15^0'=tmp_15^0, tmp___0_16^0'=tmp___0_16^0, tmp___1_17^0'=tmp___1_17^0, tmp___2_18^0'=tmp___2_18^0, cnt_122^0-cnt_117^0 <= 0, cost: 1
	New rule:
	l1 -> l7 : ___cil_tmp6_20^0'=0, ___retres5_19^0'=0, lt_21^0'=lt_21^post9, lt_45^0'=lt_45^post9, lt_46^0'=lt_46^post9, lt_47^0'=lt_47^post9, lt_48^0'=lt_48^post9, lt_49^0'=lt_49^post9, lt_50^0'=lt_50^post9, result_4^0'=0, cnt_122^0-cnt_117^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^post1, ___retres5_19^0'=___retres5_19^post1, cnt_117^0'=cnt_117^post1, cnt_122^0'=cnt_122^post1, cnt_187^0'=cnt_187^post1, cnt_198^0'=cnt_198^post1, cnt_94^0'=cnt_94^post1, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^post1, lt_21^0'=lt_21^post1, lt_38^0'=lt_38^post1, lt_39^0'=lt_39^post1, lt_40^0'=lt_40^post1, lt_41^0'=lt_41^post1, lt_42^0'=lt_42^post1, lt_43^0'=lt_43^post1, lt_44^0'=lt_44^post1, lt_45^0'=lt_45^post1, lt_46^0'=lt_46^post1, lt_47^0'=lt_47^post1, lt_48^0'=lt_48^post1, lt_49^0'=lt_49^post1, lt_50^0'=lt_50^post1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^post1, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=tmp_15^post1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, (0 == 0 /\ tmp_15^0-tmp_15^post10 == 0 /\ -cnt_198^post1+cnt_198^post10 == 0 /\ lt_47^post10-lt_47^post1 == 0 /\ cnt_94^0-cnt_94^post10 == 0 /\ -lt_48^post1+lt_48^post10 == 0 /\ -loop_count_14^post10+loop_count_14^0 == 0 /\ -devext_7^post10+devext_7^0 == 0 /\ -request_8^post10+request_8^0 == 0 /\ -cnt_117^post1+cnt_117^post10 == 0 /\ cnt_187^0-cnt_187^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ -lt_113^post1+lt_113^post10 == 0 /\ -lt_45^post1+lt_45^post10 == 0 /\ lt_50^post1-tmp_15^post1 == 0 /\ npackets_10^0-npackets_10^post10 == 0 /\ -tmp___1_17^post10+tmp___1_17^0 == 0 /\ lt_41^post10-lt_41^post1 == 0 /\ lt_40^post10-lt_40^post1 == 0 /\ lt_45^0-lt_45^post10 == 0 /\ -cnt_122^post1+cnt_122^post10 == 0 /\ -lt_46^post1+lt_46^post10 == 0 /\ npacketsold_9^0-npacketsold_9^post10 == 0 /\ lt_50^0-lt_50^post10 == 0 /\ -cnt_117^post10+cnt_117^0 == 0 /\ lt_90^post10-lt_90^post1 == 0 /\ lt_46^0-lt_46^post10 == 0 /\ -___cil_tmp6_20^post10+___cil_tmp6_20^0 == 0 /\ ___cil_tmp6_20^post10-___cil_tmp6_20^post1 == 0 /\ i_12^0-i_12^post10 == 0 /\ -___retres5_19^post1+___retres5_19^post10 == 0 /\ lt_51^0-lt_51^post10 == 0 /\ lt_41^0-lt_41^post10 == 0 /\ lt_43^post10-lt_43^post1 == 0 /\ -lt_44^post10+lt_44^0 == 0 /\ -lt_40^post10+lt_40^0 == 0 /\ lt_42^0-lt_42^post10 == 0 /\ irp_11^0-irp_11^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -lt_39^post10+lt_39^0 == 0 /\ -lt_47^post10+lt_47^0 == 0 /\ cnt_187^post10-cnt_187^post1 == 0 /\ lt_44^post10-lt_44^post1 == 0 /\ lt_48^0-lt_48^post10 == 0 /\ -lt_49^post1+lt_49^post10 == 0 /\ -cnt_94^post1+cnt_94^post10 == 0 /\ -tmp___2_18^post10+tmp___2_18^0 == 0 /\ loop_max_13^0-loop_max_13^post10 == 0 /\ ___retres5_19^0-___retres5_19^post10 == 0 /\ -lt_113^post10+lt_113^0 == 0 /\ -lt_43^post10+lt_43^0 == 0 /\ lt_21^post10-lt_21^post1 == 0 /\ lt_51^1-tmp_15^post1 == 0 /\ -lt_90^post10+lt_90^0 == 0 /\ -lt_39^post1+lt_39^post10 == 0 /\ cnt_122^0-cnt_122^post10 == 0 /\ -cnt_198^post10+cnt_198^0 == 0 /\ -lt_42^post1+lt_42^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ tmp___0_16^0-tmp___0_16^post10 == 0 /\ -lt_38^post1+lt_38^post10 == 0 /\ lt_49^0-lt_49^post10 == 0), cost: 1
	New rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^post10, ___retres5_19^0'=___retres5_19^post10, cnt_117^0'=cnt_117^post10, cnt_122^0'=cnt_122^post10, cnt_187^0'=cnt_187^post10, cnt_198^0'=cnt_198^post10, cnt_94^0'=cnt_94^post10, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^post10, lt_21^0'=lt_21^post10, lt_38^0'=lt_38^post10, lt_39^0'=lt_39^post10, lt_40^0'=lt_40^post10, lt_41^0'=lt_41^post10, lt_42^0'=lt_42^post10, lt_43^0'=lt_43^post10, lt_44^0'=lt_44^post10, lt_45^0'=lt_45^post10, lt_46^0'=lt_46^post10, lt_47^0'=lt_47^post10, lt_48^0'=lt_48^post10, lt_49^0'=lt_49^post10, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^post10, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, (0 == 0 /\ tmp_15^0-tmp_15^post10 == 0 /\ cnt_94^0-cnt_94^post10 == 0 /\ -loop_count_14^post10+loop_count_14^0 == 0 /\ -devext_7^post10+devext_7^0 == 0 /\ -request_8^post10+request_8^0 == 0 /\ cnt_187^0-cnt_187^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ npackets_10^0-npackets_10^post10 == 0 /\ -tmp___1_17^post10+tmp___1_17^0 == 0 /\ lt_45^0-lt_45^post10 == 0 /\ npacketsold_9^0-npacketsold_9^post10 == 0 /\ lt_50^0-lt_50^post10 == 0 /\ -cnt_117^post10+cnt_117^0 == 0 /\ lt_46^0-lt_46^post10 == 0 /\ -___cil_tmp6_20^post10+___cil_tmp6_20^0 == 0 /\ i_12^0-i_12^post10 == 0 /\ lt_51^0-lt_51^post10 == 0 /\ lt_41^0-lt_41^post10 == 0 /\ -lt_44^post10+lt_44^0 == 0 /\ -lt_40^post10+lt_40^0 == 0 /\ lt_42^0-lt_42^post10 == 0 /\ irp_11^0-irp_11^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -lt_39^post10+lt_39^0 == 0 /\ -lt_47^post10+lt_47^0 == 0 /\ lt_48^0-lt_48^post10 == 0 /\ -tmp___2_18^post10+tmp___2_18^0 == 0 /\ loop_max_13^0-loop_max_13^post10 == 0 /\ ___retres5_19^0-___retres5_19^post10 == 0 /\ -lt_113^post10+lt_113^0 == 0 /\ -lt_43^post10+lt_43^0 == 0 /\ -lt_90^post10+lt_90^0 == 0 /\ cnt_122^0-cnt_122^post10 == 0 /\ -cnt_198^post10+cnt_198^0 == 0 /\ result_4^0-result_4^post10 == 0 /\ tmp___0_16^0-tmp___0_16^post10 == 0 /\ lt_49^0-lt_49^post10 == 0), cost: 1
	
		propagated equality cnt_198^post1 = cnt_198^post10
		
		propagated equality lt_47^post1 = lt_47^post10
		
		propagated equality lt_48^post1 = lt_48^post10
		
		propagated equality cnt_117^post1 = cnt_117^post10
		
		propagated equality lt_113^post1 = lt_113^post10
		
		propagated equality lt_45^post1 = lt_45^post10
		
		propagated equality lt_50^post1 = tmp_15^post1
		
		propagated equality lt_41^post1 = lt_41^post10
		
		propagated equality lt_40^post1 = lt_40^post10
		
		propagated equality cnt_122^post1 = cnt_122^post10
		
		propagated equality lt_46^post1 = lt_46^post10
		
		propagated equality lt_90^post1 = lt_90^post10
		
		propagated equality ___cil_tmp6_20^post1 = ___cil_tmp6_20^post10
		
		propagated equality ___retres5_19^post1 = ___retres5_19^post10
		
		propagated equality lt_43^post1 = lt_43^post10
		
		propagated equality cnt_187^post1 = cnt_187^post10
		
		propagated equality lt_44^post1 = lt_44^post10
		
		propagated equality lt_49^post1 = lt_49^post10
		
		propagated equality cnt_94^post1 = cnt_94^post10
		
		propagated equality lt_21^post1 = lt_21^post10
		
		propagated equality tmp_15^post1 = lt_51^1
		
		propagated equality lt_39^post1 = lt_39^post10
		
		propagated equality lt_42^post1 = lt_42^post10
		
		propagated equality lt_38^post1 = lt_38^post10
		
	Propagated Equalities

	Original rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^post10, ___retres5_19^0'=___retres5_19^post10, cnt_117^0'=cnt_117^post10, cnt_122^0'=cnt_122^post10, cnt_187^0'=cnt_187^post10, cnt_198^0'=cnt_198^post10, cnt_94^0'=cnt_94^post10, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^post10, lt_21^0'=lt_21^post10, lt_38^0'=lt_38^post10, lt_39^0'=lt_39^post10, lt_40^0'=lt_40^post10, lt_41^0'=lt_41^post10, lt_42^0'=lt_42^post10, lt_43^0'=lt_43^post10, lt_44^0'=lt_44^post10, lt_45^0'=lt_45^post10, lt_46^0'=lt_46^post10, lt_47^0'=lt_47^post10, lt_48^0'=lt_48^post10, lt_49^0'=lt_49^post10, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^post10, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, (0 == 0 /\ tmp_15^0-tmp_15^post10 == 0 /\ cnt_94^0-cnt_94^post10 == 0 /\ -loop_count_14^post10+loop_count_14^0 == 0 /\ -devext_7^post10+devext_7^0 == 0 /\ -request_8^post10+request_8^0 == 0 /\ cnt_187^0-cnt_187^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ npackets_10^0-npackets_10^post10 == 0 /\ -tmp___1_17^post10+tmp___1_17^0 == 0 /\ lt_45^0-lt_45^post10 == 0 /\ npacketsold_9^0-npacketsold_9^post10 == 0 /\ lt_50^0-lt_50^post10 == 0 /\ -cnt_117^post10+cnt_117^0 == 0 /\ lt_46^0-lt_46^post10 == 0 /\ -___cil_tmp6_20^post10+___cil_tmp6_20^0 == 0 /\ i_12^0-i_12^post10 == 0 /\ lt_51^0-lt_51^post10 == 0 /\ lt_41^0-lt_41^post10 == 0 /\ -lt_44^post10+lt_44^0 == 0 /\ -lt_40^post10+lt_40^0 == 0 /\ lt_42^0-lt_42^post10 == 0 /\ irp_11^0-irp_11^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -lt_39^post10+lt_39^0 == 0 /\ -lt_47^post10+lt_47^0 == 0 /\ lt_48^0-lt_48^post10 == 0 /\ -tmp___2_18^post10+tmp___2_18^0 == 0 /\ loop_max_13^0-loop_max_13^post10 == 0 /\ ___retres5_19^0-___retres5_19^post10 == 0 /\ -lt_113^post10+lt_113^0 == 0 /\ -lt_43^post10+lt_43^0 == 0 /\ -lt_90^post10+lt_90^0 == 0 /\ cnt_122^0-cnt_122^post10 == 0 /\ -cnt_198^post10+cnt_198^0 == 0 /\ result_4^0-result_4^post10 == 0 /\ tmp___0_16^0-tmp___0_16^post10 == 0 /\ lt_49^0-lt_49^post10 == 0), cost: 1
	New rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, 0 == 0, cost: 1
	
		propagated equality tmp_15^post10 = tmp_15^0
		
		propagated equality cnt_94^post10 = cnt_94^0
		
		propagated equality loop_count_14^post10 = loop_count_14^0
		
		propagated equality devext_7^post10 = devext_7^0
		
		propagated equality request_8^post10 = request_8^0
		
		propagated equality cnt_187^post10 = cnt_187^0
		
		propagated equality lt_38^post10 = lt_38^0
		
		propagated equality npackets_10^post10 = npackets_10^0
		
		propagated equality tmp___1_17^post10 = tmp___1_17^0
		
		propagated equality lt_45^post10 = lt_45^0
		
		propagated equality npacketsold_9^post10 = npacketsold_9^0
		
		propagated equality lt_50^post10 = lt_50^0
		
		propagated equality cnt_117^post10 = cnt_117^0
		
		propagated equality lt_46^post10 = lt_46^0
		
		propagated equality ___cil_tmp6_20^post10 = ___cil_tmp6_20^0
		
		propagated equality i_12^post10 = i_12^0
		
		propagated equality lt_51^post10 = lt_51^0
		
		propagated equality lt_41^post10 = lt_41^0
		
		propagated equality lt_44^post10 = lt_44^0
		
		propagated equality lt_40^post10 = lt_40^0
		
		propagated equality lt_42^post10 = lt_42^0
		
		propagated equality irp_11^post10 = irp_11^0
		
		propagated equality lt_21^post10 = lt_21^0
		
		propagated equality lt_39^post10 = lt_39^0
		
		propagated equality lt_47^post10 = lt_47^0
		
		propagated equality lt_48^post10 = lt_48^0
		
		propagated equality tmp___2_18^post10 = tmp___2_18^0
		
		propagated equality loop_max_13^post10 = loop_max_13^0
		
		propagated equality ___retres5_19^post10 = ___retres5_19^0
		
		propagated equality lt_113^post10 = lt_113^0
		
		propagated equality lt_43^post10 = lt_43^0
		
		propagated equality lt_90^post10 = lt_90^0
		
		propagated equality cnt_122^post10 = cnt_122^0
		
		propagated equality cnt_198^post10 = cnt_198^0
		
		propagated equality result_4^post10 = result_4^0
		
		propagated equality tmp___0_16^post10 = tmp___0_16^0
		
		propagated equality lt_49^post10 = lt_49^0
		
	Simplified Guard

	Original rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, 0 == 0, cost: 1
	New rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l1 : ___cil_tmp6_20^0'=___cil_tmp6_20^0, ___retres5_19^0'=___retres5_19^0, cnt_117^0'=cnt_117^0, cnt_122^0'=cnt_122^0, cnt_187^0'=cnt_187^0, cnt_198^0'=cnt_198^0, cnt_94^0'=cnt_94^0, devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_113^0'=lt_113^0, lt_21^0'=lt_21^0, lt_38^0'=lt_38^0, lt_39^0'=lt_39^0, lt_40^0'=lt_40^0, lt_41^0'=lt_41^0, lt_42^0'=lt_42^0, lt_43^0'=lt_43^0, lt_44^0'=lt_44^0, lt_45^0'=lt_45^0, lt_46^0'=lt_46^0, lt_47^0'=lt_47^0, lt_48^0'=lt_48^0, lt_49^0'=lt_49^0, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, lt_90^0'=lt_90^0, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, T, cost: 1
	New rule:
	l8 -> l1 : devext_7^0'=devext_7^post1, i_12^0'=i_12^post1, irp_11^0'=irp_11^post1, loop_count_14^0'=loop_count_14^post1, loop_max_13^0'=loop_max_13^post1, lt_50^0'=lt_51^1, lt_51^0'=lt_51^post1, npackets_10^0'=npackets_10^post1, npacketsold_9^0'=npacketsold_9^post1, request_8^0'=request_8^post1, result_4^0'=result_4^post1, tmp_15^0'=lt_51^1, tmp___0_16^0'=tmp___0_16^post1, tmp___1_17^0'=tmp___1_17^post1, tmp___2_18^0'=tmp___2_18^post1, T, cost: 1

Step with 19

	Trace

	19[T]
	
	Blocked

	[{}, {}]

Step with 11

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 12

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}]

Step with 14

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {}, {}, {}]

Step with 15

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {}]

Step with 17

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)], 17[T]
	
	Blocked

	[{}, {}, {}, {}, {}, {}, {}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}, {17[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {}, {}, {15[T]}]

Step with 16

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {15[T]}, {}]

Step with 17

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)], 17[T]
	
	Blocked

	[{}, {}, {}, {}, {15[T]}, {}, {}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {15[T]}, {17[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {}, {}, {15[T], 16[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 12[(1+lt_44^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {14[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}]

Step with 13

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {}]

Step with 14

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {12[T]}, {}, {}]

Step with 16

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {}, {}, {}]

Step with 17

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)], 17[T]
	
	Blocked

	[{}, {}, {12[T]}, {}, {}, {}, {}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 16[(1-lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {}, {}, {17[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {12[T]}, {}, {16[T]}]

Step with 15

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {}, {16[T]}, {}]

Step with 17

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)], 17[T]
	
	Blocked

	[{}, {}, {12[T]}, {}, {16[T]}, {}, {}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T], 15[(1+lt_43^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {}, {16[T]}, {17[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)], 14[T]
	
	Blocked

	[{}, {}, {12[T]}, {}, {15[T], 16[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)], 13[(1-lt_44^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T]}, {14[T]}]

Backtrack

	Trace

	19[T], 11[(1-cnt_122^0+cnt_117^0 <= 0)]
	
	Blocked

	[{}, {}, {12[T], 13[T]}]

Backtrack

	Trace

	19[T]
	
	Blocked

	[{}, {11[T]}]

Step with 18

	Trace

	19[T], 18[(cnt_122^0-cnt_117^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {}]

Backtrack

	Trace

	19[T]
	
	Blocked

	[{}, {11[T], 18[T]}]

Backtrack

	Trace

	Blocked

	[{19[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b