NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l89, true>
<l1, l2, ((0 + CurrentWaitIrp^0) <= 0) /\ (0 <= (0 + CurrentWaitIrp^0))>
<l1, l3, (1 <= (0 + CurrentWaitIrp^0))>
<l1, l3, ((1 + CurrentWaitIrp^0) <= 0)>
<l4, l1, (undef337 = 1), par{i1212^0 -> (0 + OldIrql^0), keR^0 -> 0}>
<l5, l4, ((0 + ___rho_7_^0) <= 0), par{status^0 -> 7, x1010^0 -> (0 + Irp^0)}>
<l5, l4, (1 <= (0 + ___rho_7_^0)), par{status^0 -> 1}>
<l6, l5, (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550), par{CurrentWaitIrp^0 -> undef508, ___rho_7_^0 -> undef550, keA^0 -> 0}>
<l7, l6, ((0 + ___rho_6_^0) <= 0)>
<l7, l6, (1 <= (0 + ___rho_6_^0)), par{status^0 -> 4}>
<l8, l9, ((0 + ___rho_5_^0) <= 0)>
<l8, l7, (1 <= (0 + ___rho_5_^0)) /\ (undef886 = undef886), par{CurrentWaitIrp^0 -> 0, ___rho_6_^0 -> undef886}>
<l10, l2, true, par{x66^0 -> (0 + CurrentWaitIrp^0), y77^0 -> 2}>
<l11, l2, ((0 + CurrentWaitIrp^0) <= 0) /\ (0 <= (0 + CurrentWaitIrp^0))>
<l11, l10, (1 <= (0 + CurrentWaitIrp^0))>
<l11, l10, ((1 + CurrentWaitIrp^0) <= 0)>
<l12, l11, ((0 + ___rho_4_^0) <= 0) /\ (undef1347 = 1) /\ (undef1272 = undef1272) /\ (undef1348 = 1), par{NewMask^0 -> undef1272, i55^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l12, l2, (1 <= (0 + ___rho_4_^0)), par{status^0 -> 4}>
<l13, l8, ((0 + ___rho_3_^0) <= 0)>
<l13, l12, (1 <= (0 + ___rho_3_^0)) /\ (undef1526 = undef1526) /\ (undef1558 = undef1558), par{CurrentWaitIrp^0 -> 0, NewMask^0 -> undef1526, ___rho_4_^0 -> undef1558}>
<l2, l14, ((0 + status^0) <= 7) /\ (7 <= (0 + status^0))>
<l2, l15, (8 <= (0 + status^0))>
<l2, l15, ((1 + status^0) <= 7)>
<l16, l2, ((0 + ___rho_2_^0) <= 0)>
<l16, l2, (1 <= (0 + ___rho_2_^0)), par{status^0 -> 4}>
<l17, l13, ((0 + ___rho_1_^0) <= 0)>
<l17, l16, (1 <= (0 + ___rho_1_^0)) /\ (undef2139 = undef2139), par{___rho_2_^0 -> undef2139}>
<l18, l19, true>
<l19, l18, true>
<l20, l21, true>
<l14, l22, true, par{x6565^0 -> (0 + DeviceObject^0)}>
<l23, l14, true, par{x6363^0 -> (0 + Irp^0), y6464^0 -> (0 + status^0)}>
<l15, l14, ((0 + Irp^0) <= 0) /\ (0 <= (0 + Irp^0))>
<l15, l23, (1 <= (0 + Irp^0))>
<l15, l23, ((1 + Irp^0) <= 0)>
<l24, l2, ((0 + ___rho_22_^0) <= 0), par{status^0 -> 41}>
<l24, l2, (1 <= (0 + ___rho_22_^0))>
<l25, l2, (undef3113 = 1) /\ (undef3114 = 1), par{i6262^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l26, l25, ((0 + ___rho_34_^0) <= 0)>
<l26, l25, (1 <= (0 + ___rho_34_^0)), par{status^0 -> 4}>
<l27, l24, ((0 + ___rho_21_^0) <= 0)>
<l27, l26, (1 <= (0 + ___rho_21_^0)) /\ (undef3406 = undef3406), par{___rho_34_^0 -> undef3406}>
<l28, l29, true, par{status^0 -> 15}>
<l30, l29, true, par{LStop^0 -> 33}>
<l31, l30, (28 <= (0 + LData^0))>
<l31, l30, ((1 + LData^0) <= 27)>
<l31, l30, ((0 + LData^0) <= 27) /\ (27 <= (0 + LData^0)), par{status^0 -> 15}>
<l32, l28, (30 <= (0 + ___rho_33_^0))>
<l32, l28, ((1 + ___rho_33_^0) <= 29)>
<l32, l31, ((0 + ___rho_33_^0) <= 29) /\ (29 <= (0 + ___rho_33_^0))>
<l33, l29, true, par{LStop^0 -> 37}>
<l34, l33, true, par{status^0 -> 15}>
<l35, l33, ((0 + LData^0) <= 27) /\ (27 <= (0 + LData^0))>
<l35, l34, (28 <= (0 + LData^0))>
<l35, l34, ((1 + LData^0) <= 27)>
<l36, l32, (37 <= (0 + ___rho_33_^0))>
<l36, l32, ((1 + ___rho_33_^0) <= 36)>
<l36, l35, ((0 + ___rho_33_^0) <= 36) /\ (36 <= (0 + ___rho_33_^0))>
<l29, l2, (undef4879 = 1) /\ (undef4880 = 1), par{i5858^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l37, l36, (29 <= (0 + ___rho_33_^0))>
<l37, l36, ((1 + ___rho_33_^0) <= 28)>
<l37, l29, ((0 + ___rho_33_^0) <= 28) /\ (28 <= (0 + ___rho_33_^0)), par{LStop^0 -> 32}>
<l38, l39, true, par{status^0 -> 15}>
<l40, l38, (37 <= (0 + ___rho_32_^0))>
<l40, l38, ((1 + ___rho_32_^0) <= 36)>
<l40, l39, ((0 + ___rho_32_^0) <= 36) /\ (36 <= (0 + ___rho_32_^0)), par{LParity^0 -> 37}>
<l41, l40, (35 <= (0 + ___rho_32_^0))>
<l41, l40, ((1 + ___rho_32_^0) <= 34)>
<l41, l39, ((0 + ___rho_32_^0) <= 34) /\ (34 <= (0 + ___rho_32_^0)), par{LParity^0 -> 35}>
<l42, l41, (33 <= (0 + ___rho_32_^0))>
<l42, l41, ((1 + ___rho_32_^0) <= 32)>
<l42, l39, ((0 + ___rho_32_^0) <= 32) /\ (32 <= (0 + ___rho_32_^0)), par{LParity^0 -> 33}>
<l43, l42, (31 <= (0 + ___rho_32_^0))>
<l43, l42, ((1 + ___rho_32_^0) <= 30)>
<l43, l39, ((0 + ___rho_32_^0) <= 30) /\ (30 <= (0 + ___rho_32_^0)), par{LParity^0 -> 31}>
<l39, l37, (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l44, l43, (29 <= (0 + ___rho_32_^0))>
<l44, l43, ((1 + ___rho_32_^0) <= 28)>
<l44, l39, ((0 + ___rho_32_^0) <= 28) /\ (28 <= (0 + ___rho_32_^0)), par{LParity^0 -> 29}>
<l45, l46, true>
<l47, l48, true>
<l49, l50, true, par{status^0 -> 15}>
<l51, l49, (9 <= (0 + ___rho_31_^0))>
<l51, l49, ((1 + ___rho_31_^0) <= 8)>
<l51, l50, ((0 + ___rho_31_^0) <= 8) /\ (8 <= (0 + ___rho_31_^0)), par{LData^0 -> 26}>
<l52, l51, (8 <= (0 + ___rho_31_^0))>
<l52, l51, ((1 + ___rho_31_^0) <= 7)>
<l52, l50, ((0 + ___rho_31_^0) <= 7) /\ (7 <= (0 + ___rho_31_^0)), par{LData^0 -> 25, Mask^0 -> 127}>
<l53, l52, (7 <= (0 + ___rho_31_^0))>
<l53, l52, ((1 + ___rho_31_^0) <= 6)>
<l53, l50, ((0 + ___rho_31_^0) <= 6) /\ (6 <= (0 + ___rho_31_^0)), par{LData^0 -> 24, Mask^0 -> 63}>
<l50, l44, (undef7606 = undef7606), par{___rho_32_^0 -> undef7606}>
<l46, l17, (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679), par{___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_1_^0 -> undef7676, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_3_^0 -> undef7693, ___rho_5_^0 -> undef7695, ___rho_8_^0 -> undef7698}>
<l54, l53, (6 <= (0 + ___rho_31_^0))>
<l54, l53, ((1 + ___rho_31_^0) <= 5)>
<l54, l50, ((0 + ___rho_31_^0) <= 5) /\ (5 <= (0 + ___rho_31_^0)), par{LData^0 -> 27, Mask^0 -> 31}>
<l55, l54, (undef8025 = undef8025), par{___rho_31_^0 -> undef8025}>
<l56, l55, ((0 + ___rho_30_^0) <= 0)>
<l56, l55, (1 <= (0 + ___rho_30_^0)), par{status^0 -> 4}>
<l57, l27, ((0 + ___rho_20_^0) <= 0)>
<l57, l56, (1 <= (0 + ___rho_20_^0)) /\ (undef8394 = undef8394) /\ (undef8360 = undef8360), par{LData^0 -> 0, LParity^0 -> 0, LStop^0 -> 0, Mask^0 -> 255, ___rho_30_^0 -> undef8360, pLineControl^0 -> undef8394}>
<l58, l2, ((0 + ___rho_29_^0) <= 0) /\ (undef8493 = 1) /\ (undef8494 = 1), par{i5454^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l58, l2, (1 <= (0 + ___rho_29_^0)), par{status^0 -> 4}>
<l59, l57, ((0 + ___rho_19_^0) <= 0)>
<l59, l58, (1 <= (0 + ___rho_19_^0)) /\ (undef8731 = undef8731) /\ (undef8696 = undef8696), par{___rho_29_^0 -> undef8696, pBaudRate^0 -> undef8731}>
<l60, l46, (2 <= (0 + status^0)) /\ ((0 + status^0) <= 2)>
<l60, l18, ((1 + status^0) <= 2)>
<l60, l18, (3 <= (0 + status^0))>
<l61, l2, ((0 + ___rho_28_^0) <= 0) /\ (undef9083 = 1) /\ (undef9084 = 1), par{i5050^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l61, l2, (1 <= (0 + ___rho_28_^0)), par{status^0 -> 4}>
<l62, l59, ((0 + ___rho_18_^0) <= 0)>
<l62, l61, (1 <= (0 + ___rho_18_^0)) /\ (undef9285 = undef9285), par{___rho_28_^0 -> undef9285}>
<l63, l2, ((0 + ___rho_27_^0) <= 0)>
<l63, l2, (1 <= (0 + ___rho_27_^0)), par{status^0 -> 4}>
<l64, l62, ((0 + ___rho_17_^0) <= 0)>
<l64, l63, (1 <= (0 + ___rho_17_^0)) /\ (undef9620 = undef9620), par{___rho_27_^0 -> undef9620}>
<l65, l64, ((0 + ___rho_16_^0) <= 0)>
<l65, l2, (1 <= (0 + ___rho_16_^0)) /\ (undef9841 = 1) /\ (undef9842 = 1), par{i4545^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0, x4646^0 -> (0 + DeviceObject^0)}>
<l66, l2, (undef9927 = 1) /\ (undef9928 = 1), par{i4141^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l67, l66, ((0 + ___rho_26_^0) <= 0)>
<l67, l66, (1 <= (0 + ___rho_26_^0)), par{status^0 -> 4}>
<l68, l65, ((0 + ___rho_15_^0) <= 0)>
<l68, l67, (1 <= (0 + ___rho_15_^0)) /\ (undef10193 = undef10193) /\ (undef10211 = undef10211), par{SerialStatus^0 -> undef10193, ___rho_26_^0 -> undef10211}>
<l22, l69, true>
<l69, l22, true>
<l70, l2, (undef10517 = 1) /\ (undef10518 = 1), par{i3737^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l71, l70, ((0 + ___rho_25_^0) <= 0)>
<l71, l70, (1 <= (0 + ___rho_25_^0)), par{status^0 -> 4}>
<l72, l68, ((0 + ___rho_14_^0) <= 0)>
<l72, l71, (1 <= (0 + ___rho_14_^0)) /\ (undef10800 = undef10800), par{___rho_25_^0 -> undef10800}>
<l73, l2, (undef10939 = 1) /\ (undef10940 = 1), par{i3333^0 -> (0 + OldIrql^0), keA^0 -> 0, keR^0 -> 0}>
<l74, l73, ((0 + ___rho_24_^0) <= 0)>
<l74, l73, (1 <= (0 + ___rho_24_^0)), par{status^0 -> 15}>
<l75, l74, (undef11137 = undef11137), par{___rho_24_^0 -> undef11137}>
<l76, l75, ((0 + ___rho_23_^0) <= 0)>
<l76, l75, (1 <= (0 + ___rho_23_^0)), par{status^0 -> 4}>
<l77, l72, ((0 + ___rho_13_^0) <= 0)>
<l77, l76, (1 <= (0 + ___rho_13_^0)) /\ (undef11455 = undef11455) /\ (undef11472 = undef11472), par{NewTimeouts^0 -> undef11455, ___rho_23_^0 -> undef11472}>
<l78, l2, ((0 + ___rho_13_^0) <= 0)>
<l78, l2, (1 <= (0 + ___rho_13_^0)), par{status^0 -> 4}>
<l79, l77, ((0 + ___rho_12_^0) <= 0)>
<l79, l78, (1 <= (0 + ___rho_12_^0)) /\ (undef11797 = undef11797), par{___rho_13_^0 -> undef11797}>
<l80, l2, true, par{x2828^0 -> (0 + CancelIrp^0), y2929^0 -> 11}>
<l81, l2, ((0 + CancelIrp^0) <= 0) /\ (0 <= (0 + CancelIrp^0))>
<l81, l80, (1 <= (0 + CancelIrp^0))>
<l81, l80, ((1 + CancelIrp^0) <= 0)>
<l82, l81, (undef12285 = 1), par{i2727^0 -> (0 + OldIrql^0), keR^0 -> 0}>
<l83, l82, ((0 + ___rho_11_^0) <= 0)>
<l83, l82, (1 <= (0 + ___rho_11_^0)) /\ (undef12370 = undef12370), par{CancelIrp^0 -> undef12370}>
<l84, l47, ((0 + ___rho_10_^0) <= 0) /\ (undef12539 = 1) /\ (undef12538 = 1), par{i2121^0 -> (0 + OldIrql^0), ip1919^0 -> (0 + CancelIrql^0), keA^0 -> 0, keR^0 -> 0, x2222^0 -> (0 + CancelIrp^0), y2323^0 -> 11}>
<l84, l47, (1 <= (0 + ___rho_10_^0)), par{ip1818^0 -> (0 + CancelIrql^0)}>
<l48, l84, (1 <= (0 + length^0)) /\ (undef12624 = undef12624) /\ (undef12637 = undef12637), par{CancelIrp^0 -> undef12624, ___rho_10_^0 -> undef12637, length^0 -> (~(1) + length^0)}>
<l48, l83, ((0 + length^0) <= 0) /\ (undef12722 = undef12722), par{CancelIrp^0 -> 0, ___rho_11_^0 -> undef12722}>
<l85, l2, ((0 + ___rho_91_^0) <= 0)>
<l85, l47, (1 <= (0 + ___rho_91_^0)) /\ (undef12960 = 1) /\ (undef12942 = undef12942), par{keA^0 -> 0, length^0 -> undef12942}>
<l86, l85, (undef13007 = undef13007), par{___rho_91_^0 -> undef13007}>
<l87, l86, ((0 + ___rho_9_^0) <= 0)>
<l87, l86, (1 <= (0 + ___rho_9_^0)), par{status^0 -> 4}>
<l9, l79, ((0 + ___rho_8_^0) <= 0)>
<l9, l87, (1 <= (0 + ___rho_8_^0)) /\ (undef13297 = undef13297) /\ (undef13305 = undef13305) /\ (undef13344 = undef13344), par{CancelIrp^0 -> undef13297, Mask^0 -> undef13305, ___rho_9_^0 -> undef13344}>
<l3, l2, true, par{x1313^0 -> (0 + CurrentWaitIrp^0), y1414^0 -> 2}>
<l88, l60, (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534), par{CancelIrql^0 -> undef13466, DeviceObject^0 -> undef13468, Irp^0 -> undef13469, LData^0 -> 0, LParity^0 -> 0, LStop^0 -> 0, Mask^0 -> 255, NewTimeouts^0 -> undef13475, SerialStatus^0 -> undef13477, csl^0 -> undef13513, irql^0 -> undef13528, keA^0 -> 0, keR^0 -> 0, length^0 -> undef13531, lock^0 -> undef13532, pBaudRate^0 -> undef13533, pLineControl^0 -> undef13534, status^0 -> undef13535}>
<l89, l88, true>

Fresh variables:
undef337, undef508, undef550, undef590, undef886, undef1272, undef1347, undef1348, undef1526, undef1558, undef2139, undef3113, undef3114, undef3406, undef4879, undef4880, undef6263, undef7606, undef7668, undef7669, undef7670, undef7671, undef7672, undef7673, undef7674, undef7675, undef7676, undef7677, undef7678, undef7679, undef7693, undef7695, undef7698, undef8025, undef8360, undef8394, undef8493, undef8494, undef8696, undef8731, undef9083, undef9084, undef9285, undef9620, undef9841, undef9842, undef9927, undef9928, undef10193, undef10211, undef10517, undef10518, undef10800, undef10939, undef10940, undef11137, undef11455, undef11472, undef11797, undef12285, undef12370, undef12538, undef12539, undef12624, undef12637, undef12722, undef12942, undef12960, undef13007, undef13297, undef13305, undef13344, undef13466, undef13468, undef13469, undef13475, undef13477, undef13513, undef13528, undef13531, undef13532, undef13533, undef13534, undef13535, undef13549, undef13550, undef13551, 

Undef variables:
undef337, undef508, undef550, undef590, undef886, undef1272, undef1347, undef1348, undef1526, undef1558, undef2139, undef3113, undef3114, undef3406, undef4879, undef4880, undef6263, undef7606, undef7668, undef7669, undef7670, undef7671, undef7672, undef7673, undef7674, undef7675, undef7676, undef7677, undef7678, undef7679, undef7693, undef7695, undef7698, undef8025, undef8360, undef8394, undef8493, undef8494, undef8696, undef8731, undef9083, undef9084, undef9285, undef9620, undef9841, undef9842, undef9927, undef9928, undef10193, undef10211, undef10517, undef10518, undef10800, undef10939, undef10940, undef11137, undef11455, undef11472, undef11797, undef12285, undef12370, undef12538, undef12539, undef12624, undef12637, undef12722, undef12942, undef12960, undef13007, undef13297, undef13305, undef13344, undef13466, undef13468, undef13469, undef13475, undef13477, undef13513, undef13528, undef13531, undef13532, undef13533, undef13534, undef13535, undef13549, undef13550, undef13551, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l9, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ ((0 + undef7676) <= 0) /\ ((0 + undef7693) <= 0) /\ ((0 + undef7695) <= 0), par{___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535}>
<l0, l7, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ ((0 + undef7676) <= 0) /\ ((0 + undef7693) <= 0) /\ (1 <= (0 + undef7695)) /\ (undef886 = undef886), par{CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_6_^0 -> undef886, ___rho_8_^0 -> undef7698, status^0 -> undef13535}>
<l0, l2, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ ((0 + undef7676) <= 0) /\ (1 <= (0 + undef7693)) /\ (undef1526 = undef1526) /\ (undef1558 = undef1558) /\ ((0 + undef1558) <= 0) /\ (undef1347 = 1) /\ (undef1272 = undef1272) /\ (undef1348 = 1) /\ ((0 + 0) <= 0) /\ (0 <= (0 + 0)), par{CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535}>
<l0, l2, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ ((0 + undef7676) <= 0) /\ (1 <= (0 + undef7693)) /\ (undef1526 = undef1526) /\ (undef1558 = undef1558) /\ (1 <= (0 + undef1558)), par{CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> 4}>
<l0, l2, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ (1 <= (0 + undef7676)) /\ (undef2139 = undef2139) /\ ((0 + undef2139) <= 0), par{___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535}>
<l0, l2, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (2 <= (0 + undef13535)) /\ ((0 + undef13535) <= 2) /\ (undef7676 = undef7676) /\ (undef7693 = undef7693) /\ (undef7695 = undef7695) /\ (undef7698 = undef7698) /\ (undef7668 = undef7668) /\ (undef7669 = undef7669) /\ (undef7670 = undef7670) /\ (undef7671 = undef7671) /\ (undef7672 = undef7672) /\ (undef7673 = undef7673) /\ (undef7674 = undef7674) /\ (undef7675 = undef7675) /\ (undef7677 = undef7677) /\ (undef7678 = undef7678) /\ (undef7679 = undef7679) /\ (1 <= (0 + undef7676)) /\ (undef2139 = undef2139) /\ (1 <= (0 + undef2139)), par{___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> 4}>
<l0, l18, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ ((1 + undef13535) <= 2), par{status^0 -> undef13535}>
<l0, l18, (CancelIrql^0 = undef13466) /\ (DeviceObject^0 = undef13468) /\ (Irp^0 = undef13469) /\ (LData^0 = 0) /\ (length^0 = undef13531) /\ (undef13550 = 0) /\ (undef13549 = (0 + undef13550)) /\ (undef13532 = undef13532) /\ (undef13466 = undef13466) /\ (undef13528 = undef13528) /\ (undef13513 = undef13513) /\ (undef13468 = undef13468) /\ (undef13469 = undef13469) /\ (undef13551 = 1) /\ (undef13535 = undef13535) /\ (undef13531 = undef13531) /\ (undef13475 = undef13475) /\ (undef13477 = undef13477) /\ (undef13533 = undef13533) /\ (undef13534 = undef13534) /\ (3 <= (0 + undef13535)), par{status^0 -> undef13535}>
<l2, l22, ((0 + status^0) <= 7) /\ (7 <= (0 + status^0))>
<l2, l15, (8 <= (0 + status^0))>
<l2, l15, ((1 + status^0) <= 7)>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ ((0 + undef508) <= 0) /\ (0 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ (1 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ ((1 + undef508) <= 0), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ ((0 + undef508) <= 0) /\ (0 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ (1 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l7, l2, ((0 + ___rho_6_^0) <= 0) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ ((1 + undef508) <= 0), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ ((0 + undef508) <= 0) /\ (0 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ (1 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ ((0 + undef550) <= 0) /\ (undef337 = 1) /\ ((1 + undef508) <= 0), par{CurrentWaitIrp^0 -> undef508, status^0 -> 7}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ ((0 + undef508) <= 0) /\ (0 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ (1 <= (0 + undef508)), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l7, l2, (1 <= (0 + ___rho_6_^0)) /\ (undef590 = 1) /\ (undef508 = undef508) /\ (undef550 = undef550) /\ (1 <= (0 + undef550)) /\ (undef337 = 1) /\ ((1 + undef508) <= 0), par{CurrentWaitIrp^0 -> undef508, status^0 -> 1}>
<l9, l65, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ ((0 + ___rho_13_^0) <= 0) /\ ((0 + ___rho_14_^0) <= 0) /\ ((0 + ___rho_15_^0) <= 0)>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ ((0 + ___rho_13_^0) <= 0) /\ ((0 + ___rho_14_^0) <= 0) /\ (1 <= (0 + ___rho_15_^0)) /\ (undef10193 = undef10193) /\ (undef10211 = undef10211) /\ ((0 + undef10211) <= 0) /\ (undef9927 = 1) /\ (undef9928 = 1), par{___rho_26_^0 -> undef10211}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ ((0 + ___rho_13_^0) <= 0) /\ ((0 + ___rho_14_^0) <= 0) /\ (1 <= (0 + ___rho_15_^0)) /\ (undef10193 = undef10193) /\ (undef10211 = undef10211) /\ (1 <= (0 + undef10211)) /\ (undef9927 = 1) /\ (undef9928 = 1), par{___rho_26_^0 -> undef10211, status^0 -> 4}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ ((0 + ___rho_13_^0) <= 0) /\ (1 <= (0 + ___rho_14_^0)) /\ (undef10800 = undef10800) /\ ((0 + undef10800) <= 0) /\ (undef10517 = 1) /\ (undef10518 = 1)>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ ((0 + ___rho_13_^0) <= 0) /\ (1 <= (0 + ___rho_14_^0)) /\ (undef10800 = undef10800) /\ (1 <= (0 + undef10800)) /\ (undef10517 = 1) /\ (undef10518 = 1), par{status^0 -> 4}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ (1 <= (0 + ___rho_13_^0)) /\ (undef11455 = undef11455) /\ (undef11472 = undef11472) /\ ((0 + undef11472) <= 0) /\ (undef11137 = undef11137) /\ ((0 + undef11137) <= 0) /\ (undef10939 = 1) /\ (undef10940 = 1)>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ (1 <= (0 + ___rho_13_^0)) /\ (undef11455 = undef11455) /\ (undef11472 = undef11472) /\ ((0 + undef11472) <= 0) /\ (undef11137 = undef11137) /\ (1 <= (0 + undef11137)) /\ (undef10939 = 1) /\ (undef10940 = 1), par{status^0 -> 15}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ (1 <= (0 + ___rho_13_^0)) /\ (undef11455 = undef11455) /\ (undef11472 = undef11472) /\ (1 <= (0 + undef11472)) /\ (undef11137 = undef11137) /\ ((0 + undef11137) <= 0) /\ (undef10939 = 1) /\ (undef10940 = 1), par{status^0 -> 4}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ ((0 + ___rho_12_^0) <= 0) /\ (1 <= (0 + ___rho_13_^0)) /\ (undef11455 = undef11455) /\ (undef11472 = undef11472) /\ (1 <= (0 + undef11472)) /\ (undef11137 = undef11137) /\ (1 <= (0 + undef11137)) /\ (undef10939 = 1) /\ (undef10940 = 1), par{status^0 -> 15}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ (1 <= (0 + ___rho_12_^0)) /\ (undef11797 = undef11797) /\ ((0 + undef11797) <= 0), par{___rho_13_^0 -> undef11797}>
<l9, l2, ((0 + ___rho_8_^0) <= 0) /\ (1 <= (0 + ___rho_12_^0)) /\ (undef11797 = undef11797) /\ (1 <= (0 + undef11797)), par{___rho_13_^0 -> undef11797, status^0 -> 4}>
<l9, l2, (1 <= (0 + ___rho_8_^0)) /\ (undef13297 = undef13297) /\ (undef13305 = undef13305) /\ (undef13344 = undef13344) /\ ((0 + undef13344) <= 0) /\ (undef13007 = undef13007) /\ ((0 + undef13007) <= 0)>
<l9, l47, (1 <= (0 + ___rho_8_^0)) /\ (undef13297 = undef13297) /\ (undef13305 = undef13305) /\ (undef13344 = undef13344) /\ ((0 + undef13344) <= 0) /\ (undef13007 = undef13007) /\ (1 <= (0 + undef13007)) /\ (undef12960 = 1) /\ (undef12942 = undef12942), par{length^0 -> undef12942}>
<l9, l2, (1 <= (0 + ___rho_8_^0)) /\ (undef13297 = undef13297) /\ (undef13305 = undef13305) /\ (undef13344 = undef13344) /\ (1 <= (0 + undef13344)) /\ (undef13007 = undef13007) /\ ((0 + undef13007) <= 0), par{status^0 -> 4}>
<l9, l47, (1 <= (0 + ___rho_8_^0)) /\ (undef13297 = undef13297) /\ (undef13305 = undef13305) /\ (undef13344 = undef13344) /\ (1 <= (0 + undef13344)) /\ (undef13007 = undef13007) /\ (1 <= (0 + undef13007)) /\ (undef12960 = 1) /\ (undef12942 = undef12942), par{length^0 -> undef12942, status^0 -> 4}>
<l15, l22, ((0 + Irp^0) <= 0) /\ (0 <= (0 + Irp^0))>
<l15, l22, (1 <= (0 + Irp^0))>
<l15, l22, ((1 + Irp^0) <= 0)>
<l18, l18, true>
<l22, l22, true>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ (37 <= (0 + ___rho_33_^0)) /\ (30 <= (0 + ___rho_33_^0)) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((1 + ___rho_33_^0) <= 36) /\ (30 <= (0 + ___rho_33_^0)) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((1 + ___rho_33_^0) <= 36) /\ ((0 + ___rho_33_^0) <= 29) /\ (29 <= (0 + ___rho_33_^0)) /\ (28 <= (0 + LData^0)) /\ (undef4879 = 1) /\ (undef4880 = 1)>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((1 + ___rho_33_^0) <= 36) /\ ((0 + ___rho_33_^0) <= 29) /\ (29 <= (0 + ___rho_33_^0)) /\ ((1 + LData^0) <= 27) /\ (undef4879 = 1) /\ (undef4880 = 1)>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((1 + ___rho_33_^0) <= 36) /\ ((0 + ___rho_33_^0) <= 29) /\ (29 <= (0 + ___rho_33_^0)) /\ ((0 + LData^0) <= 27) /\ (27 <= (0 + LData^0)) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((0 + ___rho_33_^0) <= 36) /\ (36 <= (0 + ___rho_33_^0)) /\ ((0 + LData^0) <= 27) /\ (27 <= (0 + LData^0)) /\ (undef4879 = 1) /\ (undef4880 = 1)>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((0 + ___rho_33_^0) <= 36) /\ (36 <= (0 + ___rho_33_^0)) /\ (28 <= (0 + LData^0)) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, (29 <= (0 + ___rho_33_^0)) /\ ((0 + ___rho_33_^0) <= 36) /\ (36 <= (0 + ___rho_33_^0)) /\ ((1 + LData^0) <= 27) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, ((1 + ___rho_33_^0) <= 28) /\ ((1 + ___rho_33_^0) <= 36) /\ ((1 + ___rho_33_^0) <= 29) /\ (undef4879 = 1) /\ (undef4880 = 1), par{status^0 -> 15}>
<l37, l2, ((0 + ___rho_33_^0) <= 28) /\ (28 <= (0 + ___rho_33_^0)) /\ (undef4879 = 1) /\ (undef4880 = 1)>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ (33 <= (0 + ___rho_32_^0)) /\ (35 <= (0 + ___rho_32_^0)) /\ (37 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ (33 <= (0 + ___rho_32_^0)) /\ (35 <= (0 + ___rho_32_^0)) /\ ((1 + ___rho_32_^0) <= 36) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ (33 <= (0 + ___rho_32_^0)) /\ (35 <= (0 + ___rho_32_^0)) /\ ((0 + ___rho_32_^0) <= 36) /\ (36 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ (33 <= (0 + ___rho_32_^0)) /\ ((1 + ___rho_32_^0) <= 34) /\ ((1 + ___rho_32_^0) <= 36) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ (33 <= (0 + ___rho_32_^0)) /\ ((0 + ___rho_32_^0) <= 34) /\ (34 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ ((1 + ___rho_32_^0) <= 32) /\ ((1 + ___rho_32_^0) <= 34) /\ ((1 + ___rho_32_^0) <= 36) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ (31 <= (0 + ___rho_32_^0)) /\ ((0 + ___rho_32_^0) <= 32) /\ (32 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ ((1 + ___rho_32_^0) <= 30) /\ ((1 + ___rho_32_^0) <= 32) /\ ((1 + ___rho_32_^0) <= 34) /\ ((1 + ___rho_32_^0) <= 36) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, (29 <= (0 + ___rho_32_^0)) /\ ((0 + ___rho_32_^0) <= 30) /\ (30 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l44, l37, ((1 + ___rho_32_^0) <= 28) /\ ((1 + ___rho_32_^0) <= 30) /\ ((1 + ___rho_32_^0) <= 32) /\ ((1 + ___rho_32_^0) <= 34) /\ ((1 + ___rho_32_^0) <= 36) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263, status^0 -> 15}>
<l44, l37, ((0 + ___rho_32_^0) <= 28) /\ (28 <= (0 + ___rho_32_^0)) /\ (undef6263 = undef6263), par{___rho_33_^0 -> undef6263}>
<l47, l47, (1 <= (0 + length^0)) /\ (undef12624 = undef12624) /\ (undef12637 = undef12637) /\ ((0 + undef12637) <= 0) /\ (undef12539 = 1) /\ (undef12538 = 1), par{length^0 -> (~(1) + length^0)}>
<l47, l47, (1 <= (0 + length^0)) /\ (undef12624 = undef12624) /\ (undef12637 = undef12637) /\ (1 <= (0 + undef12637)), par{length^0 -> (~(1) + length^0)}>
<l47, l2, ((0 + length^0) <= 0) /\ (undef12722 = undef12722) /\ ((0 + undef12722) <= 0) /\ (undef12285 = 1) /\ ((0 + 0) <= 0) /\ (0 <= (0 + 0))>
<l47, l2, ((0 + length^0) <= 0) /\ (undef12722 = undef12722) /\ (1 <= (0 + undef12722)) /\ (undef12370 = undef12370) /\ (undef12285 = 1) /\ ((0 + undef12370) <= 0) /\ (0 <= (0 + undef12370))>
<l47, l2, ((0 + length^0) <= 0) /\ (undef12722 = undef12722) /\ (1 <= (0 + undef12722)) /\ (undef12370 = undef12370) /\ (undef12285 = 1) /\ (1 <= (0 + undef12370))>
<l47, l2, ((0 + length^0) <= 0) /\ (undef12722 = undef12722) /\ (1 <= (0 + undef12722)) /\ (undef12370 = undef12370) /\ (undef12285 = 1) /\ ((1 + undef12370) <= 0)>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ (8 <= (0 + undef8025)) /\ (9 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15}>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ (8 <= (0 + undef8025)) /\ ((0 + undef8025) <= 8) /\ (8 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 26, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606}>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ ((0 + undef8025) <= 7) /\ (7 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 25, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606}>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ ((0 + undef8025) <= 6) /\ (6 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 24, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606}>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ ((1 + undef8025) <= 5) /\ ((1 + undef8025) <= 6) /\ ((1 + undef8025) <= 7) /\ ((1 + undef8025) <= 8) /\ (undef7606 = undef7606), par{___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15}>
<l56, l44, ((0 + ___rho_30_^0) <= 0) /\ (undef8025 = undef8025) /\ ((0 + undef8025) <= 5) /\ (5 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 27, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ (8 <= (0 + undef8025)) /\ (9 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ (8 <= (0 + undef8025)) /\ ((0 + undef8025) <= 8) /\ (8 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 26, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ (7 <= (0 + undef8025)) /\ ((0 + undef8025) <= 7) /\ (7 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 25, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ (6 <= (0 + undef8025)) /\ ((0 + undef8025) <= 6) /\ (6 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 24, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ ((1 + undef8025) <= 5) /\ ((1 + undef8025) <= 6) /\ ((1 + undef8025) <= 7) /\ ((1 + undef8025) <= 8) /\ (undef7606 = undef7606), par{___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15}>
<l56, l44, (1 <= (0 + ___rho_30_^0)) /\ (undef8025 = undef8025) /\ ((0 + undef8025) <= 5) /\ (5 <= (0 + undef8025)) /\ (undef7606 = undef7606), par{LData^0 -> 27, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4}>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ ((0 + ___rho_19_^0) <= 0) /\ ((0 + ___rho_20_^0) <= 0) /\ ((0 + ___rho_21_^0) <= 0) /\ ((0 + ___rho_22_^0) <= 0), par{status^0 -> 41}>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ ((0 + ___rho_19_^0) <= 0) /\ ((0 + ___rho_20_^0) <= 0) /\ ((0 + ___rho_21_^0) <= 0) /\ (1 <= (0 + ___rho_22_^0))>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ ((0 + ___rho_19_^0) <= 0) /\ ((0 + ___rho_20_^0) <= 0) /\ (1 <= (0 + ___rho_21_^0)) /\ (undef3406 = undef3406) /\ ((0 + undef3406) <= 0) /\ (undef3113 = 1) /\ (undef3114 = 1)>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ ((0 + ___rho_19_^0) <= 0) /\ ((0 + ___rho_20_^0) <= 0) /\ (1 <= (0 + ___rho_21_^0)) /\ (undef3406 = undef3406) /\ (1 <= (0 + undef3406)) /\ (undef3113 = 1) /\ (undef3114 = 1), par{status^0 -> 4}>
<l65, l56, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ ((0 + ___rho_19_^0) <= 0) /\ (1 <= (0 + ___rho_20_^0)) /\ (undef8394 = undef8394) /\ (undef8360 = undef8360), par{LData^0 -> 0, ___rho_30_^0 -> undef8360}>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ (1 <= (0 + ___rho_19_^0)) /\ (undef8731 = undef8731) /\ (undef8696 = undef8696) /\ ((0 + undef8696) <= 0) /\ (undef8493 = 1) /\ (undef8494 = 1)>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ ((0 + ___rho_18_^0) <= 0) /\ (1 <= (0 + ___rho_19_^0)) /\ (undef8731 = undef8731) /\ (undef8696 = undef8696) /\ (1 <= (0 + undef8696)), par{status^0 -> 4}>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ (1 <= (0 + ___rho_18_^0)) /\ (undef9285 = undef9285) /\ ((0 + undef9285) <= 0) /\ (undef9083 = 1) /\ (undef9084 = 1)>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ ((0 + ___rho_17_^0) <= 0) /\ (1 <= (0 + ___rho_18_^0)) /\ (undef9285 = undef9285) /\ (1 <= (0 + undef9285)), par{status^0 -> 4}>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ (1 <= (0 + ___rho_17_^0)) /\ (undef9620 = undef9620) /\ ((0 + undef9620) <= 0)>
<l65, l2, ((0 + ___rho_16_^0) <= 0) /\ (1 <= (0 + ___rho_17_^0)) /\ (undef9620 = undef9620) /\ (1 <= (0 + undef9620)), par{status^0 -> 4}>
<l65, l2, (1 <= (0 + ___rho_16_^0)) /\ (undef9841 = 1) /\ (undef9842 = 1)>

Fresh variables:
undef337, undef508, undef550, undef590, undef886, undef1272, undef1347, undef1348, undef1526, undef1558, undef2139, undef3113, undef3114, undef3406, undef4879, undef4880, undef6263, undef7606, undef7668, undef7669, undef7670, undef7671, undef7672, undef7673, undef7674, undef7675, undef7676, undef7677, undef7678, undef7679, undef7693, undef7695, undef7698, undef8025, undef8360, undef8394, undef8493, undef8494, undef8696, undef8731, undef9083, undef9084, undef9285, undef9620, undef9841, undef9842, undef9927, undef9928, undef10193, undef10211, undef10517, undef10518, undef10800, undef10939, undef10940, undef11137, undef11455, undef11472, undef11797, undef12285, undef12370, undef12538, undef12539, undef12624, undef12637, undef12722, undef12942, undef12960, undef13007, undef13297, undef13305, undef13344, undef13466, undef13468, undef13469, undef13475, undef13477, undef13513, undef13528, undef13531, undef13532, undef13533, undef13534, undef13535, undef13549, undef13550, undef13551, 

Undef variables:
undef337, undef508, undef550, undef590, undef886, undef1272, undef1347, undef1348, undef1526, undef1558, undef2139, undef3113, undef3114, undef3406, undef4879, undef4880, undef6263, undef7606, undef7668, undef7669, undef7670, undef7671, undef7672, undef7673, undef7674, undef7675, undef7676, undef7677, undef7678, undef7679, undef7693, undef7695, undef7698, undef8025, undef8360, undef8394, undef8493, undef8494, undef8696, undef8731, undef9083, undef9084, undef9285, undef9620, undef9841, undef9842, undef9927, undef9928, undef10193, undef10211, undef10517, undef10518, undef10800, undef10939, undef10940, undef11137, undef11455, undef11472, undef11797, undef12285, undef12370, undef12538, undef12539, undef12624, undef12637, undef12722, undef12942, undef12960, undef13007, undef13297, undef13305, undef13344, undef13466, undef13468, undef13469, undef13475, undef13477, undef13513, undef13528, undef13531, undef13532, undef13533, undef13534, undef13535, undef13549, undef13550, undef13551, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l18, l18, true, {all remain the same}>
Variables:

Graph 2:
Transitions:
Variables:

Graph 3:
Transitions:
Variables:

Graph 4:
Transitions:
<l47, l47, undef12637 <= 0 /\ 1 <= length^0 /\ undef12538 = 1 /\ undef12539 = 1, {length^0 -> -1 + length^0, rest remain the same}>
<l47, l47, 1 <= length^0 /\ 1 <= undef12637, {length^0 -> -1 + length^0, rest remain the same}>
Variables:
length^0

Graph 5:
Transitions:
Variables:

Graph 6:
Transitions:
Variables:

Graph 7:
Transitions:
Variables:

Graph 8:
Transitions:
Variables:

Graph 9:
Transitions:
Variables:

Graph 10:
Transitions:
Variables:

Graph 11:
Transitions:
<l22, l22, true, {all remain the same}>
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
<l0, l18, 3 <= undef13535 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>

Graph 2
<l0, l7, undef7676 <= 0 /\ undef7693 <= 0 /\ 1 <= undef7695 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1 /\ undef13535 = 2, {CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_6_^0 -> undef886, ___rho_8_^0 -> undef7698, status^0 -> undef13535, rest remain the same}>

Graph 3
<l0, l9, undef7676 <= 0 /\ undef7693 <= 0 /\ undef7695 <= 0 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1 /\ undef13535 = 2, {___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535, rest remain the same}>

Graph 4
<l9, l47, undef13344 <= 0 /\ 1 <= ___rho_8_^0 /\ 1 <= undef13007 /\ undef12960 = 1, {length^0 -> undef12942, rest remain the same}>
<l9, l47, 1 <= ___rho_8_^0 /\ 1 <= undef13007 /\ 1 <= undef13344 /\ undef12960 = 1, {length^0 -> undef12942, status^0 -> 4, rest remain the same}>

Graph 5
<l9, l65, ___rho_12_^0 <= 0 /\ ___rho_13_^0 <= 0 /\ ___rho_14_^0 <= 0 /\ ___rho_15_^0 <= 0 /\ ___rho_8_^0 <= 0, {all remain the same}>

Graph 6
<l65, l56, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ ___rho_19_^0 <= 0 /\ 1 <= ___rho_20_^0, {LData^0 -> 0, ___rho_30_^0 -> undef8360, rest remain the same}>

Graph 7
<l56, l44, ___rho_30_^0 <= 0 /\ 9 <= undef8025, {___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15, rest remain the same}>
<l56, l44, ___rho_30_^0 <= 0 /\ undef8025 = 8, {LData^0 -> 26, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, rest remain the same}>
<l56, l44, ___rho_30_^0 <= 0 /\ undef8025 = 7, {LData^0 -> 25, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, rest remain the same}>
<l56, l44, ___rho_30_^0 <= 0 /\ undef8025 = 6, {LData^0 -> 24, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, rest remain the same}>
<l56, l44, ___rho_30_^0 <= 0 /\ undef8025 <= 4, {___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15, rest remain the same}>
<l56, l44, ___rho_30_^0 <= 0 /\ undef8025 = 5, {LData^0 -> 27, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ 9 <= undef8025, {___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ undef8025 = 8, {LData^0 -> 26, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ undef8025 = 7, {LData^0 -> 25, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ undef8025 = 6, {LData^0 -> 24, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ undef8025 <= 4, {___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 15, rest remain the same}>
<l56, l44, 1 <= ___rho_30_^0 /\ undef8025 = 5, {LData^0 -> 27, ___rho_31_^0 -> undef8025, ___rho_32_^0 -> undef7606, status^0 -> 4, rest remain the same}>

Graph 8
<l44, l37, 37 <= ___rho_32_^0, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 35, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 36, {___rho_33_^0 -> undef6263, rest remain the same}>
<l44, l37, ___rho_32_^0 = 33, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 34, {___rho_33_^0 -> undef6263, rest remain the same}>
<l44, l37, ___rho_32_^0 = 31, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 32, {___rho_33_^0 -> undef6263, rest remain the same}>
<l44, l37, ___rho_32_^0 = 29, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 30, {___rho_33_^0 -> undef6263, rest remain the same}>
<l44, l37, ___rho_32_^0 <= 27, {___rho_33_^0 -> undef6263, status^0 -> 15, rest remain the same}>
<l44, l37, ___rho_32_^0 = 28, {___rho_33_^0 -> undef6263, rest remain the same}>

Graph 9
<l0, l2, undef1558 <= 0 /\ undef7676 <= 0 /\ 1 <= undef7693 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef1347 = 1 /\ undef1348 = 1 /\ undef13551 = 1 /\ undef13535 = 2, {CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535, rest remain the same}>
<l0, l2, undef7676 <= 0 /\ 1 <= undef1558 /\ 1 <= undef7693 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1 /\ undef13535 = 2, {CurrentWaitIrp^0 -> 0, ___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> 4, rest remain the same}>
<l0, l2, undef2139 <= 0 /\ 1 <= undef7676 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1 /\ undef13535 = 2, {___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> undef13535, rest remain the same}>
<l0, l2, 1 <= undef2139 /\ 1 <= undef7676 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1 /\ undef13535 = 2, {___rho_12_^0 -> undef7668, ___rho_13_^0 -> undef7669, ___rho_14_^0 -> undef7670, ___rho_15_^0 -> undef7671, ___rho_16_^0 -> undef7672, ___rho_17_^0 -> undef7673, ___rho_18_^0 -> undef7674, ___rho_19_^0 -> undef7675, ___rho_20_^0 -> undef7677, ___rho_21_^0 -> undef7678, ___rho_22_^0 -> undef7679, ___rho_8_^0 -> undef7698, status^0 -> 4, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ undef550 <= 0 /\ undef508 = 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ undef550 <= 0 /\ 1 <= undef508 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ undef550 <= 0 /\ 1 + undef508 <= 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ 1 <= undef550 /\ undef508 = 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ 1 <= undef508 /\ 1 <= undef550 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l7, l2, ___rho_6_^0 <= 0 /\ 1 + undef508 <= 0 /\ 1 <= undef550 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l7, l2, undef550 <= 0 /\ 1 <= ___rho_6_^0 /\ undef508 = 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, undef550 <= 0 /\ 1 <= ___rho_6_^0 /\ 1 <= undef508 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, undef550 <= 0 /\ 1 <= ___rho_6_^0 /\ 1 + undef508 <= 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 7, rest remain the same}>
<l7, l2, 1 <= ___rho_6_^0 /\ 1 <= undef550 /\ undef508 = 0 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l7, l2, 1 <= ___rho_6_^0 /\ 1 <= undef508 /\ 1 <= undef550 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l7, l2, 1 <= ___rho_6_^0 /\ 1 + undef508 <= 0 /\ 1 <= undef550 /\ undef337 = 1 /\ undef590 = 1, {CurrentWaitIrp^0 -> undef508, status^0 -> 1, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_13_^0 <= 0 /\ ___rho_14_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ undef10211 <= 0 /\ 1 <= ___rho_15_^0 /\ undef9927 = 1 /\ undef9928 = 1, {___rho_26_^0 -> undef10211, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_13_^0 <= 0 /\ ___rho_14_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ 1 <= ___rho_15_^0 /\ 1 <= undef10211 /\ undef9927 = 1 /\ undef9928 = 1, {___rho_26_^0 -> undef10211, status^0 -> 4, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_13_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ undef10800 <= 0 /\ 1 <= ___rho_14_^0 /\ undef10517 = 1 /\ undef10518 = 1, {all remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_13_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ 1 <= ___rho_14_^0 /\ 1 <= undef10800 /\ undef10517 = 1 /\ undef10518 = 1, {status^0 -> 4, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ undef11137 <= 0 /\ undef11472 <= 0 /\ 1 <= ___rho_13_^0 /\ undef10939 = 1 /\ undef10940 = 1, {all remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ undef11472 <= 0 /\ 1 <= ___rho_13_^0 /\ 1 <= undef11137 /\ undef10939 = 1 /\ undef10940 = 1, {status^0 -> 15, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ undef11137 <= 0 /\ 1 <= ___rho_13_^0 /\ 1 <= undef11472 /\ undef10939 = 1 /\ undef10940 = 1, {status^0 -> 4, rest remain the same}>
<l9, l2, ___rho_12_^0 <= 0 /\ ___rho_8_^0 <= 0 /\ 1 <= ___rho_13_^0 /\ 1 <= undef11137 /\ 1 <= undef11472 /\ undef10939 = 1 /\ undef10940 = 1, {status^0 -> 15, rest remain the same}>
<l9, l2, ___rho_8_^0 <= 0 /\ undef11797 <= 0 /\ 1 <= ___rho_12_^0, {___rho_13_^0 -> undef11797, rest remain the same}>
<l9, l2, ___rho_8_^0 <= 0 /\ 1 <= ___rho_12_^0 /\ 1 <= undef11797, {___rho_13_^0 -> undef11797, status^0 -> 4, rest remain the same}>
<l9, l2, undef13007 <= 0 /\ undef13344 <= 0 /\ 1 <= ___rho_8_^0, {all remain the same}>
<l9, l2, undef13007 <= 0 /\ 1 <= ___rho_8_^0 /\ 1 <= undef13344, {status^0 -> 4, rest remain the same}>
<l37, l2, 37 <= ___rho_33_^0 /\ undef4879 = 1 /\ undef4880 = 1, {status^0 -> 15, rest remain the same}>
<l37, l2, 30 <= ___rho_33_^0 /\ ___rho_33_^0 <= 35 /\ undef4879 = 1 /\ undef4880 = 1, {status^0 -> 15, rest remain the same}>
<l37, l2, 28 <= LData^0 /\ undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 29, {all remain the same}>
<l37, l2, LData^0 <= 26 /\ undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 29, {all remain the same}>
<l37, l2, undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 29 /\ LData^0 = 27, {status^0 -> 15, rest remain the same}>
<l37, l2, undef4879 = 1 /\ undef4880 = 1 /\ LData^0 = 27 /\ ___rho_33_^0 = 36, {all remain the same}>
<l37, l2, 28 <= LData^0 /\ undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 36, {status^0 -> 15, rest remain the same}>
<l37, l2, LData^0 <= 26 /\ undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 36, {status^0 -> 15, rest remain the same}>
<l37, l2, ___rho_33_^0 <= 27 /\ undef4879 = 1 /\ undef4880 = 1, {status^0 -> 15, rest remain the same}>
<l37, l2, undef4879 = 1 /\ undef4880 = 1 /\ ___rho_33_^0 = 28, {all remain the same}>
<l47, l2, length^0 <= 0 /\ undef12722 <= 0 /\ undef12285 = 1, {all remain the same}>
<l47, l2, length^0 <= 0 /\ 1 <= undef12722 /\ undef12370 = 0 /\ undef12285 = 1, {all remain the same}>
<l47, l2, length^0 <= 0 /\ 1 <= undef12370 /\ 1 <= undef12722 /\ undef12285 = 1, {all remain the same}>
<l47, l2, length^0 <= 0 /\ 1 + undef12370 <= 0 /\ 1 <= undef12722 /\ undef12285 = 1, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ ___rho_19_^0 <= 0 /\ ___rho_20_^0 <= 0 /\ ___rho_21_^0 <= 0 /\ ___rho_22_^0 <= 0, {status^0 -> 41, rest remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ ___rho_19_^0 <= 0 /\ ___rho_20_^0 <= 0 /\ ___rho_21_^0 <= 0 /\ 1 <= ___rho_22_^0, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ ___rho_19_^0 <= 0 /\ ___rho_20_^0 <= 0 /\ undef3406 <= 0 /\ 1 <= ___rho_21_^0 /\ undef3113 = 1 /\ undef3114 = 1, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ ___rho_19_^0 <= 0 /\ ___rho_20_^0 <= 0 /\ 1 <= ___rho_21_^0 /\ 1 <= undef3406 /\ undef3113 = 1 /\ undef3114 = 1, {status^0 -> 4, rest remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ undef8696 <= 0 /\ 1 <= ___rho_19_^0 /\ undef8493 = 1 /\ undef8494 = 1, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ ___rho_18_^0 <= 0 /\ 1 <= ___rho_19_^0 /\ 1 <= undef8696, {status^0 -> 4, rest remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ undef9285 <= 0 /\ 1 <= ___rho_18_^0 /\ undef9083 = 1 /\ undef9084 = 1, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ ___rho_17_^0 <= 0 /\ 1 <= ___rho_18_^0 /\ 1 <= undef9285, {status^0 -> 4, rest remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ undef9620 <= 0 /\ 1 <= ___rho_17_^0, {all remain the same}>
<l65, l2, ___rho_16_^0 <= 0 /\ 1 <= ___rho_17_^0 /\ 1 <= undef9620, {status^0 -> 4, rest remain the same}>
<l65, l2, 1 <= ___rho_16_^0 /\ undef9841 = 1 /\ undef9842 = 1, {all remain the same}>

Graph 10
<l2, l15, 8 <= status^0, {all remain the same}>
<l2, l15, status^0 <= 6, {all remain the same}>

Graph 11
<l2, l22, status^0 = 7, {all remain the same}>
<l15, l22, Irp^0 = 0, {all remain the same}>
<l15, l22, 1 <= Irp^0, {all remain the same}>
<l15, l22, 1 + Irp^0 <= 0, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 9 )
( 7 , 2 )
( 9 , 3 )
( 15 , 10 )
( 18 , 1 )
( 22 , 11 )
( 37 , 8 )
( 44 , 7 )
( 47 , 4 )
( 56 , 6 )
( 65 , 5 )

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.001699

> No variable changes in termination graph.
Checking conditional unfeasibility...
Termination failed. Trying to show unreachability...
Proving unreachability of entry: <l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>

LOG: CALL check - Post:1 <= 0 - Process 1
* Exit transition: <l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004081s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.004160s
Cannot prove unreachability

Proving non-termination of subgraph 1
Transitions:
<l18, l18, true, {all remain the same}>
Variables:

Checking conditional non-termination of SCC {l18}...
> No exit transition to close.
Calling reachability with...
Transition: <l18, end, true, {all remain the same}>
Conditions: 
Transition: <l18, end, true, {all remain the same}>
Conditions: 
OPEN EXITS: 
<l18, end, true, {all remain the same}>
<l18, end, true, {all remain the same}>

--- Reachability graph ---
> Graph without transitions.

Calling reachability with...
Transition: <l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
Conditions: 
Transition: <l0, l18, 3 <= undef13535 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
Conditions: 
Transition: <l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
Conditions: 
Transition: <l0, l18, 3 <= undef13535 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
Conditions: 
OPEN EXITS: 
<l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
<l0, l18, 3 <= undef13535 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
<l0, l18, undef13535 <= 1 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>
<l0, l18, 3 <= undef13535 /\ CancelIrql^0 = undef13466 /\ DeviceObject^0 = undef13468 /\ Irp^0 = undef13469 /\ LData^0 = 0 /\ length^0 = undef13531 /\ undef13549 = undef13550 /\ undef13550 = 0 /\ undef13551 = 1, {status^0 -> undef13535, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate