YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l31, true>
<l1, l2, true>
<l3, l4, ((1 + next^0) <= (1 + N^0))>
<l5, l1, ((1 + next^0) <= (1 + N^0)), par{i^0 -> (1 + i^0)}>
<l6, l5, ((1 + s_ab^0) <= 1), par{s_ab^0 -> 1}>
<l6, l5, (1 <= (0 + s_ab^0)), par{s_ab^0 -> 0}>
<l7, l8, (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l7, l8, ((0 + pos^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l8, l3, (2 <= (0 + c2^0))>
<l8, l3, ((1 + c2^0) <= 1)>
<l8, l6, ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0))>
<l9, l7, (1 <= (0 + pos^0))>
<l9, l8, ((0 + pos^0) <= 0) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l10, l8, (1 <= (0 + z^0)), par{z^0 -> (~(1) + z^0)}>
<l10, l9, ((0 + z^0) <= 0)>
<l11, l10, (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1)>
<l12, l13, ((1 + lr^0) <= 1)>
<l12, l13, (1 <= (0 + lr^0)), par{rrep^0 -> 3}>
<l14, l12, (1 <= (0 + lr^0))>
<l14, l13, ((0 + lr^0) <= 0), par{rrep^0 -> 2}>
<l15, l12, (1 <= (0 + fr^0))>
<l15, l14, ((0 + fr^0) <= 0)>
<l16, l15, true>
<l13, l11, ((1 + r_ab^0) <= 1), par{r_ab^0 -> 1}>
<l13, l11, (1 <= (0 + r_ab^0)), par{r_ab^0 -> 0}>
<l17, l16, (1 <= (0 + lr^0))>
<l17, l16, ((1 + lr^0) <= 0)>
<l17, l13, ((0 + lr^0) <= 0) /\ (0 <= (0 + lr^0)), par{rrep^0 -> 1}>
<l18, l15, ((0 + fr^0) <= 0) /\ (0 <= (0 + fr^0))>
<l18, l17, (1 <= (0 + fr^0))>
<l18, l17, ((1 + fr^0) <= 0)>
<l19, l11, ((1 + br^0) <= (0 + r_ab^0))>
<l19, l11, ((1 + r_ab^0) <= (0 + br^0))>
<l19, l18, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0))>
<l20, l19, true, par{recv^0 -> 1}>
<l21, l20, (1 <= (0 + recv^0))>
<l21, l20, ((0 + recv^0) <= 0), par{r_ab^0 -> (0 + br^0)}>
<l22, l23, (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l22, l23, ((0 + pos^0) <= 1) /\ (1 <= (0 + c1^0)), par{pos^0 -> (1 + pos^0)}>
<l23, l3, ((1 + c1^0) <= 1)>
<l23, l21, (1 <= (0 + c1^0)), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0)}>
<l24, l22, (1 <= (0 + pos^0))>
<l24, l23, ((0 + pos^0) <= 0) /\ (1 <= (0 + c1^0)), par{pos^0 -> (1 + pos^0)}>
<l25, l23, (1 <= (0 + z^0)), par{z^0 -> (~(1) + z^0)}>
<l25, l24, ((0 + z^0) <= 0)>
<l26, l1, (0 <= (0 + z^0)) /\ (1 <= (0 + N^0)), par{i^0 -> 0, next^0 -> 1, pos^0 -> 0}>
<l4, l25, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1)>
<l27, l4, true, par{bs^0 -> (0 + s_ab^0)}>
<l28, l27, ((1 + i^0) <= (~(1) + N^0)), par{ls^0 -> 0}>
<l28, l27, ((~(1) + N^0) <= (0 + i^0)), par{ls^0 -> 1}>
<l29, l28, (1 <= (0 + i^0)), par{fs^0 -> 0}>
<l29, l28, ((0 + i^0) <= 0), par{fs^0 -> 1}>
<l2, l30, ((0 + N^0) <= (0 + i^0))>
<l2, l29, ((1 + i^0) <= (0 + N^0))>
<l31, l26, true>

Fresh variables:

