NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l35, true>
<l1, l2, ((0 + k3^0) <= 0) /\ (undef68 = 1), par{i___02020^0 -> (0 + Irql^0), keR^0 -> 0}>
<l1, l3, (1 <= (0 + k3^0)) /\ (undef136 = undef136) /\ (undef108 = undef108) /\ (undef75 = undef75) /\ (undef137 = 1), par{IsochDetachData^0 -> undef75, a1818^0 -> (0 + undef75), i^0 -> undef108, i___01717^0 -> (0 + Irql^0), k3^0 -> (~(1) + k3^0), keR^0 -> 0}>
<l4, l5, ((0 + AsyncAddressData^0) <= 0)>
<l4, l5, (1 <= (0 + AsyncAddressData^0))>
<l6, l4, ((0 + __rho_9_^0) <= 0)>
<l6, l4, (1 <= (0 + __rho_9_^0))>
<l7, l6, (undef427 = undef427), par{__rho_9_^0 -> undef427}>
<l8, l7, ((0 + __rho_8_^0) <= 0)>
<l8, l7, (1 <= (0 + __rho_8_^0))>
<l9, l8, (undef627 = undef627), par{__rho_8_^0 -> undef627}>
<l10, l9, ((0 + __rho_7_^0) <= 0)>
<l10, l9, (1 <= (0 + __rho_7_^0))>
<l11, l12, true>
<l13, l10, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894), par{AsyncAddressData^0 -> undef875, __rho_7_^0 -> undef894, k2^0 -> (~(1) + k2^0)}>
<l13, l3, ((0 + k2^0) <= 0) /\ (undef1010 = 1) /\ (undef953 = undef953), par{__rho_10_^0 -> undef953, i___01313^0 -> (0 + Irql^0), k3^0 -> (0 + undef953), keR^0 -> 0}>
<l5, l13, true>
<l3, l1, (undef1145 = 1), par{keA^0 -> 0}>
<l14, l11, true, par{a77^0 -> (0 + CromData^0)}>
<l15, l14, ((0 + __rho_3_^0) <= 0)>
<l15, l14, (1 <= (0 + __rho_3_^0))>
<l16, l15, (undef1362 = undef1362), par{__rho_3_^0 -> undef1362}>
<l17, l16, ((0 + __rho_2_^0) <= 0)>
<l17, l16, (1 <= (0 + __rho_2_^0))>
<l2, l18, (undef1615 = 1) /\ (undef1559 = undef1559), par{__rho_11_^0 -> undef1559, k4^0 -> (0 + undef1559), keA^0 -> 0}>
<l19, l11, ((0 + CromData^0) <= 0)>
<l19, l17, (1 <= (0 + CromData^0)) /\ (undef1697 = undef1697), par{__rho_2_^0 -> undef1697}>
<l12, l19, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752), par{CromData^0 -> undef1752, k1^0 -> (~(1) + k1^0)}>
<l12, l5, ((0 + k1^0) <= 0) /\ (undef1885 = 1) /\ (undef1884 = 1) /\ (undef1833 = undef1833), par{__rho_4_^0 -> undef1833, i___099^0 -> (0 + Irql^0), k2^0 -> (0 + undef1833), keA^0 -> 0, keR^0 -> 0}>
<l20, l21, true>
<l22, l11, (undef2017 = 0) /\ (undef2020 = 1) /\ (undef1970 = undef1970), par{__rho_5_^0 -> undef1970, k1^0 -> (0 + undef1970), keA^0 -> 0, ntStatus^0 -> (0 + undef2017), ret_IoSetDeviceInterfaceState44^0 -> undef2017}>
<l23, l24, true>
<l25, l26, true, par{phi_nSUC_ret^0 -> 1}>
<l27, l26, ((0 + ntStatus^0) <= 2) /\ (2 <= (0 + ntStatus^0))>
<l27, l25, (3 <= (0 + ntStatus^0))>
<l27, l25, ((1 + ntStatus^0) <= 2)>
<l26, l28, true>
<l28, l26, true>
<l21, l20, (1 <= (0 + k5^0)) /\ (undef2557 = 0) /\ (undef2491 = undef2491) /\ (undef2553 = 0), par{BusResetIrp^0 -> undef2491, a4343^0 -> 0, a4545^0 -> (0 + undef2491), k5^0 -> (~(1) + k5^0), phi_io_compl^0 -> 1, prevCancel^0 -> (0 + undef2553), ret_IoSetCancelRoutine4444^0 -> undef2553}>
<l21, l27, ((0 + k5^0) <= 0) /\ (undef2625 = 1), par{i___04747^0 -> (0 + Irql^0), keR^0 -> 0}>
<l29, l22, ((0 + __rho_1_^0) <= 0)>
<l29, l22, (1 <= (0 + __rho_1_^0)) /\ (undef2758 = 0), par{a11^0 -> (0 + DeviceObject^0), b22^0 -> (0 + Irp^0), ntStatus^0 -> (0 + undef2758), ret_t1394Diag_PnpStopDevice33^0 -> undef2758}>
<l30, l2, (1 <= (0 + pIrb^0)) /\ (undef2826 = 0), par{a3232^0 -> (0 + pIrb^0), a3434^0 -> (0 + ResourceIrp^0), a3737^0 -> (0 + pIrb^0), a3838^0 -> (0 + ResourceIrp^0), b3333^0 -> 0, b3535^0 -> (0 + pIrb^0), ntStatus^0 -> (0 + undef2826), ret_t1394_SubmitIrpSynch3636^0 -> undef2826}>
<l30, l2, ((0 + pIrb^0) <= 0), par{a3131^0 -> (0 + ResourceIrp^0)}>
<l31, l30, (undef2955 = 0), par{a2828^0 -> 1, b2929^0 -> 0, pIrb^0 -> (0 + undef2955), ret_ExAllocatePool3030^0 -> undef2955}>
<l32, l31, (1 <= (0 + ResourceIrp^0))>
<l32, l31, ((1 + ResourceIrp^0) <= 0)>
<l32, l2, ((0 + ResourceIrp^0) <= 0) /\ (0 <= (0 + ResourceIrp^0))>
<l33, l2, ((0 + IsochResourceData^0) <= 0)>
<l33, l32, (1 <= (0 + IsochResourceData^0)) /\ (undef3286 = undef3286) /\ (undef3296 = undef3296) /\ (undef3238 = undef3238) /\ (undef3291 = 0), par{ResourceIrp^0 -> (0 + undef3291), StackSize^0 -> undef3238, a2525^0 -> (0 + undef3238), b2626^0 -> 0, pIrb^0 -> undef3286, ret_IoAllocateIrp2727^0 -> undef3291}>
<l18, l20, ((0 + k4^0) <= 0) /\ (undef3365 = 1) /\ (undef3364 = 1) /\ (undef3309 = undef3309), par{__rho_12_^0 -> undef3309, i___04040^0 -> (0 + Irql^0), k5^0 -> (0 + undef3309), keA^0 -> 0, keR^0 -> 0}>
<l18, l33, (1 <= (0 + k4^0)) /\ (undef3373 = undef3373) /\ (undef3433 = 1), par{IsochResourceData^0 -> undef3373, i___02424^0 -> (0 + Irql^0), k4^0 -> (~(1) + k4^0), keR^0 -> 0}>
<l34, l29, (undef3482 = 0) /\ (undef3481 = (0 + undef3482)) /\ (undef3489 = (0 + undef3481)) /\ (undef3452 = undef3452) /\ (undef3447 = undef3447), par{__rho_1_^0 -> undef3447, __rho_666_^0 -> undef3452, ioA^0 -> undef3481, ioR^0 -> undef3482, keA^0 -> (0 + undef3489), keR^0 -> undef3489, phi_io_compl^0 -> 0, phi_nSUC_ret^0 -> 0}>
<l35, l34, true>

