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 -> 1}>
<l27, l26, ((0 + ntStatus^0) <= 2) /\ (2 <= (0 + ntStatus^0))>
<l27, l25, (3 <= (0 + ntStatus^0))>
<l27, l25, ((1 + ntStatus^0) <= 2)>
<l26, l28, true>
<l28, l26, true>
<l21, l20, (1 <= (0 + k5^0)), 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.004348

Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

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

> 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.000996s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001060s
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.001043s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001111s

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.008424s
Time used: 0.008265
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.046298s
Time used: 1.04627

LOG: SAT solveNonLinear - Elapsed time: 1.054722s
Cost: 52; Total time: 1.05454
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.011427s
Remaining time after improvement: 0.998326
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.001331s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000788s
Time used: 1.00078

LOG: SAT solveNonLinear - Elapsed time: 1.024239s
Cost: 52; Total time: 1.02395
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.99725
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.001701s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001775s

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

LOG: RETURN check - Elapsed time: 2.128296s

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.032767s
Time used: 0.032376
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000671s
Time used: 1.00066

LOG: SAT solveNonLinear - Elapsed time: 1.033438s
Cost: 51; Total time: 1.03303
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.018168s
Remaining time after improvement: 0.995146
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.001121s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001188s
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.001123s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001191s

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.010130s
Time used: 0.00996
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001090s
Time used: 1.00108

LOG: SAT solveNonLinear - Elapsed time: 1.011220s
Cost: 52; Total time: 1.01104
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.006373s
Remaining time after improvement: 0.997692
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.001608s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001256s
Time used: 1.00124

LOG: SAT solveNonLinear - Elapsed time: 1.025369s
Cost: 52; Total time: 1.02502
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.012401s
Remaining time after improvement: 0.996254
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.002105s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002182s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.118785s
Cost: 51; Total time: 1.11802
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.011364s
Remaining time after improvement: 0.992775
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.010769s
Time used: 0.010596
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.012557s
Cost: 52; Total time: 1.01237
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.006600s
Remaining time after improvement: 0.997493
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.001735s
> 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.024998s
Time used: 0.024661
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001383s
Time used: 1.00137

LOG: SAT solveNonLinear - Elapsed time: 1.026380s
Cost: 52; Total time: 1.02603
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.012989s
Remaining time after improvement: 0.995835
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.002269s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002346s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.790454s
Time used: 0.790443

LOG: SAT solveNonLinear - Elapsed time: 1.002705s
Cost: 51; Total time: 1.00166
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.018344s
Remaining time after improvement: 0.990728
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.011085s
Time used: 0.010909
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.013855s
Cost: 52; Total time: 1.01367
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.006547s
Remaining time after improvement: 0.997673
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.001819s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002076s
Time used: 1.00206

LOG: SAT solveNonLinear - Elapsed time: 1.027929s
Cost: 52; Total time: 1.02757
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.013322s
Remaining time after improvement: 0.995586
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.002496s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002573s

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

LOG: RETURN check - Elapsed time: 2.096121s

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

LOG: RETURN check - Elapsed time: 11.655639s

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.004010s
Time used: 0.003905
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003012s
Time used: 1.00299

LOG: SAT solveNonLinear - Elapsed time: 1.007022s
Cost: 51; Total time: 1.0069
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.012964s
Remaining time after improvement: 0.998856
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.001536s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001605s
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.001448s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001518s

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.011046s
Time used: 0.010866
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002479s
Time used: 1.0024

LOG: SAT solveNonLinear - Elapsed time: 1.013525s
Cost: 52; Total time: 1.01327
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.006718s
Remaining time after improvement: 0.997459
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.002579s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001673s
Time used: 1.00166

LOG: SAT solveNonLinear - Elapsed time: 1.029376s
Cost: 52; Total time: 1.02904
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.013174s
Remaining time after improvement: 0.995654
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.003199s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003278s

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

LOG: RETURN check - Elapsed time: 2.100766s

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.026978s
Time used: 0.026525
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000820s
Time used: 1.00078

LOG: SAT solveNonLinear - Elapsed time: 1.027798s
Cost: 51; Total time: 1.0273
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.019473s
Remaining time after improvement: 0.994498
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.001520s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001602s
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.001621s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001694s

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.011931s
Time used: 0.011724
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004623s
Time used: 1.0046

LOG: SAT solveNonLinear - Elapsed time: 1.016554s
Cost: 52; Total time: 1.01633
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.010328s
Remaining time after improvement: 0.996991
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.003259s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001427s
Time used: 1.00141

LOG: SAT solveNonLinear - Elapsed time: 1.031040s
Cost: 52; Total time: 1.03067
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.013603s
Remaining time after improvement: 0.995354
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.003190s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003273s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001531s
Time used: 1.00152

LOG: SAT solveNonLinear - Elapsed time: 1.090769s
Cost: 51; Total time: 1.08978
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.013398s
Remaining time after improvement: 0.99195
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.011980s
Time used: 0.011778
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003045s
Time used: 1.00303

LOG: SAT solveNonLinear - Elapsed time: 1.015025s
Cost: 52; Total time: 1.01481
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.007163s
Remaining time after improvement: 0.997101
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.002657s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002628s
Time used: 1.00261

LOG: SAT solveNonLinear - Elapsed time: 1.032791s
Cost: 52; Total time: 1.03244
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.013573s
Remaining time after improvement: 0.995296
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.002979s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003064s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.776190s
Time used: 0.77618

