NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l35, true>
<l1, l2, ((0 + k3^0) <= 0) /\ (undef62 = 1), par{i___02020^0 -> (0 + Irql^0), keR^0 -> 0}>
<l1, l3, (1 <= (0 + k3^0)) /\ (undef124 = undef124) /\ (undef98 = undef98) /\ (undef67 = undef67) /\ (undef125 = 1), par{IsochDetachData^0 -> undef67, a1818^0 -> (0 + undef67), i^0 -> undef98, 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, (undef388 = undef388), par{__rho_9_^0 -> undef388}>
<l8, l7, ((0 + __rho_8_^0) <= 0)>
<l8, l7, (1 <= (0 + __rho_8_^0))>
<l9, l8, (undef570 = undef570), par{__rho_8_^0 -> undef570}>
<l10, l9, ((0 + __rho_7_^0) <= 0)>
<l10, l9, (1 <= (0 + __rho_7_^0))>
<l11, l12, true>
<l13, l10, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813), par{AsyncAddressData^0 -> undef797, __rho_7_^0 -> undef813, k2^0 -> (~(1) + k2^0)}>
<l13, l3, ((0 + k2^0) <= 0) /\ (undef920 = 1) /\ (undef866 = undef866), par{__rho_10_^0 -> undef866, i___01313^0 -> (0 + Irql^0), k3^0 -> (0 + undef866), keR^0 -> 0}>
<l5, l13, true>
<l3, l1, (undef1043 = 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, (undef1239 = undef1239), par{__rho_3_^0 -> undef1239}>
<l17, l16, ((0 + __rho_2_^0) <= 0)>
<l17, l16, (1 <= (0 + __rho_2_^0))>
<l2, l18, (undef1471 = 1) /\ (undef1418 = undef1418), par{__rho_11_^0 -> undef1418, k4^0 -> (0 + undef1418), keA^0 -> 0}>
<l19, l11, ((0 + CromData^0) <= 0)>
<l19, l17, (1 <= (0 + CromData^0)) /\ (undef1544 = undef1544), par{__rho_2_^0 -> undef1544}>
<l12, l19, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595), par{CromData^0 -> undef1595, k1^0 -> (~(1) + k1^0)}>
<l12, l5, ((0 + k1^0) <= 0) /\ (undef1717 = 1) /\ (undef1716 = 1) /\ (undef1668 = undef1668), par{__rho_4_^0 -> undef1668, i___099^0 -> (0 + Irql^0), k2^0 -> (0 + undef1668), keA^0 -> 0, keR^0 -> 0}>
<l20, l21, true>
<l22, l11, (undef1837 = 0) /\ (undef1840 = 1) /\ (undef1793 = undef1793), par{__rho_5_^0 -> undef1793, k1^0 -> (0 + undef1793), keA^0 -> 0, ntStatus^0 -> (0 + undef1837), ret_IoSetDeviceInterfaceState44^0 -> undef1837}>
<l23, l24, true>
<l25, l26, true, par{phi_nSUC_ret^0 -> 0}>
<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)), par{a4343^0 -> 1, k5^0 -> (~(1) + k5^0), phi_io_compl^0 -> 1}>
<l21, l27, ((0 + k5^0) <= 0) /\ (undef2390 = 1), par{i___04545^0 -> (0 + Irql^0), keR^0 -> 0}>
<l29, l22, ((0 + __rho_1_^0) <= 0)>
<l29, l22, (1 <= (0 + __rho_1_^0)) /\ (undef2511 = 0), par{a11^0 -> 1, b22^0 -> (0 + Irp^0), ntStatus^0 -> (0 + undef2511), ret_t1394Diag_PnpStopDevice33^0 -> undef2511}>
<l30, l2, (1 <= (0 + pIrb^0)) /\ (undef2573 = 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 + undef2573), ret_t1394_SubmitIrpSynch3636^0 -> undef2573}>
<l30, l2, ((0 + pIrb^0) <= 0), par{a3131^0 -> (0 + ResourceIrp^0)}>
<l31, l30, (undef2691 = 0), par{a2828^0 -> 1, b2929^0 -> 0, pIrb^0 -> (0 + undef2691), ret_ExAllocatePool3030^0 -> undef2691}>
<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)) /\ (undef2993 = undef2993) /\ (undef3001 = undef3001) /\ (undef2997 = 0), par{ResourceIrp^0 -> (0 + undef2997), a2525^0 -> 1, b2626^0 -> 0, pIrb^0 -> undef2993, ret_IoAllocateIrp2727^0 -> undef2997}>
<l18, l20, ((0 + k4^0) <= 0) /\ (undef3064 = 1) /\ (undef3063 = 1) /\ (undef3011 = undef3011), par{__rho_12_^0 -> undef3011, i___04040^0 -> (0 + Irql^0), k5^0 -> (0 + undef3011), keA^0 -> 0, keR^0 -> 0}>
<l18, l33, (1 <= (0 + k4^0)) /\ (undef3070 = undef3070) /\ (undef3126 = 1), par{IsochResourceData^0 -> undef3070, i___02424^0 -> (0 + Irql^0), k4^0 -> (~(1) + k4^0), keR^0 -> 0}>
<l34, l29, (undef3171 = 0) /\ (undef3170 = (0 + undef3171)) /\ (undef3178 = (0 + undef3170)) /\ (undef3142 = undef3142) /\ (undef3137 = undef3137), par{__rho_1_^0 -> undef3137, __rho_666_^0 -> undef3142, ioA^0 -> undef3170, ioR^0 -> undef3171, keA^0 -> (0 + undef3178), keR^0 -> undef3178, phi_io_compl^0 -> 0, phi_nSUC_ret^0 -> 0}>
<l35, l34, true>