Fresh variables:
undef68, undef75, undef108, undef136, undef137, undef427, undef627, undef875, undef894, undef942, undef953, undef1010, undef1145, undef1362, undef1559, undef1615, undef1697, undef1752, undef1833, undef1884, undef1885, undef1970, undef2017, undef2020, undef2491, undef2553, undef2557, undef2625, undef2758, undef2826, undef2955, undef3238, undef3286, undef3291, undef3296, undef3309, undef3364, undef3365, undef3373, undef3433, undef3447, undef3452, undef3481, undef3482, undef3489, 

Undef variables:
undef68, undef75, undef108, undef136, undef137, undef427, undef627, undef875, undef894, undef942, undef953, undef1010, undef1145, undef1362, undef1559, undef1615, undef1697, undef1752, undef1833, undef1884, undef1885, undef1970, undef2017, undef2020, undef2491, undef2553, undef2557, undef2625, undef2758, undef2826, undef2955, undef3238, undef3286, undef3291, undef3296, undef3309, undef3364, undef3365, undef3373, undef3433, undef3447, undef3452, undef3481, undef3482, undef3489, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l11, (k1^0 = (0 + undef1970)) /\ (ntStatus^0 = (0 + undef2017)) /\ (undef3482 = 0) /\ (undef3481 = (0 + undef3482)) /\ (undef3489 = (0 + undef3481)) /\ (undef3452 = undef3452) /\ (undef3447 = undef3447) /\ ((0 + undef3447) <= 0) /\ (undef2017 = 0) /\ (undef2020 = 1) /\ (undef1970 = undef1970)>
<l0, l11, (k1^0 = (0 + undef1970)) /\ (ntStatus^0 = (0 + undef2017)) /\ (undef3482 = 0) /\ (undef3481 = (0 + undef3482)) /\ (undef3489 = (0 + undef3481)) /\ (undef3452 = undef3452) /\ (undef3447 = undef3447) /\ (1 <= (0 + undef3447)) /\ (undef2758 = 0) /\ (undef2017 = 0) /\ (undef2020 = 1) /\ (undef1970 = undef1970)>
<l2, l20, (undef1615 = 1) /\ (undef1559 = undef1559) /\ ((0 + (0 + undef1559)) <= 0) /\ (undef3365 = 1) /\ (undef3364 = 1) /\ (undef3309 = undef3309), par{k5^0 -> (0 + undef3309)}>
<l2, l2, (undef1615 = 1) /\ (undef1559 = undef1559) /\ (1 <= (0 + (0 + undef1559))) /\ (undef3373 = undef3373) /\ (undef3433 = 1) /\ ((0 + undef3373) <= 0)>
<l2, l2, (undef1615 = 1) /\ (undef1559 = undef1559) /\ (1 <= (0 + (0 + undef1559))) /\ (undef3373 = undef3373) /\ (undef3433 = 1) /\ (1 <= (0 + undef3373)) /\ (undef3286 = undef3286) /\ (undef3296 = undef3296) /\ (undef3238 = undef3238) /\ (undef3291 = 0) /\ ((0 + (0 + undef3291)) <= 0) /\ (0 <= (0 + (0 + undef3291)))>
<l3, l2, (undef1145 = 1) /\ ((0 + k3^0) <= 0) /\ (undef68 = 1)>
<l3, l3, (undef1145 = 1) /\ (1 <= (0 + k3^0)) /\ (undef136 = undef136) /\ (undef108 = undef108) /\ (undef75 = undef75) /\ (undef137 = 1), par{k3^0 -> (~(1) + k3^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ ((0 + undef894) <= 0) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ ((0 + undef627) <= 0) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ ((0 + undef427) <= 0) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ ((0 + undef875) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef942 = undef942) /\ (undef875 = undef875) /\ (undef894 = undef894) /\ (1 <= (0 + undef894)) /\ (undef627 = undef627) /\ (1 <= (0 + undef627)) /\ (undef427 = undef427) /\ (1 <= (0 + undef427)) /\ (1 <= (0 + undef875)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l3, ((0 + k2^0) <= 0) /\ (undef1010 = 1) /\ (undef953 = undef953), par{k3^0 -> (0 + undef953)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752) /\ ((0 + undef1752) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752) /\ (1 <= (0 + undef1752)) /\ (undef1697 = undef1697) /\ ((0 + undef1697) <= 0) /\ (undef1362 = undef1362) /\ ((0 + undef1362) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752) /\ (1 <= (0 + undef1752)) /\ (undef1697 = undef1697) /\ ((0 + undef1697) <= 0) /\ (undef1362 = undef1362) /\ (1 <= (0 + undef1362)), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752) /\ (1 <= (0 + undef1752)) /\ (undef1697 = undef1697) /\ (1 <= (0 + undef1697)) /\ (undef1362 = undef1362) /\ ((0 + undef1362) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1752 = undef1752) /\ (1 <= (0 + undef1752)) /\ (undef1697 = undef1697) /\ (1 <= (0 + undef1697)) /\ (undef1362 = undef1362) /\ (1 <= (0 + undef1362)), par{k1^0 -> (~(1) + k1^0)}>
<l11, l5, ((0 + k1^0) <= 0) /\ (undef1885 = 1) /\ (undef1884 = 1) /\ (undef1833 = undef1833), par{k2^0 -> (0 + undef1833)}>
<l20, l20, (1 <= (0 + k5^0)) /\ (undef2557 = 0) /\ (undef2491 = undef2491) /\ (undef2553 = 0), par{k5^0 -> (~(1) + k5^0)}>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2625 = 1) /\ ((0 + ntStatus^0) <= 2) /\ (2 <= (0 + ntStatus^0))>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2625 = 1) /\ (3 <= (0 + ntStatus^0))>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2625 = 1) /\ ((1 + ntStatus^0) <= 2)>
<l26, l26, true>

Fresh variables:
undef68, undef75, undef108, undef136, undef137, undef427, undef627, undef875, undef894, undef942, undef953, undef1010, undef1145, undef1362, undef1559, undef1615, undef1697, undef1752, undef1833, undef1884, undef1885, undef1970, undef2017, undef2020, undef2491, undef2553, undef2557, undef2625, undef2758, undef2826, undef2955, undef3238, undef3286, undef3291, undef3296, undef3309, undef3364, undef3365, undef3373, undef3433, undef3447, undef3452, undef3481, undef3482, undef3489, 

Undef variables:
undef68, undef75, undef108, undef136, undef137, undef427, undef627, undef875, undef894, undef942, undef953, undef1010, undef1145, undef1362, undef1559, undef1615, undef1697, undef1752, undef1833, undef1884, undef1885, undef1970, undef2017, undef2020, undef2491, undef2553, undef2557, undef2625, undef2758, undef2826, undef2955, undef3238, undef3286, undef3291, undef3296, undef3309, undef3364, undef3365, undef3373, undef3433, undef3447, undef3452, undef3481, undef3482, undef3489, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>
Variables:
k1^0

Graph 2:
Transitions:
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>
Variables:
k2^0

Graph 3:
Transitions:
<l3, l3, 1 <= k3^0 /\ undef137 = 1 /\ undef1145 = 1, {k3^0 -> -1 + k3^0, rest remain the same}>
Variables:
k3^0