LOG: SAT solveNonLinear - Elapsed time: 1.002633s
Cost: 51; Total time: 1.00125
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.017193s
Remaining time after improvement: 0.989014
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.011657s
Time used: 0.011464
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004035s
Time used: 1.00402

LOG: SAT solveNonLinear - Elapsed time: 1.015692s
Cost: 52; Total time: 1.01549
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.997292
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.001914s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003529s
Time used: 1.00352

LOG: SAT solveNonLinear - Elapsed time: 1.032354s
Cost: 52; Total time: 1.03201
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.013694s
Remaining time after improvement: 0.995204
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.002693s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002778s

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

LOG: RETURN check - Elapsed time: 2.110179s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003115s
Time used: 1.0031

LOG: SAT solveNonLinear - Elapsed time: 1.013473s
Cost: 51; Total time: 1.01332
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.002981s
Remaining time after improvement: 0.998512
Some transition disabled by a set of quasi-invariant(s):
Quasi-invariant at l3: k3^0 <= 0

LOG: NEXT CALL check - disable

LOG: CALL check - Post:k3^0 <= 0 - Process 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.027953s
Time used: 0.027503
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001077s
Time used: 1.00107

LOG: SAT solveNonLinear - Elapsed time: 1.029031s
Cost: 51; Total time: 1.02857
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.020464s
Remaining time after improvement: 0.994709
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.012654s
Time used: 0.012444
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.018725s
Time used: 1.01871

LOG: SAT solveNonLinear - Elapsed time: 1.031379s
Cost: 52; Total time: 1.03116
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.007031s
Remaining time after improvement: 0.996977
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.002747s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002285s
Time used: 1.00227

LOG: SAT solveNonLinear - Elapsed time: 1.032894s
Cost: 52; Total time: 1.0325
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.013575s
Remaining time after improvement: 0.995292
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.003697s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003780s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.092393s
Cost: 51; Total time: 1.09138
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.014051s
Remaining time after improvement: 0.991538
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.012926s
Time used: 0.012714
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003718s
Time used: 1.00371

LOG: SAT solveNonLinear - Elapsed time: 1.016644s
Cost: 52; Total time: 1.01642
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.007352s
Remaining time after improvement: 0.997221
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.003751s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003277s
Time used: 1.00327

LOG: SAT solveNonLinear - Elapsed time: 1.034589s
Cost: 52; Total time: 1.03424
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.013790s
Remaining time after improvement: 0.995145
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.003048s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003137s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.772041s
Time used: 0.772024

LOG: SAT solveNonLinear - Elapsed time: 1.002632s
Cost: 51; Total time: 1.00124
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.023617s
Remaining time after improvement: 0.989304
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.012256s
Time used: 0.012062
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.016185s
Cost: 52; Total time: 1.01597
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.007593s
Remaining time after improvement: 0.997198
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.002068s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004399s
Time used: 1.00439

LOG: SAT solveNonLinear - Elapsed time: 1.033543s
Cost: 52; Total time: 1.0332
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.013732s
Remaining time after improvement: 0.995238
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.003110s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003190s

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

LOG: RETURN check - Elapsed time: 2.113528s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.979247s
Time used: 0.979234

LOG: SAT solveNonLinear - Elapsed time: 1.003727s
Cost: 51; Total time: 1.00356
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.004773s
Remaining time after improvement: 0.998594
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.028380s
Time used: 0.027932
Improving Solution with cost 51 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.014369s
Time used: 1.01435

LOG: SAT solveNonLinear - Elapsed time: 1.042749s
Cost: 51; Total time: 1.04228
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.018549s
Remaining time after improvement: 0.994314
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.012781s
Time used: 0.012573
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.016965s
Cost: 52; Total time: 1.01675
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.007038s
Remaining time after improvement: 0.996916
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.002913s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.034271s
Cost: 52; Total time: 1.03391
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.014033s
Remaining time after improvement: 0.995001
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.003727s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003816s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001785s
Time used: 1.00177

LOG: SAT solveNonLinear - Elapsed time: 1.094470s
Cost: 51; Total time: 1.09342
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.014898s
Remaining time after improvement: 0.990444
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.013862s
Time used: 0.013648
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004012s
Time used: 1.00399

LOG: SAT solveNonLinear - Elapsed time: 1.017874s
Cost: 52; Total time: 1.01764
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.007310s
Remaining time after improvement: 0.997286
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.003674s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003563s
Time used: 1.00355

LOG: SAT solveNonLinear - Elapsed time: 1.035331s
Cost: 52; Total time: 1.03498
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.013990s
Remaining time after improvement: 0.994973
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.003608s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003692s

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

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.772372s
Time used: 0.772362

LOG: SAT solveNonLinear - Elapsed time: 1.002604s
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.024143s
Remaining time after improvement: 0.98915
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.012777s
Time used: 0.012582
Improving Solution with cost 52 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.012419s
Time used: 1.0124

LOG: SAT solveNonLinear - Elapsed time: 1.025196s
Cost: 52; Total time: 1.02498
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.007821s
Remaining time after improvement: 0.997184
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.002088s
> Postcondition is not implied!

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004712s
Time used: 1.0047

LOG: SAT solveNonLinear - Elapsed time: 1.034373s
Cost: 52; Total time: 1.03402
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.013997s
Remaining time after improvement: 0.995012
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.003074s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.003153s

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

LOG: RETURN check - Elapsed time: 2.125212s

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

LOG: RETURN check - Elapsed time: 9.652694s

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

LOG: RETURN check - Elapsed time: 45.678885s
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