Fresh variables:
undef62, undef67, undef98, undef124, undef125, undef388, undef570, undef797, undef813, undef858, undef866, undef920, undef1043, undef1239, undef1418, undef1471, undef1544, undef1595, undef1668, undef1716, undef1717, undef1793, undef1837, undef1840, undef2390, undef2511, undef2573, undef2691, undef2993, undef2997, undef3001, undef3011, undef3063, undef3064, undef3070, undef3126, undef3137, undef3142, undef3170, undef3171, undef3178, 

Undef variables:
undef62, undef67, undef98, undef124, undef125, undef388, undef570, undef797, undef813, undef858, undef866, undef920, undef1043, undef1239, undef1418, undef1471, undef1544, undef1595, undef1668, undef1716, undef1717, undef1793, undef1837, undef1840, undef2390, undef2511, undef2573, undef2691, undef2993, undef2997, undef3001, undef3011, undef3063, undef3064, undef3070, undef3126, undef3137, undef3142, undef3170, undef3171, undef3178, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l11, (k1^0 = (0 + undef1793)) /\ (ntStatus^0 = (0 + undef1837)) /\ (undef3171 = 0) /\ (undef3170 = (0 + undef3171)) /\ (undef3178 = (0 + undef3170)) /\ (undef3142 = undef3142) /\ (undef3137 = undef3137) /\ ((0 + undef3137) <= 0) /\ (undef1837 = 0) /\ (undef1840 = 1) /\ (undef1793 = undef1793)>
<l0, l11, (k1^0 = (0 + undef1793)) /\ (ntStatus^0 = (0 + undef1837)) /\ (undef3171 = 0) /\ (undef3170 = (0 + undef3171)) /\ (undef3178 = (0 + undef3170)) /\ (undef3142 = undef3142) /\ (undef3137 = undef3137) /\ (1 <= (0 + undef3137)) /\ (undef2511 = 0) /\ (undef1837 = 0) /\ (undef1840 = 1) /\ (undef1793 = undef1793)>
<l2, l20, (undef1471 = 1) /\ (undef1418 = undef1418) /\ ((0 + (0 + undef1418)) <= 0) /\ (undef3064 = 1) /\ (undef3063 = 1) /\ (undef3011 = undef3011), par{k5^0 -> (0 + undef3011)}>
<l2, l2, (undef1471 = 1) /\ (undef1418 = undef1418) /\ (1 <= (0 + (0 + undef1418))) /\ (undef3070 = undef3070) /\ (undef3126 = 1) /\ ((0 + undef3070) <= 0)>
<l2, l2, (undef1471 = 1) /\ (undef1418 = undef1418) /\ (1 <= (0 + (0 + undef1418))) /\ (undef3070 = undef3070) /\ (undef3126 = 1) /\ (1 <= (0 + undef3070)) /\ (undef2993 = undef2993) /\ (undef3001 = undef3001) /\ (undef2997 = 0) /\ ((0 + (0 + undef2997)) <= 0) /\ (0 <= (0 + (0 + undef2997)))>
<l3, l2, (undef1043 = 1) /\ ((0 + k3^0) <= 0) /\ (undef62 = 1)>
<l3, l3, (undef1043 = 1) /\ (1 <= (0 + k3^0)) /\ (undef124 = undef124) /\ (undef98 = undef98) /\ (undef67 = undef67) /\ (undef125 = 1), par{k3^0 -> (~(1) + k3^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ ((0 + undef813) <= 0) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ ((0 + undef570) <= 0) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ ((0 + undef388) <= 0) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ ((0 + undef797) <= 0), par{k2^0 -> (~(1) + k2^0)}>
<l5, l5, (1 <= (0 + k2^0)) /\ (undef858 = undef858) /\ (undef797 = undef797) /\ (undef813 = undef813) /\ (1 <= (0 + undef813)) /\ (undef570 = undef570) /\ (1 <= (0 + undef570)) /\ (undef388 = undef388) /\ (1 <= (0 + undef388)) /\ (1 <= (0 + undef797)), par{k2^0 -> (~(1) + k2^0)}>
<l5, l3, ((0 + k2^0) <= 0) /\ (undef920 = 1) /\ (undef866 = undef866), par{k3^0 -> (0 + undef866)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595) /\ ((0 + undef1595) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595) /\ (1 <= (0 + undef1595)) /\ (undef1544 = undef1544) /\ ((0 + undef1544) <= 0) /\ (undef1239 = undef1239) /\ ((0 + undef1239) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595) /\ (1 <= (0 + undef1595)) /\ (undef1544 = undef1544) /\ ((0 + undef1544) <= 0) /\ (undef1239 = undef1239) /\ (1 <= (0 + undef1239)), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595) /\ (1 <= (0 + undef1595)) /\ (undef1544 = undef1544) /\ (1 <= (0 + undef1544)) /\ (undef1239 = undef1239) /\ ((0 + undef1239) <= 0), par{k1^0 -> (~(1) + k1^0)}>
<l11, l11, (1 <= (0 + k1^0)) /\ (undef1595 = undef1595) /\ (1 <= (0 + undef1595)) /\ (undef1544 = undef1544) /\ (1 <= (0 + undef1544)) /\ (undef1239 = undef1239) /\ (1 <= (0 + undef1239)), par{k1^0 -> (~(1) + k1^0)}>
<l11, l5, ((0 + k1^0) <= 0) /\ (undef1717 = 1) /\ (undef1716 = 1) /\ (undef1668 = undef1668), par{k2^0 -> (0 + undef1668)}>
<l20, l20, (1 <= (0 + k5^0)), par{k5^0 -> (~(1) + k5^0)}>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2390 = 1) /\ ((0 + ntStatus^0) <= 2) /\ (2 <= (0 + ntStatus^0))>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2390 = 1) /\ (3 <= (0 + ntStatus^0))>
<l20, l26, ((0 + k5^0) <= 0) /\ (undef2390 = 1) /\ ((1 + ntStatus^0) <= 2)>
<l26, l26, true>