Graph 4:
Transitions:
<l2, l2, undef3373 <= 0 /\ 1 <= undef1559 /\ undef1615 = 1 /\ undef3433 = 1, {all remain the same}>
<l2, l2, 1 <= undef1559 /\ 1 <= undef3373 /\ undef3291 = 0 /\ undef1615 = 1 /\ undef3433 = 1, {all remain the same}>
Variables:

Graph 5:
Transitions:
<l20, l20, 1 <= k5^0 /\ undef2553 = 0 /\ undef2557 = 0, {k5^0 -> -1 + k5^0, rest remain the same}>
Variables:
k5^0

Graph 6:
Transitions:
<l26, l26, true, {all remain the same}>
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l11, undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef2020 = 1, {all remain the same}>

Graph 2
<l11, l5, k1^0 <= 0 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>

Graph 3
<l5, l3, k2^0 <= 0 /\ undef1010 = 1, {k3^0 -> undef953, rest remain the same}>

Graph 4
<l3, l2, k3^0 <= 0 /\ undef68 = 1 /\ undef1145 = 1, {all remain the same}>

Graph 5
<l2, l20, undef1559 <= 0 /\ undef1615 = 1 /\ undef3364 = 1 /\ undef3365 = 1, {k5^0 -> undef3309, rest remain the same}>

Graph 6
<l20, l26, k5^0 <= 0 /\ undef2625 = 1 /\ ntStatus^0 = 2, {all remain the same}>
<l20, l26, k5^0 <= 0 /\ 3 <= ntStatus^0 /\ undef2625 = 1, {all remain the same}>
<l20, l26, k5^0 <= 0 /\ ntStatus^0 <= 1 /\ undef2625 = 1, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 4 )
( 3 , 3 )
( 5 , 2 )
( 11 , 1 )
( 20 , 5 )
( 26 , 6 )

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

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

Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002255s
Ranking function: -1 + k1^0
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.016717

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006727s
Ranking function: -1 + k2^0
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.000869

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001049s
Ranking function: -1 + k3^0
New Graphs: 
Proving termination of subgraph 4
Checking unfeasibility...
Time used: 0.001107

> No variable changes in termination graph.
Checking conditional unfeasibility...
Termination failed. Trying to show unreachability...
Proving unreachability of entry: <l3, l2, k3^0 <= 0 /\ undef68 = 1 /\ undef1145 = 1, {all remain the same}>

LOG: CALL check - Post:1 <= 0 - Process 1
* Exit transition: <l3, l2, k3^0 <= 0 /\ undef68 = 1 /\ undef1145 = 1, {all remain the same}>
* Postcondition  : 1 <= 0
Postcodition moved up: 1 <= 0

LOG: Try proving POST
Postcondition: 1 <= 0

LOG: CALL check - Post:1 <= 0 - Process 2
* Exit transition: <l5, l3, k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
* Postcondition  : 1 <= 0
Postcodition moved up: 1 <= 0

LOG: Try proving POST
Postcondition: 1 <= 0

LOG: CALL check - Post:1 <= 0 - Process 3
* Exit transition: <l11, l5, k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : 1 <= 0
Postcodition moved up: 1 <= 0

LOG: Try proving POST
Postcondition: 1 <= 0

LOG: CALL check - Post:1 <= 0 - Process 4
* Exit transition: <l0, l11, undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001150s
Postcondition: 1 <= 0

LOG: CALL check - Post:1 <= 0 - Process 5
* Exit transition: <l0, l11, 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001142s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= 0 /\ undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 0 <= 0 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1752 <= 0 /\ 1 <= k1^0 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: 1 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008509s
Time used: 0.008353
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000534s
Time used: 1.00052

LOG: SAT solveNonLinear - Elapsed time: 1.009044s
Cost: 52; Total time: 1.00887
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006183s
Remaining time after improvement: 0.998354
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 6
* Exit transition: <l0, l11, 0 <= 0 /\ undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001448s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023512s
Time used: 0.023239
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000542s
Time used: 1.00053

LOG: SAT solveNonLinear - Elapsed time: 1.024054s
Cost: 52; Total time: 1.02377
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011879s
Remaining time after improvement: 0.996847
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 7
* Exit transition: <l0, l11, 0 <= 0 /\ undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001843s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.078374s

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
POST: 1 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032755s
Time used: 0.032363
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000628s
Time used: 1.00062