Undef variables:

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l4, (i^0 = 0) /\ (next^0 = 1) /\ (pos^0 = 0) /\ (0 <= (0 + z^0)) /\ (1 <= (0 + N^0)) /\ ((1 + 0) <= (0 + N^0)) /\ ((0 + 0) <= 0) /\ ((1 + 0) <= (~(1) + N^0)), par{bs^0 -> (0 + s_ab^0), fs^0 -> 1, ls^0 -> 0}>
<l0, l4, (i^0 = 0) /\ (next^0 = 1) /\ (pos^0 = 0) /\ (0 <= (0 + z^0)) /\ (1 <= (0 + N^0)) /\ ((1 + 0) <= (0 + N^0)) /\ ((0 + 0) <= 0) /\ ((~(1) + N^0) <= (0 + 0)), par{bs^0 -> (0 + s_ab^0), fs^0 -> 1, ls^0 -> 1}>
<l4, l4, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((1 + c1^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)), par{z^0 -> (~(1) + z^0)}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ (1 <= (0 + z^0)) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + recv^0)), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), recv^0 -> 1, z^0 -> (~(1) + z^0)}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ (1 <= (0 + z^0)) /\ (1 <= (0 + c1^0)) /\ ((0 + recv^0) <= 0), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), r_ab^0 -> (0 + (0 + bs^0)), recv^0 -> 1, z^0 -> (~(1) + z^0)}>
<l4, l4, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((1 + c1^0) <= 1) /\ ((1 + (1 + next^0)) <= (1 + N^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + recv^0)), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), next^0 -> (1 + next^0), pos^0 -> 0, recv^0 -> 1}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ (1 <= (0 + c1^0)) /\ ((0 + recv^0) <= 0), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), next^0 -> (1 + next^0), pos^0 -> 0, r_ab^0 -> (0 + (0 + bs^0)), recv^0 -> 1}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + recv^0)), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), pos^0 -> (1 + pos^0), recv^0 -> 1}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + c1^0)) /\ ((0 + recv^0) <= 0), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), pos^0 -> (1 + pos^0), r_ab^0 -> (0 + (0 + bs^0)), recv^0 -> 1}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + recv^0)), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), pos^0 -> (1 + pos^0), recv^0 -> 1}>
<l4, l19, (0 <= (0 + c1^0)) /\ ((0 + c1^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c1^0)) /\ (1 <= (0 + c1^0)) /\ ((0 + recv^0) <= 0), par{br^0 -> (0 + bs^0), fr^0 -> (0 + fs^0), lr^0 -> (0 + ls^0), pos^0 -> (1 + pos^0), r_ab^0 -> (0 + (0 + bs^0)), recv^0 -> 1}>
<l6, l30, ((1 + s_ab^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)) /\ ((0 + N^0) <= (0 + (1 + i^0))), par{i^0 -> (1 + i^0), s_ab^0 -> 1}>
<l6, l4, ((1 + s_ab^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ (1 <= (0 + (1 + i^0))) /\ ((1 + (1 + i^0)) <= (~(1) + N^0)), par{bs^0 -> (0 + 1), fs^0 -> 0, i^0 -> (1 + i^0), ls^0 -> 0, s_ab^0 -> 1}>
<l6, l4, ((1 + s_ab^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ (1 <= (0 + (1 + i^0))) /\ ((~(1) + N^0) <= (0 + (1 + i^0))), par{bs^0 -> (0 + 1), fs^0 -> 0, i^0 -> (1 + i^0), ls^0 -> 1, s_ab^0 -> 1}>
<l6, l4, ((1 + s_ab^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ ((0 + (1 + i^0)) <= 0) /\ ((1 + (1 + i^0)) <= (~(1) + N^0)), par{bs^0 -> (0 + 1), fs^0 -> 1, i^0 -> (1 + i^0), ls^0 -> 0, s_ab^0 -> 1}>
<l6, l4, ((1 + s_ab^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ ((0 + (1 + i^0)) <= 0) /\ ((~(1) + N^0) <= (0 + (1 + i^0))), par{bs^0 -> (0 + 1), fs^0 -> 1, i^0 -> (1 + i^0), ls^0 -> 1, s_ab^0 -> 1}>
<l6, l30, (1 <= (0 + s_ab^0)) /\ ((1 + next^0) <= (1 + N^0)) /\ ((0 + N^0) <= (0 + (1 + i^0))), par{i^0 -> (1 + i^0), s_ab^0 -> 0}>
<l6, l4, (1 <= (0 + s_ab^0)) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ (1 <= (0 + (1 + i^0))) /\ ((1 + (1 + i^0)) <= (~(1) + N^0)), par{bs^0 -> (0 + 0), fs^0 -> 0, i^0 -> (1 + i^0), ls^0 -> 0, s_ab^0 -> 0}>
<l6, l4, (1 <= (0 + s_ab^0)) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ (1 <= (0 + (1 + i^0))) /\ ((~(1) + N^0) <= (0 + (1 + i^0))), par{bs^0 -> (0 + 0), fs^0 -> 0, i^0 -> (1 + i^0), ls^0 -> 1, s_ab^0 -> 0}>
<l6, l4, (1 <= (0 + s_ab^0)) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ ((0 + (1 + i^0)) <= 0) /\ ((1 + (1 + i^0)) <= (~(1) + N^0)), par{bs^0 -> (0 + 0), fs^0 -> 1, i^0 -> (1 + i^0), ls^0 -> 0, s_ab^0 -> 0}>
<l6, l4, (1 <= (0 + s_ab^0)) /\ ((1 + next^0) <= (1 + N^0)) /\ ((1 + (1 + i^0)) <= (0 + N^0)) /\ ((0 + (1 + i^0)) <= 0) /\ ((~(1) + N^0) <= (0 + (1 + i^0))), par{bs^0 -> (0 + 0), fs^0 -> 1, i^0 -> (1 + i^0), ls^0 -> 1, s_ab^0 -> 0}>
<l13, l4, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)), par{r_ab^0 -> 1, z^0 -> (~(1) + z^0)}>
<l13, l6, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{r_ab^0 -> 1, z^0 -> (~(1) + z^0)}>
<l13, l4, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + (1 + next^0)) <= (1 + N^0)), par{next^0 -> (1 + next^0), pos^0 -> 0, r_ab^0 -> 1}>
<l13, l6, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{next^0 -> (1 + next^0), pos^0 -> 0, r_ab^0 -> 1}>
<l13, l6, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0), r_ab^0 -> 1}>
<l13, l6, ((1 + r_ab^0) <= 1) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0), r_ab^0 -> 1}>
<l13, l4, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)), par{r_ab^0 -> 0, z^0 -> (~(1) + z^0)}>
<l13, l6, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{r_ab^0 -> 0, z^0 -> (~(1) + z^0)}>
<l13, l4, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + (1 + next^0)) <= (1 + N^0)), par{next^0 -> (1 + next^0), pos^0 -> 0, r_ab^0 -> 0}>
<l13, l6, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{next^0 -> (1 + next^0), pos^0 -> 0, r_ab^0 -> 0}>
<l13, l6, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0), r_ab^0 -> 0}>
<l13, l6, (1 <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0), r_ab^0 -> 0}>
<l15, l13, (1 <= (0 + fr^0)) /\ ((1 + lr^0) <= 1)>
<l15, l13, (1 <= (0 + fr^0)) /\ (1 <= (0 + lr^0))>
<l15, l13, ((0 + fr^0) <= 0) /\ (1 <= (0 + lr^0)) /\ (1 <= (0 + lr^0))>
<l15, l13, ((0 + fr^0) <= 0) /\ ((0 + lr^0) <= 0)>
<l19, l4, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)), par{z^0 -> (~(1) + z^0)}>
<l19, l6, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{z^0 -> (~(1) + z^0)}>
<l19, l4, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + (1 + next^0)) <= (1 + N^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l19, l6, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l19, l6, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l19, l6, ((1 + br^0) <= (0 + r_ab^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l19, l4, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + next^0) <= (1 + N^0)), par{z^0 -> (~(1) + z^0)}>
<l19, l6, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{z^0 -> (~(1) + z^0)}>
<l19, l4, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((1 + c2^0) <= 1) /\ ((1 + (1 + next^0)) <= (1 + N^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l19, l6, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ (2 <= (0 + pos^0)) /\ (0 <= (0 + z^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{next^0 -> (1 + next^0), pos^0 -> 0}>
<l19, l6, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ (1 <= (0 + pos^0)) /\ ((0 + pos^0) <= 1) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l19, l6, ((1 + r_ab^0) <= (0 + br^0)) /\ (0 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ ((0 + z^0) <= 0) /\ ((0 + pos^0) <= 0) /\ (1 <= (0 + c2^0)) /\ ((0 + c2^0) <= 1) /\ (1 <= (0 + c2^0)), par{pos^0 -> (1 + pos^0)}>
<l19, l15, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ ((0 + fr^0) <= 0) /\ (0 <= (0 + fr^0))>
<l19, l15, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ (1 <= (0 + fr^0)) /\ (1 <= (0 + lr^0))>
<l19, l15, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ (1 <= (0 + fr^0)) /\ ((1 + lr^0) <= 0)>
<l19, l13, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ (1 <= (0 + fr^0)) /\ ((0 + lr^0) <= 0) /\ (0 <= (0 + lr^0))>
<l19, l15, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ ((1 + fr^0) <= 0) /\ (1 <= (0 + lr^0))>
<l19, l15, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ ((1 + fr^0) <= 0) /\ ((1 + lr^0) <= 0)>
<l19, l13, ((0 + r_ab^0) <= (0 + br^0)) /\ ((0 + br^0) <= (0 + r_ab^0)) /\ ((1 + fr^0) <= 0) /\ ((0 + lr^0) <= 0) /\ (0 <= (0 + lr^0))>

Fresh variables:

Undef variables:

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l4, l4, 1 <= z^0 /\ next^0 <= N^0 /\ c1^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 1 <= z^0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, recv^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l4, l19, 1 <= z^0 /\ recv^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, r_ab^0 -> bs^0, recv^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l4, l4, 1 + next^0 <= N^0 /\ 2 <= pos^0 /\ c1^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 + i^0 <= 0 /\ next^0 <= N^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 + i^0 <= 0 /\ next^0 <= N^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 + i^0 <= 0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 + i^0 <= 0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= z^0 /\ r_ab^0 <= 0 /\ c2^0 = 1, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 1 <= z^0 /\ c2^0 = 1, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l15, br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, c1^0, next^0, z^0, br^0, bs^0, fr^0, fs^0, lr^0, ls^0, recv^0, r_ab^0, pos^0, i^0, s_ab^0, c2^0

Graph 2:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l4, 0 <= z^0 /\ 2 <= N^0 /\ i^0 = 0 /\ pos^0 = 0 /\ next^0 = 1, {bs^0 -> s_ab^0, fs^0 -> 1, ls^0 -> 0, rest remain the same}>
<l0, l4, 0 <= z^0 /\ i^0 = 0 /\ pos^0 = 0 /\ N^0 = 1 /\ next^0 = 1, {bs^0 -> s_ab^0, fs^0 -> 1, ls^0 -> 1, rest remain the same}>

Graph 2
<l6, l30, next^0 <= N^0 /\ s_ab^0 <= 0 /\ N^0 <= 1 + i^0, {i^0 -> 1 + i^0, s_ab^0 -> 1, rest remain the same}>
<l6, l30, 1 <= s_ab^0 /\ next^0 <= N^0 /\ N^0 <= 1 + i^0, {i^0 -> 1 + i^0, s_ab^0 -> 0, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 4 , 1 )
( 6 , 1 )
( 13 , 1 )
( 15 , 1 )
( 19 , 1 )
( 30 , 2 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 2.62817
Some transition disabled by a set of invariant(s):
Invariant at l4: 0 <= i^0
Invariant at l6: 0 <= i^0
Invariant at l13: 0 <= i^0
Invariant at l15: 0 <= i^0
Invariant at l19: 0 <= i^0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l6, l4, 1 + i^0 <= 0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c1^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 1 <= recv^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, recv^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 1 <= z^0 /\ 0 <= i^0 /\ recv^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, r_ab^0 -> bs^0, recv^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c1^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l6, l4, 1 + i^0 <= 0 /\ next^0 <= N^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l6, l4, 1 + i^0 <= 0 /\ next^0 <= N^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l6, l4, 1 + i^0 <= 0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 1, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 1 <= z^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 1 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Checking unfeasibility...
Time used: 4.00049

Checking conditional termination of SCC {l4, l6, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.034826s
Ranking function: -9 + 4*c1^0 + 5*z^0
New Graphs: 
Transitions:
<l4, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c1^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l4, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c1^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= z^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l6, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.021745s
Ranking function: -11 + N^0 - c1^0 - next^0 + 11*z^0
New Graphs: 
Transitions:
<l4, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c1^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= z^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l6, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.020248s
Ranking function: -8 + 8*N^0 - c1^0 - 8*next^0 + z^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 3 + i^0 <= N^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l6, l4, next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ 3 + i^0 <= N^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l6, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= z^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l6, 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l13, l6, 1 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, r_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ 0 <= i^0 /\ c2^0 = 1, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l6, 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1, {pos^0 -> 1 + pos^0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l6, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.019178s
Ranking function: -24 + 9*N^0 - 2*i^0 - next^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 0, {r_ab^0 -> 1, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {r_ab^0 -> 0, z^0 -> -1 + z^0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 0, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 0, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 0, {z^0 -> -1 + z^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.061518s
Ranking function: -4 + N^0 - 11*c2^0 - next^0 + 4*z^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l13, l4, 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 0, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, r_ab^0 -> 0, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 1, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 1 <= z^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, s_ab^0 -> 0, z^0 -> ((0 + ~(1)) + 0) + z^0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.053148s
Ranking function: -15 + 3*N^0 - 2*i^0 - next^0 + 11*z^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ c2^0 = 0 /\ z^0 = 0, {next^0 -> 1 + next^0, pos^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.033933s
Ranking function: -4 + 4*N^0 - 13*c2^0 - 4*next^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 + next^0 <= N^0 /\ 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + next^0 <= N^0 /\ 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, next^0 -> ((0 + 1) + 0) + next^0, pos^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.035369s
Ranking function: -13 + 11*N^0 - 2*i^0 - 9*next^0
New Graphs: 
Transitions:
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ 2 <= pos^0 /\ z^0 = 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, next^0 -> 1 + next^0, pos^0 -> 0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1 /\ pos^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 1 <= recv^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, recv^0 -> 1, rest remain the same}>
<l4, l19, 0 <= i^0 /\ pos^0 <= 0 /\ recv^0 <= 0 /\ z^0 <= 0 /\ c1^0 = 1, {br^0 -> bs^0, fr^0 -> fs^0, lr^0 -> ls^0, pos^0 -> 1 + pos^0, r_ab^0 -> bs^0, recv^0 -> 1, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ r_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 1, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 1, rest remain the same}>
<l13, l4, 1 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, r_ab^0 -> 0, s_ab^0 -> 0, rest remain the same}>
<l15, l13, 1 <= fr^0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l15, l13, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, 1 <= lr^0 /\ fr^0 <= 0 /\ 0 <= i^0, {all remain the same}>
<l15, l13, fr^0 <= 0 /\ 0 <= i^0 /\ lr^0 <= 0, {all remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + br^0 <= r_ab^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ z^0 <= 0 /\ c2^0 = 1 /\ pos^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ s_ab^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 1, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 1, rest remain the same}>
<l19, l4, 1 + r_ab^0 <= br^0 /\ 1 <= s_ab^0 /\ next^0 <= N^0 /\ 0 <= i^0 /\ pos^0 <= 0 /\ z^0 <= 0 /\ c2^0 = 1 /\ N^0 = 2 + i^0, {bs^0 -> 0, fs^0 -> 0, i^0 -> 1 + i^0, ls^0 -> 1, pos^0 -> ((0 + 1) + 0) + pos^0, s_ab^0 -> 0, rest remain the same}>
<l19, l15, 0 <= i^0 /\ br^0 = r_ab^0 /\ fr^0 = 0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 <= fr^0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 <= fr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 <= lr^0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l15, 1 + fr^0 <= 0 /\ 1 + lr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0, {all remain the same}>
<l19, l13, 1 + fr^0 <= 0 /\ 0 <= i^0 /\ br^0 = r_ab^0 /\ lr^0 = 0, {all remain the same}>
Variables:
N^0, br^0, bs^0, c1^0, c2^0, fr^0, fs^0, i^0, lr^0, ls^0, next^0, pos^0, r_ab^0, recv^0, s_ab^0, z^0
Checking conditional termination of SCC {l4, l13, l15, l19}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.017893s
Ranking function: -5 + (7 / 2)*N^0 - 2*i^0 - next^0
New Graphs: 
Proving termination of subgraph 2
Analyzing SCC {l30}...
No cycles found.

Program Terminates