Fresh variables:
undef62, undef67, undef98, undef124, undef125, undef388, undef570, undef797, undef813, undef858, undef866, undef920, undef1043, undef1239, undef1418, undef1471, undef1544, undef1595, undef1668, undef1716, undef1717, undef1793, undef1837, undef1840, undef2390, undef2511, undef2573, undef2691, undef2993, undef2997, undef3001, undef3011, undef3063, undef3064, undef3070, undef3126, undef3137, undef3142, undef3170, undef3171, undef3178, 

Undef variables:
undef62, undef67, undef98, undef124, undef125, undef388, undef570, undef797, undef813, undef858, undef866, undef920, undef1043, undef1239, undef1418, undef1471, undef1544, undef1595, undef1668, undef1716, undef1717, undef1793, undef1837, undef1840, undef2390, undef2511, undef2573, undef2691, undef2993, undef2997, undef3001, undef3011, undef3063, undef3064, undef3070, undef3126, undef3137, undef3142, undef3170, undef3171, undef3178, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1595, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1595, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1544 /\ 1 <= undef1595, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595, {k1^0 -> -1 + k1^0, rest remain the same}>
Variables:
k1^0

Graph 2:
Transitions:
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>
Variables:
k2^0

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

Graph 4:
Transitions:
<l2, l2, undef3070 <= 0 /\ 1 <= undef1418 /\ undef1471 = 1 /\ undef3126 = 1, {all remain the same}>
<l2, l2, 1 <= undef1418 /\ 1 <= undef3070 /\ undef2997 = 0 /\ undef1471 = 1 /\ undef3126 = 1, {all remain the same}>
Variables:

Graph 5:
Transitions:
<l20, l20, 1 <= k5^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, undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1840 = 1, {all remain the same}>

Graph 2
<l11, l5, k1^0 <= 0 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>

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

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

Graph 5
<l2, l20, undef1418 <= 0 /\ undef1471 = 1 /\ undef3063 = 1 /\ undef3064 = 1, {k5^0 -> undef3011, rest remain the same}>

Graph 6
<l20, l26, k5^0 <= 0 /\ undef2390 = 1 /\ ntStatus^0 = 2, {all remain the same}>
<l20, l26, k5^0 <= 0 /\ 3 <= ntStatus^0 /\ undef2390 = 1, {all remain the same}>
<l20, l26, k5^0 <= 0 /\ ntStatus^0 <= 1 /\ undef2390 = 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.004321

Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

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

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

LOG: CALL check - Post:1 <= 0 - Process 1
* Exit transition: <l3, l2, k3^0 <= 0 /\ undef62 = 1 /\ undef1043 = 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 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, 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 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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, undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL check - Post:1 <= 0 - Process 5
* Exit transition: <l0, l11, 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001103s

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= 0 /\ undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 0 <= 0 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1595 <= 0 /\ 1 <= k1^0 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.008386s
Time used: 0.00823
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.045450s
Time used: 1.04544

LOG: SAT solveNonLinear - Elapsed time: 1.053836s
Cost: 52; Total time: 1.05367
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.011477s
Remaining time after improvement: 0.998313
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 /\ undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000742s
Time used: 1.00074

LOG: SAT solveNonLinear - Elapsed time: 1.024083s
Cost: 52; Total time: 1.0238
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.011466s
Remaining time after improvement: 0.996866
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 /\ undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001754s

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

LOG: RETURN check - Elapsed time: 2.127420s

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, k2^0 <= 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, 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.032672s
Time used: 0.032286
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000611s
Time used: 1.0006

LOG: SAT solveNonLinear - Elapsed time: 1.033283s
Cost: 51; Total time: 1.03289
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.018203s
Remaining time after improvement: 0.995178
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 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

LOG: CALL check - Post:undef1668 <= 0 - Process 9
* Exit transition: <l0, l11, undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef1668 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001171s
Postcondition: undef1668 <= 0

LOG: CALL check - Post:undef1668 <= 0 - Process 10
* Exit transition: <l0, l11, 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef1668 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001166s

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.010103s
Time used: 0.009935
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001228s
Time used: 1.00121

LOG: SAT solveNonLinear - Elapsed time: 1.011330s
Cost: 52; Total time: 1.01115
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.006382s
Remaining time after improvement: 0.997691
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001070s
Time used: 1.00106

LOG: SAT solveNonLinear - Elapsed time: 1.025131s
Cost: 52; Total time: 1.0248
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.012441s
Remaining time after improvement: 0.996198
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002181s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001232s
Time used: 1.00123

LOG: SAT solveNonLinear - Elapsed time: 1.118399s
Cost: 51; Total time: 1.11764
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.011261s
Remaining time after improvement: 0.992892
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 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.010743s
Time used: 0.010569
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.012526s
Cost: 52; Total time: 1.01234
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.006561s
Remaining time after improvement: 0.99751
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001466s
Time used: 1.00145

LOG: SAT solveNonLinear - Elapsed time: 1.026492s
Cost: 52; Total time: 1.02613
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.013001s
Remaining time after improvement: 0.995815
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002283s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.790627s
Time used: 0.790621

LOG: SAT solveNonLinear - Elapsed time: 1.002630s
Cost: 51; Total time: 1.0016
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.015464s
Remaining time after improvement: 0.990497
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 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, 0 <= 0 /\ undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= 0 /\ 1 <= k1^0 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, 0 <= 0 /\ k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.011073s
Time used: 0.010896
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002756s
Time used: 1.00275

LOG: SAT solveNonLinear - Elapsed time: 1.013830s
Cost: 52; Total time: 1.01365
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.006605s
Remaining time after improvement: 0.997446
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002022s
Time used: 1.00202

LOG: SAT solveNonLinear - Elapsed time: 1.027799s
Cost: 52; Total time: 1.02745
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.013229s
Remaining time after improvement: 0.995645
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, undef3137 <= 0 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002583s

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

LOG: RETURN check - Elapsed time: 2.095872s

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

LOG: RETURN check - Elapsed time: 11.652019s

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

LOG: Narrow transition size 1
ENTRIES:
<l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, rest remain the same}>
END ENTRIES:
GRAPH:
<l3, l3, 0 <= 0 /\ 1 <= k3^0 /\ undef62 = 1 /\ undef125 = 1 /\ undef1043 = 1, {k3^0 -> -1 + k3^0, rest remain the same}>
END GRAPH:
EXIT: <l3, l2, k3^0 <= 0 /\ undef62 = 1 /\ undef1043 = 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.003958s
Time used: 0.003859
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003573s
Time used: 1.00356

LOG: SAT solveNonLinear - Elapsed time: 1.007531s
Cost: 51; Total time: 1.00742
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.013058s
Remaining time after improvement: 0.998834
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 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef866 <= 0

LOG: Try proving POST
Postcondition: undef866 <= 0

LOG: CALL check - Post:undef866 <= 0 - Process 20
* Exit transition: <l11, l5, k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : undef866 <= 0
Postcodition moved up: undef866 <= 0

LOG: Try proving POST
Postcondition: undef866 <= 0

LOG: CALL check - Post:undef866 <= 0 - Process 21
* Exit transition: <l0, l11, undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef866 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001522s
Postcondition: undef866 <= 0

LOG: CALL check - Post:undef866 <= 0 - Process 22
* Exit transition: <l0, l11, 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef866 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001527s

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
POST: undef866 <= 0


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002263s
Time used: 1.00225

LOG: SAT solveNonLinear - Elapsed time: 1.013198s
Cost: 52; Total time: 1.01301
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.006739s
Remaining time after improvement: 0.997467
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, undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : 1 + k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001502s
Time used: 1.0015

LOG: SAT solveNonLinear - Elapsed time: 1.029202s
Cost: 52; Total time: 1.02888
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.013298s
Remaining time after improvement: 0.99564
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, undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003315s

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

LOG: RETURN check - Elapsed time: 2.100324s

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, 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.026980s
Time used: 0.026531
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000747s
Time used: 1.00073

LOG: SAT solveNonLinear - Elapsed time: 1.027727s
Cost: 51; Total time: 1.02727
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.019503s
Remaining time after improvement: 0.994513
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

LOG: CALL check - Post:undef1668 <= 0 - Process 26
* Exit transition: <l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef1668 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001623s
Postcondition: undef1668 <= 0

LOG: CALL check - Post:undef1668 <= 0 - Process 27
* Exit transition: <l0, l11, 1 <= undef866 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : undef1668 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001726s

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.011866s
Time used: 0.011663
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002325s
Time used: 1.00232

LOG: SAT solveNonLinear - Elapsed time: 1.014191s
Cost: 52; Total time: 1.01398
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.006742s
Remaining time after improvement: 0.997175
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001471s
Time used: 1.00146

LOG: SAT solveNonLinear - Elapsed time: 1.037234s
Cost: 52; Total time: 1.03687
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.013690s
Remaining time after improvement: 0.995342
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003414s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001514s
Time used: 1.00151

LOG: SAT solveNonLinear - Elapsed time: 1.090292s
Cost: 51; Total time: 1.0893
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.013628s
Remaining time after improvement: 0.991955
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1668 <= 0

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

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 0 <= undef1668 /\ 1 <= undef866 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.011895s
Time used: 0.0117
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003094s
Time used: 1.00308

LOG: SAT solveNonLinear - Elapsed time: 1.014989s
Cost: 52; Total time: 1.01478
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.007142s
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002516s
Time used: 1.00251

LOG: SAT solveNonLinear - Elapsed time: 1.032687s
Cost: 52; Total time: 1.03236
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.013726s
Remaining time after improvement: 0.995278
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003055s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.775897s
Time used: 0.775888

LOG: SAT solveNonLinear - Elapsed time: 1.002585s
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.021747s
Remaining time after improvement: 0.989333
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.011793s
Time used: 0.011599
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003914s
Time used: 1.00391

LOG: SAT solveNonLinear - Elapsed time: 1.015707s
Cost: 52; Total time: 1.01551
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.007188s
Remaining time after improvement: 0.997312
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003504s
Time used: 1.00349

LOG: SAT solveNonLinear - Elapsed time: 1.032283s
Cost: 52; Total time: 1.03194
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.013840s
Remaining time after improvement: 0.995182
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002802s

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

LOG: RETURN check - Elapsed time: 2.109315s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003060s
Time used: 1.00305

LOG: SAT solveNonLinear - Elapsed time: 1.013372s
Cost: 51; Total time: 1.01323
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.002992s
Remaining time after improvement: 0.998662
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 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef866 <= 0

LOG: Try proving POST
Postcondition: undef866 <= 0

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

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, 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.028081s
Time used: 0.027641
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001156s
Time used: 1.00115

LOG: SAT solveNonLinear - Elapsed time: 1.029237s
Cost: 51; Total time: 1.02879
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.020593s
Remaining time after improvement: 0.994717
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.012572s
Time used: 0.012366
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.017774s
Time used: 1.01777

LOG: SAT solveNonLinear - Elapsed time: 1.030345s
Cost: 52; Total time: 1.03013
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.007005s
Remaining time after improvement: 0.996998
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002300s
Time used: 1.00229

LOG: SAT solveNonLinear - Elapsed time: 1.032543s
Cost: 52; Total time: 1.03218
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.013651s
Remaining time after improvement: 0.995263
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003775s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001659s
Time used: 1.00165

LOG: SAT solveNonLinear - Elapsed time: 1.092778s
Cost: 51; Total time: 1.09175
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.014228s
Remaining time after improvement: 0.991421
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1668 <= 0

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

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 0 <= undef1668 /\ 1 <= undef866 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.012909s
Time used: 0.012703
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.016455s
Cost: 52; Total time: 1.01624
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.007398s
Remaining time after improvement: 0.997291
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003445s
Time used: 1.00343

LOG: SAT solveNonLinear - Elapsed time: 1.034714s
Cost: 52; Total time: 1.03437
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.013917s
Remaining time after improvement: 0.995095
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003128s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.773849s
Time used: 0.773843