LOG: SAT solveNonLinear - Elapsed time: 1.033384s
Cost: 51; Total time: 1.03298
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.018178s
Remaining time after improvement: 0.995287
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 8
* Exit transition: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: CALL check - Post:undef1833 <= 0 - Process 9
* Exit transition: <l0, l11, undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef1833 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001221s
Postcondition: undef1833 <= 0

LOG: CALL check - Post:undef1833 <= 0 - Process 10
* Exit transition: <l0, l11, 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef1833 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001244s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010119s
Time used: 0.009954
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003019s
Time used: 1.00301

LOG: SAT solveNonLinear - Elapsed time: 1.013138s
Cost: 52; Total time: 1.01296
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006417s
Remaining time after improvement: 0.997688
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 11
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001711s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024144s
Time used: 0.023814
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001141s
Time used: 1.00113

LOG: SAT solveNonLinear - Elapsed time: 1.025285s
Cost: 52; Total time: 1.02494
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.012603s
Remaining time after improvement: 0.996181
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 12
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002240s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.088985s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.117611s
Time used: 0.116857
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001409s
Time used: 1.0014

LOG: SAT solveNonLinear - Elapsed time: 1.119020s
Cost: 51; Total time: 1.11826
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011243s
Remaining time after improvement: 0.993256
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 13
* Exit transition: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010817s
Time used: 0.010642
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001790s
Time used: 1.00178

LOG: SAT solveNonLinear - Elapsed time: 1.012607s
Cost: 52; Total time: 1.01242
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006582s
Remaining time after improvement: 0.997515
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 14
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001894s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025119s
Time used: 0.024767
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001453s
Time used: 1.00144

LOG: SAT solveNonLinear - Elapsed time: 1.026572s
Cost: 52; Total time: 1.02621
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013019s
Remaining time after improvement: 0.995846
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 15
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002378s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.090739s
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.211950s
Time used: 0.21092
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.790769s
Time used: 0.790757

LOG: SAT solveNonLinear - Elapsed time: 1.002719s
Cost: 51; Total time: 1.00168
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.017585s
Remaining time after improvement: 0.990953
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 16
* Exit transition: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011115s
Time used: 0.010938
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002766s
Time used: 1.00276

LOG: SAT solveNonLinear - Elapsed time: 1.013881s
Cost: 52; Total time: 1.01369
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006562s
Remaining time after improvement: 0.997475
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 17
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001932s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025942s
Time used: 0.025594
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002208s
Time used: 1.0022

LOG: SAT solveNonLinear - Elapsed time: 1.028150s
Cost: 52; Total time: 1.02779
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013423s
Remaining time after improvement: 0.995632
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 18
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002650s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.097355s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 11.610233s

