by AProVE
| l0 | 1 | l1: | x1 = _Result_4HAT0 ∧ x2 = _cnt_58HAT0 ∧ x3 = _devExt_7HAT0 ∧ x4 = _i_12HAT0 ∧ x5 = _irp_11HAT0 ∧ x6 = _loop_count_14HAT0 ∧ x7 = _loop_max_13HAT0 ∧ x8 = _lt_46HAT0 ∧ x9 = _nPacketsOld_9HAT0 ∧ x10 = _nPackets_10HAT0 ∧ x11 = _request_8HAT0 ∧ x1 = _Result_4HATpost ∧ x2 = _cnt_58HATpost ∧ x3 = _devExt_7HATpost ∧ x4 = _i_12HATpost ∧ x5 = _irp_11HATpost ∧ x6 = _loop_count_14HATpost ∧ x7 = _loop_max_13HATpost ∧ x8 = _lt_46HATpost ∧ x9 = _nPacketsOld_9HATpost ∧ x10 = _nPackets_10HATpost ∧ x11 = _request_8HATpost ∧ _cnt_58HAT0 = _cnt_58HATpost ∧ _Result_4HATpost = _Result_4HATpost ∧ _lt_46HATpost = _cnt_58HAT0 ∧ _devExt_7HATpost = _devExt_7HATpost ∧ _request_8HATpost = _request_8HATpost ∧ _nPacketsOld_9HATpost = _nPacketsOld_9HATpost ∧ _nPackets_10HATpost = _nPackets_10HATpost ∧ _irp_11HATpost = _irp_11HATpost ∧ _i_12HATpost = _i_12HATpost ∧ _loop_max_13HATpost = _loop_max_13HATpost ∧ _loop_count_14HATpost = _loop_count_14HATpost | |
| l2 | 2 | l0: | x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x7 ∧ x9 = _x8 ∧ x10 = _x9 ∧ x11 = _x10 ∧ x1 = _x11 ∧ x2 = _x12 ∧ x3 = _x13 ∧ x4 = _x14 ∧ x5 = _x15 ∧ x6 = _x16 ∧ x7 = _x17 ∧ x8 = _x18 ∧ x9 = _x19 ∧ x10 = _x20 ∧ x11 = _x21 ∧ _x10 = _x21 ∧ _x9 = _x20 ∧ _x8 = _x19 ∧ _x7 = _x18 ∧ _x6 = _x17 ∧ _x5 = _x16 ∧ _x4 = _x15 ∧ _x3 = _x14 ∧ _x2 = _x13 ∧ _x1 = _x12 ∧ _x = _x11 |
| l0 | l0 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 |
| l2 | l2 | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 |
There exist no SCC in the program graph.