LOG: SAT solveNonLinear - Elapsed time: 1.002601s
Cost: 51; Total time: 1.00122
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.023731s
Remaining time after improvement: 0.989257
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.012336s
Time used: 0.012144
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003921s
Time used: 1.00391

LOG: SAT solveNonLinear - Elapsed time: 1.016257s
Cost: 52; Total time: 1.01605
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.007544s
Remaining time after improvement: 0.997234
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004153s
Time used: 1.00415

LOG: SAT solveNonLinear - Elapsed time: 1.033317s
Cost: 52; Total time: 1.03297
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.013793s
Remaining time after improvement: 0.99523
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003180s

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

LOG: RETURN check - Elapsed time: 2.113150s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.979595s
Time used: 0.979583

LOG: SAT solveNonLinear - Elapsed time: 1.004071s
Cost: 51; Total time: 1.0039
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.004794s
Remaining time after improvement: 0.998349
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 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, rest remain the same}>
* Postcondition  : k3^0 <= 0
Postcodition moved up: undef866 <= 0

LOG: Try proving POST
Postcondition: undef866 <= 0

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

LOG: NarrowEntry size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l5, l5, 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813, {k2^0 -> -1 + k2^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
END ENTRIES:
GRAPH:
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef813 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef570 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef388 <= 0 /\ 1 <= k2^0 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ undef797 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
<l5, l5, 0 <= 0 /\ 1 <= k2^0 /\ 1 <= undef388 /\ 1 <= undef570 /\ 1 <= undef797 /\ 1 <= undef813 /\ 1 <= undef866 /\ undef920 = 1, {k2^0 -> -1 + k2^0, rest remain the same}>
END GRAPH:
EXIT: <l5, l3, 0 <= 0 /\ k2^0 <= 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1, {k3^0 -> undef866, 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.028418s
Time used: 0.027978
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.011112s
Time used: 1.0111

LOG: SAT solveNonLinear - Elapsed time: 1.039529s
Cost: 51; Total time: 1.03908
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.022038s
Remaining time after improvement: 0.993494
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.013027s
Time used: 0.012822
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004101s
Time used: 1.00409

LOG: SAT solveNonLinear - Elapsed time: 1.017128s
Cost: 52; Total time: 1.01692
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.007123s
Remaining time after improvement: 0.996868
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003700s
Time used: 1.00369

LOG: SAT solveNonLinear - Elapsed time: 1.034430s
Cost: 52; Total time: 1.03406
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.014116s
Remaining time after improvement: 0.994975
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003844s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.094416s
Cost: 51; Total time: 1.09337
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.015199s
Remaining time after improvement: 0.990824
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : 1 + k2^0 <= 0
Postcodition moved up: 1 + undef1668 <= 0

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

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, 0 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 0 <= undef1668 /\ 1 <= undef866 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 0 <= undef1668 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.013852s
Time used: 0.013642
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.017603s
Cost: 52; Total time: 1.01739
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.007543s
Remaining time after improvement: 0.99723
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.035574s
Cost: 52; Total time: 1.03522
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.014146s
Remaining time after improvement: 0.99493
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 <= undef1668 /\ undef3137 <= 0 /\ 1 <= undef866 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003713s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.771463s
Time used: 0.771457

LOG: SAT solveNonLinear - Elapsed time: 1.002610s
Cost: 51; Total time: 1.00122
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.024293s
Remaining time after improvement: 0.986658
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 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
* Postcondition  : k2^0 <= 0
Postcodition moved up: undef1668 <= 0

LOG: Try proving POST
Postcondition: undef1668 <= 0

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

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

LOG: NarrowEntry size 1

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

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

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

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

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

LOG: Narrow transition size 1
ENTRIES:
<l0, l11, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, 1 <= undef866 /\ 1 <= undef1668 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l11, l11, undef1595 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1544 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, undef1239 <= 0 /\ 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
<l11, l11, 1 <= k1^0 /\ 1 <= undef866 /\ 1 <= undef1239 /\ 1 <= undef1544 /\ 1 <= undef1595 /\ 1 <= undef1668 /\ undef1716 = 1 /\ undef1717 = 1, {k1^0 -> -1 + k1^0, rest remain the same}>
END GRAPH:
EXIT: <l11, l5, k1^0 <= 0 /\ 1 <= undef866 /\ undef920 = 1 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, 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.012880s
Time used: 0.012687
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.013652s
Time used: 1.01364

LOG: SAT solveNonLinear - Elapsed time: 1.026532s
Cost: 52; Total time: 1.02633
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.007990s
Remaining time after improvement: 0.99695
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004759s
Time used: 1.00475

LOG: SAT solveNonLinear - Elapsed time: 1.034701s
Cost: 52; Total time: 1.03436
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.014134s
Remaining time after improvement: 0.994995
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, undef3137 <= 0 /\ 1 <= undef866 /\ 1 <= undef1668 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
* Postcondition  : k1^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.003238s

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

LOG: RETURN check - Elapsed time: 2.127563s

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

LOG: RETURN check - Elapsed time: 9.655414s

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

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

Proving non-termination of subgraph 4
Transitions:
<l2, l2, undef3070 <= 0 /\ 1 <= undef1418 /\ undef1471 = 1 /\ undef3126 = 1, {all remain the same}>
<l2, l2, 1 <= undef1418 /\ 1 <= undef3070 /\ undef2997 = 0 /\ undef1471 = 1 /\ undef3126 = 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 /\ undef62 = 1 /\ undef1043 = 1, {all remain the same}>
Conditions: 
OPEN EXITS: 
<l3, l2, k3^0 <= 0, {all remain the same}> (condsUp: undef62 = 1, undef1043 = 1)

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

Calling reachability with...
Transition: <l5, l3, k2^0 <= 0 /\ undef920 = 1, {k3^0 -> undef866, rest remain the same}>
Conditions: k3^0 <= 0, undef62 = 1, undef1043 = 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 -> undef866, rest remain the same}> (condsUp: undef920 = 1, undef866 <= 0, undef62 = 1, undef1043 = 1)

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

Calling reachability with...
Transition: <l11, l5, k1^0 <= 0 /\ undef1716 = 1 /\ undef1717 = 1, {k2^0 -> undef1668, rest remain the same}>
Conditions: k2^0 <= 0, undef920 = 1, undef866 <= 0, undef62 = 1, undef1043 = 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 -> undef1668, rest remain the same}> (condsUp: undef1716 = 1, undef1717 = 1, undef1668 <= 0, undef920 = 1, undef866 <= 0, undef62 = 1, undef1043 = 1)

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