LOG: NarrowEntry size 1
Narrowing transition: 
<l3, l3, 1 <= k3^0 /\ undef137 = 1 /\ undef1145 = 1, {k3^0 -> -1 + k3^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
END ENTRIES:
GRAPH:
<l3, l3, 0 <= 0 /\ 1 <= k3^0 /\ undef68 = 1 /\ undef137 = 1 /\ undef1145 = 1, {k3^0 -> -1 + k3^0, rest remain the same}>
END GRAPH:
EXIT: <l3, l2, k3^0 <= 0 /\ undef68 = 1 /\ undef1145 = 1, {all remain the same}>
POST: 1 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003965s
Time used: 0.003863
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003134s
Time used: 1.00313

LOG: SAT solveNonLinear - Elapsed time: 1.007099s
Cost: 51; Total time: 1.00699
Failed at location 3: k3^0 <= 0
Before Improving: 
Quasi-invariant at l3: k3^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013074s
Remaining time after improvement: 0.998891
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l3: k3^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k3^0 <= 0 - Process 19
* Exit transition: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef953 <= 0

LOG: Try proving POST
Postcondition: undef953 <= 0

LOG: CALL check - Post:undef953 <= 0 - Process 20
* Exit transition: <l11, l5, k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : undef953 <= 0
Postcodition moved up: undef953 <= 0

LOG: Try proving POST
Postcondition: undef953 <= 0

LOG: CALL check - Post:undef953 <= 0 - Process 21
* Exit transition: <l0, l11, undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef953 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001581s
Postcondition: undef953 <= 0

LOG: CALL check - Post:undef953 <= 0 - Process 22
* Exit transition: <l0, l11, 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef953 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001619s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: undef953 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011124s
Time used: 0.010942
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.006196s
Time used: 1.00618

LOG: SAT solveNonLinear - Elapsed time: 1.017320s
Cost: 52; Total time: 1.01713
Failed at location 11: 1 + k1^0 <= 0
Failed at location 11: 1 + k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: 1 + k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006849s
Remaining time after improvement: 0.997438
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: 1 + k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:1 + k1^0 <= 0 - Process 23
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : 1 + k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002791s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027847s
Time used: 0.027534
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001652s
Time used: 1.00161

LOG: SAT solveNonLinear - Elapsed time: 1.029498s
Cost: 52; Total time: 1.02914
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013387s
Remaining time after improvement: 0.995592
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 24
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003355s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.106441s

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
POST: k3^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027104s
Time used: 0.026642
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001341s
Time used: 1.00132

LOG: SAT solveNonLinear - Elapsed time: 1.028445s
Cost: 51; Total time: 1.02796
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.018869s
Remaining time after improvement: 0.993779
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 25
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: CALL check - Post:undef1833 <= 0 - Process 26
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef1833 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001679s
Postcondition: undef1833 <= 0

LOG: CALL check - Post:undef1833 <= 0 - Process 27
* Exit transition: <l0, l11, 1 <= undef953 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : undef1833 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001734s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011913s
Time used: 0.011707
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002345s
Time used: 1.00234

LOG: SAT solveNonLinear - Elapsed time: 1.014259s
Cost: 52; Total time: 1.01404
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006827s
Remaining time after improvement: 0.997099
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 28
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003452s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029620s
Time used: 0.029261
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001498s
Time used: 1.00149

LOG: SAT solveNonLinear - Elapsed time: 1.031118s
Cost: 52; Total time: 1.03075
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013759s
Remaining time after improvement: 0.995285
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 29
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003475s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.112237s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.089803s
Time used: 0.088837
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001608s
Time used: 1.00158

LOG: SAT solveNonLinear - Elapsed time: 1.091411s
Cost: 51; Total time: 1.09042
Failed at location 5: 1 + k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: 1 + k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013648s
Remaining time after improvement: 0.991889
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: 1 + k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:1 + k2^0 <= 0 - Process 30
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1833 <= 0

LOG: Try proving POST
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 0 <= undef1833 /\ 1 <= undef953 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: 1 + k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012024s
Time used: 0.011829
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003067s
Time used: 1.00306

LOG: SAT solveNonLinear - Elapsed time: 1.015091s
Cost: 52; Total time: 1.01489
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007125s
Remaining time after improvement: 0.997419
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 31
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002982s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.030285s
Time used: 0.02995
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002376s
Time used: 1.00236

LOG: SAT solveNonLinear - Elapsed time: 1.032661s
Cost: 52; Total time: 1.03231
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013678s
Remaining time after improvement: 0.995304
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 32
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003173s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.112135s
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.227670s
Time used: 0.226276
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.774936s
Time used: 0.774929

LOG: SAT solveNonLinear - Elapsed time: 1.002606s
Cost: 51; Total time: 1.0012
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.021858s
Remaining time after improvement: 0.989235
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 33
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011799s
Time used: 0.011609
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004178s
Time used: 1.00417

LOG: SAT solveNonLinear - Elapsed time: 1.015977s
Cost: 52; Total time: 1.01578
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007171s
Remaining time after improvement: 0.996918
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 34
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002034s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.028938s
Time used: 0.028603
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003665s
Time used: 1.00365

LOG: SAT solveNonLinear - Elapsed time: 1.032602s
Cost: 52; Total time: 1.03226
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013791s
Remaining time after improvement: 0.995236
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 35
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002821s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.111841s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 11.696520s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010494s
Time used: 0.010354
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003157s
Time used: 1.00314

LOG: SAT solveNonLinear - Elapsed time: 1.013651s
Cost: 51; Total time: 1.0135
Failed at location 3: k3^0 <= 0
Before Improving: 
Quasi-invariant at l3: k3^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002956s
Remaining time after improvement: 0.998705
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l3: k3^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k3^0 <= 0 - Process 36
* Exit transition: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef953 <= 0

LOG: Try proving POST
Postcondition: undef953 <= 0

LOG: Postcondition is not implied - Post: undef953 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
POST: k3^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.028166s
Time used: 0.02773
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002239s
Time used: 1.00223

LOG: SAT solveNonLinear - Elapsed time: 1.030405s
Cost: 51; Total time: 1.02996
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.018858s
Remaining time after improvement: 0.993654
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 37
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012645s
Time used: 0.01244
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.021708s
Time used: 1.0217

LOG: SAT solveNonLinear - Elapsed time: 1.034353s
Cost: 52; Total time: 1.03414
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006958s
Remaining time after improvement: 0.996979
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 38
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003017s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.030469s
Time used: 0.030106
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002476s
Time used: 1.00247

LOG: SAT solveNonLinear - Elapsed time: 1.032944s
Cost: 52; Total time: 1.03257
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.028031s
Remaining time after improvement: 0.992634
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 39
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.004884s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.148435s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.094170s
Time used: 0.093158
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001655s
Time used: 1.00164

LOG: SAT solveNonLinear - Elapsed time: 1.095825s
Cost: 51; Total time: 1.0948
Failed at location 5: 1 + k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: 1 + k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.014325s
Remaining time after improvement: 0.991376
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: 1 + k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:1 + k2^0 <= 0 - Process 40
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1833 <= 0

LOG: Try proving POST
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 0 <= undef1833 /\ 1 <= undef953 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: 1 + k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012972s
Time used: 0.012768
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.022236s
Time used: 1.02223

LOG: SAT solveNonLinear - Elapsed time: 1.035208s
Cost: 52; Total time: 1.03499
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007511s
Remaining time after improvement: 0.997367
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 41
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003388s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.031196s
Time used: 0.030859
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003550s
Time used: 1.00354

LOG: SAT solveNonLinear - Elapsed time: 1.034746s
Cost: 52; Total time: 1.0344
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013659s
Remaining time after improvement: 0.99528
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 42
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003558s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.140867s
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.228894s
Time used: 0.227491
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.773723s
Time used: 0.773716

LOG: SAT solveNonLinear - Elapsed time: 1.002617s
Cost: 51; Total time: 1.00121
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.023638s
Remaining time after improvement: 0.989161
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 43
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012252s
Time used: 0.012061
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.014193s
Time used: 1.01418

LOG: SAT solveNonLinear - Elapsed time: 1.026445s
Cost: 52; Total time: 1.02625
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007394s
Remaining time after improvement: 0.997217
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 44
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002212s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029524s
Time used: 0.029185
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004183s
Time used: 1.00417

LOG: SAT solveNonLinear - Elapsed time: 1.033707s
Cost: 52; Total time: 1.03336
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.014048s
Remaining time after improvement: 0.99509
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 45
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003290s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.126008s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 9.681040s
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024498s
Time used: 0.02434
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.979799s
Time used: 0.97979

LOG: SAT solveNonLinear - Elapsed time: 1.004298s
Cost: 51; Total time: 1.00413
Failed at location 3: k3^0 <= 0
Before Improving: 
Quasi-invariant at l3: k3^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004587s
Remaining time after improvement: 0.998512
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l3: k3^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k3^0 <= 0 - Process 46
* Exit transition: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef953 <= 0

LOG: Try proving POST
Postcondition: undef953 <= 0

LOG: Postcondition is not implied - Post: undef953 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef894 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef627 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef427 <= 0 /\ 1 <= k2^0 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef875 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef427 /\ 1 <= undef627 /\ 1 <= undef875 /\ 1 <= undef894 /\ 1 <= undef953 /\ undef1010 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1, {k3^0 -> undef953, rest remain the same}>
POST: k3^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.028557s
Time used: 0.028107
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.018425s
Time used: 1.01841

LOG: SAT solveNonLinear - Elapsed time: 1.046983s
Cost: 51; Total time: 1.04652
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.022517s
Remaining time after improvement: 0.994662
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 47
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012942s
Time used: 0.012734
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004312s
Time used: 1.0043

LOG: SAT solveNonLinear - Elapsed time: 1.017254s
Cost: 52; Total time: 1.01704
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007073s
Remaining time after improvement: 0.996904
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 48
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002801s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.030611s
Time used: 0.030245
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004088s
Time used: 1.00408

LOG: SAT solveNonLinear - Elapsed time: 1.034699s
Cost: 52; Total time: 1.03432
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.014089s
Remaining time after improvement: 0.995035
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 49
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003579s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.120439s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.093348s
Time used: 0.092346
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001642s
Time used: 1.00163

LOG: SAT solveNonLinear - Elapsed time: 1.094990s
Cost: 51; Total time: 1.09398
Failed at location 5: 1 + k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: 1 + k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015505s
Remaining time after improvement: 0.990726
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: 1 + k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:1 + k2^0 <= 0 - Process 50
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1833 <= 0

LOG: Try proving POST
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: 1 + undef1833 <= 0

LOG: Postcondition is not implied - Post: 1 + undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 0 <= undef1833 /\ 1 <= undef953 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1833 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: 1 + k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014091s
Time used: 0.013874
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003756s
Time used: 1.00374

LOG: SAT solveNonLinear - Elapsed time: 1.017846s
Cost: 52; Total time: 1.01762
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007520s
Remaining time after improvement: 0.996761
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 51
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003928s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032189s
Time used: 0.031841
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003481s
Time used: 1.00347

LOG: SAT solveNonLinear - Elapsed time: 1.035670s
Cost: 52; Total time: 1.03531
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.014236s
Remaining time after improvement: 0.994889
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 52
* Exit transition: <l0, l11, 0 <= undef1833 /\ undef3447 <= 0 /\ 1 <= undef953 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003877s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.128060s
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230806s
Time used: 0.229369
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.771969s
Time used: 0.771962

LOG: SAT solveNonLinear - Elapsed time: 1.002776s
Cost: 51; Total time: 1.00133
Failed at location 5: k2^0 <= 0
Before Improving: 
Quasi-invariant at l5: k2^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.023961s
Remaining time after improvement: 0.989133
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l5: k2^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k2^0 <= 0 - Process 53
* Exit transition: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1833 <= 0

LOG: Try proving POST
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure
Postcondition: undef1833 <= 0

LOG: Postcondition is not implied - Post: undef1833 <= 0 - Already checked
Already checked with failure

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
Narrowing transition: 
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l11, l11, 1 <= k1^0 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752, {k1^0 -> -1 + k1^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, 1 <= undef953 /\ 1 <= undef1833 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1752 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1697 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1362 <= 0 /\ 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef953 /\ 1 <= undef1362 /\ 1 <= undef1697 /\ 1 <= undef1752 /\ 1 <= undef1833 /\ undef1884 = 1 /\ undef1885 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef953 /\ undef1010 = 1 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
POST: k2^0 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012965s
Time used: 0.012772
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.018421s
Time used: 1.01841

LOG: SAT solveNonLinear - Elapsed time: 1.031387s
Cost: 52; Total time: 1.03119
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008056s
Remaining time after improvement: 0.99696
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 54
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002241s
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029825s
Time used: 0.029493
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004994s
Time used: 1.00498

LOG: SAT solveNonLinear - Elapsed time: 1.034818s
Cost: 52; Total time: 1.03447
Failed at location 11: k1^0 <= 0
Failed at location 11: k1^0 <= 0
Before Improving: 
Quasi-invariant at l11: k1^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013971s
Remaining time after improvement: 0.995105
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l11: k1^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k1^0 <= 0 - Process 55
* Exit transition: <l0, l11, undef3447 <= 0 /\ 1 <= undef953 /\ 1 <= undef1833 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003321s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 2.133032s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 9.674233s

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

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

Proving non-termination of subgraph 4
Transitions:
<l2, l2, undef3373 <= 0 /\ 1 <= undef1559 /\ undef1615 = 1 /\ undef3433 = 1, {all remain the same}>
<l2, l2, 1 <= undef1559 /\ 1 <= undef3373 /\ undef3291 = 0 /\ undef1615 = 1 /\ undef3433 = 1, {all remain the same}>
Variables:

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

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

Calling reachability with...
Transition: <l3, l2, k3^0 <= 0 /\ undef68 = 1 /\ undef1145 = 1, {all remain the same}>
Conditions: 
OPEN EXITS: 
<l3, l2, k3^0 <= 0, {all remain the same}> (condsUp: undef68 = 1, undef1145 = 1)

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

Calling reachability with...
Transition: <l5, l3, k2^0 <= 0 /\ undef1010 = 1, {k3^0 -> undef953, rest remain the same}>
Conditions: k3^0 <= 0, undef68 = 1, undef1145 = 1, 
OPEN EXITS: 
WARNING: Applying substitution to an expression with non-program variables.
WARNING: Applying substitution to an expression with non-program variables.
<l5, l3, k2^0 <= 0, {k3^0 -> undef953, rest remain the same}> (condsUp: undef1010 = 1, undef953 <= 0, undef68 = 1, undef1145 = 1)

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

Calling reachability with...
Transition: <l11, l5, k1^0 <= 0 /\ undef1884 = 1 /\ undef1885 = 1, {k2^0 -> undef1833, rest remain the same}>
Conditions: k2^0 <= 0, undef1010 = 1, undef953 <= 0, undef68 = 1, undef1145 = 1, 
OPEN EXITS: 
WARNING: Applying substitution to an expression with non-program variables.
WARNING: Applying substitution to an expression with non-program variables.
WARNING: Applying substitution to an expression with non-program variables.
WARNING: Applying substitution to an expression with non-program variables.
<l11, l5, k1^0 <= 0, {k2^0 -> undef1833, rest remain the same}> (condsUp: undef1884 = 1, undef1885 = 1, undef1833 <= 0, undef1010 = 1, undef953 <= 0, undef68 = 1, undef1145 = 1)

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

Calling reachability with...
Transition: <l0, l11, undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef2020 = 1, {all remain the same}>
Conditions: k1^0 <= 0, undef1884 = 1, undef1885 = 1, undef1833 <= 0, undef1010 = 1, undef953 <= 0, undef68 = 1, undef1145 = 1, 
Transition: <l0, l11, 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef2020 = 1, {all remain the same}>
Conditions: k1^0 <= 0, undef1884 = 1, undef1885 = 1, undef1833 <= 0, undef1010 = 1, undef953 <= 0, undef68 = 1, undef1145 = 1, 
OPEN EXITS: 
<l0, l11, k1^0 <= 0 /\ undef953 <= 0 /\ undef1833 <= 0 /\ undef3447 <= 0 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>
<l0, l11, k1^0 <= 0 /\ undef953 <= 0 /\ undef1833 <= 0 /\ 1 <= undef3447 /\ k1^0 = undef1970 /\ ntStatus^0 = undef2017 /\ undef2017 = 0 /\ undef2758 = 0 /\ undef3481 = undef3482 /\ undef3481 = undef3489 /\ undef3482 = 0 /\ undef68 = 1 /\ undef1010 = 1 /\ undef1145 = 1 /\ undef1884 = 1 /\ undef1885 = 1 /\ undef2020 = 1, {all remain the same}>

> Conditions are reachable!

Program does NOT terminate