Calling reachability with...
Transition: <l0, l11, undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1840 = 1, {all remain the same}>
Conditions: k1^0 <= 0, undef1716 = 1, undef1717 = 1, undef1668 <= 0, undef920 = 1, undef866 <= 0, undef62 = 1, undef1043 = 1, 
Transition: <l0, l11, 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef1840 = 1, {all remain the same}>
Conditions: k1^0 <= 0, undef1716 = 1, undef1717 = 1, undef1668 <= 0, undef920 = 1, undef866 <= 0, undef62 = 1, undef1043 = 1, 
OPEN EXITS: 
<l0, l11, k1^0 <= 0 /\ undef866 <= 0 /\ undef1668 <= 0 /\ undef3137 <= 0 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>
<l0, l11, k1^0 <= 0 /\ undef866 <= 0 /\ undef1668 <= 0 /\ 1 <= undef3137 /\ k1^0 = undef1793 /\ ntStatus^0 = undef1837 /\ undef1837 = 0 /\ undef2511 = 0 /\ undef3170 = undef3171 /\ undef3170 = undef3178 /\ undef3171 = 0 /\ undef62 = 1 /\ undef920 = 1 /\ undef1043 = 1 /\ undef1716 = 1 /\ undef1717 = 1 /\ undef1840 = 1, {all remain the same}>

> Conditions are reachable!

Program does NOT terminate