NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l29, true>
<l1, l2, true>
<l3, l4, true>
<l5, l6, true>
<l7, l8, true, par{k_1^0 -> (1 + k_1^0)}>
<l9, l7, (1 <= (0 + destflag^0))>
<l9, l7, ((1 + destflag^0) <= 0)>
<l9, l7, ((0 + destflag^0) <= 0) /\ (0 <= (0 + destflag^0))>
<l10, l7, (1 <= (0 + sourceflag^0))>
<l10, l7, ((1 + sourceflag^0) <= 0)>
<l10, l9, ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0))>
<l11, l12, true>
<l13, l14, true, par{j^0 -> (1 + j^0)}>
<l15, l13, true>
<l15, l13, true, par{destflag^0 -> 0}>
<l15, l13, true>
<l16, l10, ((0 + nodecount^0) <= (0 + j^0))>
<l16, l15, ((1 + j^0) <= (0 + nodecount^0))>
<l17, l18, true, par{j^0 -> (1 + j^0)}>
<l8, l19, true>
<l20, l17, true>
<l20, l17, true, par{sourceflag^0 -> 1}>
<l20, l17, true>
<l21, l14, ((0 + nodecount^0) <= (0 + j^0)), par{destflag^0 -> 1, j^0 -> 0}>
<l21, l20, ((1 + j^0) <= (0 + nodecount^0))>
<l22, l23, true, par{h^0 -> (1 + h^0)}>
<l24, l22, true, par{min^0 -> (0 + h^0)}>
<l24, l22, true>
<l23, l25, true>
<l25, l18, ((0 + edgecount^0) <= (0 + h^0)), par{j^0 -> 0, sourceflag^0 -> 0}>
<l25, l24, ((1 + h^0) <= (0 + edgecount^0))>
<l19, l5, ((0 + edgecount^0) <= (0 + k_1^0)), par{k^0 -> (1 + k^0)}>
<l19, l23, ((1 + k_1^0) <= (0 + edgecount^0)), par{h^0 -> 0}>
<l12, l8, ((0 + edgecount^0) <= (0 + i^0)), par{k_1^0 -> 0}>
<l12, l11, ((1 + i^0) <= (0 + edgecount^0)), par{i^0 -> (1 + i^0)}>
<l18, l21, true>
<l26, l11, true, par{i^0 -> 0, min^0 -> 0}>
<l6, l27, ((0 + k^0) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + k^0))>
<l6, l26, ((0 + nodecount^0) <= (0 + k^0))>
<l6, l26, ((1 + k^0) <= (~(1) + nodecount^0))>
<l4, l5, ((~(1) + nodecount^0) <= (0 + i^0)), par{k^0 -> 0}>
<l4, l3, ((1 + i^0) <= (~(1) + nodecount^0)), par{i^0 -> (1 + i^0)}>
<l14, l16, true>
<l2, l3, ((0 + nodecount^0) <= (0 + i^0)), par{i^0 -> 0}>
<l2, l1, ((1 + i^0) <= (0 + nodecount^0)), par{i^0 -> (1 + i^0)}>
<l28, l1, true, par{__lengthofvisited^0 -> (0 + edgecount^0), i^0 -> 1}>
<l29, l28, true>

Fresh variables:

Undef variables:

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l1, (i^0 = 1)>
<l1, l3, ((0 + nodecount^0) <= (0 + i^0)), par{i^0 -> 0}>
<l1, l1, ((1 + i^0) <= (0 + nodecount^0)), par{i^0 -> (1 + i^0)}>
<l3, l27, ((~(1) + nodecount^0) <= (0 + i^0)) /\ ((0 + 0) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + 0)), par{k^0 -> 0}>
<l3, l11, ((~(1) + nodecount^0) <= (0 + i^0)) /\ ((0 + nodecount^0) <= (0 + 0)), par{i^0 -> 0, k^0 -> 0}>
<l3, l11, ((~(1) + nodecount^0) <= (0 + i^0)) /\ ((1 + 0) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> 0}>
<l3, l3, ((1 + i^0) <= (~(1) + nodecount^0)), par{i^0 -> (1 + i^0)}>
<l11, l27, ((0 + edgecount^0) <= (0 + i^0)) /\ ((0 + edgecount^0) <= (0 + 0)) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> 0}>
<l11, l11, ((0 + edgecount^0) <= (0 + i^0)) /\ ((0 + edgecount^0) <= (0 + 0)) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> 0}>
<l11, l11, ((0 + edgecount^0) <= (0 + i^0)) /\ ((0 + edgecount^0) <= (0 + 0)) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> 0}>
<l11, l23, ((0 + edgecount^0) <= (0 + i^0)) /\ ((1 + 0) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> 0}>
<l11, l11, ((1 + i^0) <= (0 + edgecount^0)), par{i^0 -> (1 + i^0)}>
<l14, l27, ((0 + nodecount^0) <= (0 + j^0)) /\ (1 <= (0 + sourceflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ (1 <= (0 + sourceflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ (1 <= (0 + sourceflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l23, ((0 + nodecount^0) <= (0 + j^0)) /\ (1 <= (0 + sourceflag^0)) /\ ((1 + (1 + k_1^0)) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> (1 + k_1^0)}>
<l14, l27, ((0 + nodecount^0) <= (0 + j^0)) /\ ((1 + sourceflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((1 + sourceflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((1 + sourceflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l23, ((0 + nodecount^0) <= (0 + j^0)) /\ ((1 + sourceflag^0) <= 0) /\ ((1 + (1 + k_1^0)) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> (1 + k_1^0)}>
<l14, l27, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ (1 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ (1 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ (1 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l23, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ (1 <= (0 + destflag^0)) /\ ((1 + (1 + k_1^0)) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> (1 + k_1^0)}>
<l14, l27, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((1 + destflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((1 + destflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((1 + destflag^0) <= 0) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l23, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((1 + destflag^0) <= 0) /\ ((1 + (1 + k_1^0)) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> (1 + k_1^0)}>
<l14, l27, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((0 + destflag^0) <= 0) /\ (0 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + (1 + k^0)) <= (~(1) + nodecount^0)) /\ ((~(1) + nodecount^0) <= (0 + (1 + k^0))), par{k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((0 + destflag^0) <= 0) /\ (0 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((0 + nodecount^0) <= (0 + (1 + k^0))), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l11, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((0 + destflag^0) <= 0) /\ (0 <= (0 + destflag^0)) /\ ((0 + edgecount^0) <= (0 + (1 + k_1^0))) /\ ((1 + (1 + k^0)) <= (~(1) + nodecount^0)), par{i^0 -> 0, k^0 -> (1 + k^0), k_1^0 -> (1 + k_1^0)}>
<l14, l23, ((0 + nodecount^0) <= (0 + j^0)) /\ ((0 + sourceflag^0) <= 0) /\ (0 <= (0 + sourceflag^0)) /\ ((0 + destflag^0) <= 0) /\ (0 <= (0 + destflag^0)) /\ ((1 + (1 + k_1^0)) <= (0 + edgecount^0)), par{h^0 -> 0, k_1^0 -> (1 + k_1^0)}>
<l14, l14, ((1 + j^0) <= (0 + nodecount^0)), par{j^0 -> (1 + j^0)}>
<l14, l14, ((1 + j^0) <= (0 + nodecount^0)), par{destflag^0 -> 0, j^0 -> (1 + j^0)}>
<l14, l14, ((1 + j^0) <= (0 + nodecount^0)), par{j^0 -> (1 + j^0)}>
<l18, l14, ((0 + nodecount^0) <= (0 + j^0)), par{destflag^0 -> 1, j^0 -> 0}>
<l18, l18, ((1 + j^0) <= (0 + nodecount^0)), par{j^0 -> (1 + j^0)}>
<l18, l18, ((1 + j^0) <= (0 + nodecount^0)), par{j^0 -> (1 + j^0), sourceflag^0 -> 1}>
<l18, l18, ((1 + j^0) <= (0 + nodecount^0)), par{j^0 -> (1 + j^0)}>
<l23, l18, ((0 + edgecount^0) <= (0 + h^0)), par{j^0 -> 0, sourceflag^0 -> 0}>
<l23, l23, ((1 + h^0) <= (0 + edgecount^0)), par{h^0 -> (1 + h^0)}>
<l23, l23, ((1 + h^0) <= (0 + edgecount^0)), par{h^0 -> (1 + h^0)}>

Fresh variables:

Undef variables:

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l1, l1, 1 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>
Variables:
i^0, nodecount^0

Graph 2:
Transitions:
<l3, l3, 2 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>
Variables:
i^0, nodecount^0

Graph 3:
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>
<l11, l11, 1 + i^0 <= edgecount^0, {i^0 -> 1 + i^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 + sourceflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 + sourceflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 + sourceflag^0 <= 0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l14, nodecount^0 <= j^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>
<l18, l18, 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l18, 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>
<l18, l18, 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>
<l23, l18, edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, nodecount^0, j^0, k_1^0, sourceflag^0, destflag^0, h^0

Graph 4:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l1, i^0 = 1, {all remain the same}>

Graph 2
<l1, l3, nodecount^0 <= i^0, {i^0 -> 0, rest remain the same}>

Graph 3
<l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>
<l3, l11, nodecount^0 <= 1 + i^0 /\ 2 <= nodecount^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>

Graph 4
<l3, l27, nodecount^0 <= 1 + i^0 /\ nodecount^0 = 1, {k^0 -> 0, rest remain the same}>
<l11, l27, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l14, l27, 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l27, 1 + sourceflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l27, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ sourceflag^0 = 0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l27, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ sourceflag^0 = 0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l27, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0 /\ 2 + k^0 = nodecount^0, {k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 1 , 1 )
( 3 , 2 )
( 11 , 3 )
( 14 , 3 )
( 18 , 3 )
( 23 , 3 )
( 27 , 4 )

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

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

Checking conditional termination of SCC {l1}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000493s
Ranking function: -1 - i^0 + nodecount^0
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.000828

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000426s
Ranking function: -2 - i^0 + nodecount^0
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.225836
Some transition disabled by a set of invariant(s):
Invariant at l11: 0 <= i^0
Invariant at l14: 0 <= destflag^0
Invariant at l18: 1 + k_1^0 <= h^0
Invariant at l23: 1 + k_1^0 <= edgecount^0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l14, l11, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 + destflag^0 <= 0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Checking unfeasibility...
Time used: 0.416768
Some transition disabled by a set of invariant(s):
Invariant at l14: 0 <= sourceflag^0
Invariant at l18: 0 <= sourceflag^0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l14, l11, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 + sourceflag^0 <= 0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Checking unfeasibility...
Time used: 1.11665

Checking conditional termination of SCC {l11, l14, l18, l23}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.012369s
Ranking function: -5 - 10*edgecount^0 - 2*k^0 + 2*nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Variables:
destflag^0, edgecount^0, h^0, i^0, j^0, k^0, k_1^0, nodecount^0, sourceflag^0
Checking conditional termination of SCC {l11, l14, l18, l23}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008442s
Ranking function: -5 - 2*k^0 + 2*nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Variables:
destflag^0, edgecount^0, h^0, i^0, j^0, k^0, k_1^0, nodecount^0, sourceflag^0
Checking conditional termination of SCC {l11, l14, l18, l23}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005464s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.105367s
Trying to remove transition: <l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.088904s
Time used: 0.078166
Trying to remove transition: <l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.069064s
Time used: 0.06109
Trying to remove transition: <l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.037639s
Time used: 0.030152
Trying to remove transition: <l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.038464s
Time used: 0.037507
Trying to remove transition: <l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045973s
Time used: 0.044969
Trying to remove transition: <l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049917s
Time used: 0.048902
Trying to remove transition: <l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035168s
Time used: 0.034129
Trying to remove transition: <l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.076008s
Time used: 0.074897
Trying to remove transition: <l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.075369s
Time used: 0.064714
Trying to remove transition: <l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061431s
Time used: 0.050804
Trying to remove transition: <l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.258947s
Time used: 0.248313
Trying to remove transition: <l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066091s
Time used: 0.064405
Trying to remove transition: <l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.406545s
Time used: 0.404797
Trying to remove transition: <l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.071504s
Time used: 0.069657
Trying to remove transition: <l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.386729s
Time used: 0.384952
Trying to remove transition: <l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.086069s
Time used: 0.08411
Trying to remove transition: <l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059629s
Time used: 0.057715
Trying to remove transition: <l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.106806s
Time used: 0.101973
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043895s
Time used: 0.03363
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.930093s
Time used: 1.92764
Improving Solution with cost 2 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002160s
Time used: 1.00213

LOG: SAT solveNonLinear - Elapsed time: 2.932253s
Cost: 2; Total time: 2.92978
Failed at location 11: edgecount^0 + i^0 <= 0
Failed at location 11: edgecount^0 + i^0 <= 0
Before Improving: 
Quasi-invariant at l11: edgecount^0 + i^0 <= 0
Quasi-invariant at l14: 1 <= 0
Quasi-invariant at l18: 1 <= 0
Quasi-invariant at l23: 1 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.032187s
Remaining time after improvement: 0.982108
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l11: edgecount^0 + i^0 <= 0
Quasi-invariant at l14: 1 <= 0
Quasi-invariant at l18: 1 <= 0
Quasi-invariant at l23: 1 <= 0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000691s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001948s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006972s
Time used: 0.006849
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.018423s
Time used: 4.01781
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005619s
Time used: 4.00007
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006251s
Time used: 1.00018
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048388s
Time used: 0.020071
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004062s
Time used: 1.00398

LOG: SAT solveNonLinear - Elapsed time: 1.052450s
Cost: 1; Total time: 1.02405
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000641s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002235s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008551s
Time used: 0.008417
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006430s
Time used: 4.00578
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004315s
Time used: 4.00015
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006272s
Time used: 1.00001
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035292s
Time used: 0.019603
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002931s
Time used: 1.0029

LOG: SAT solveNonLinear - Elapsed time: 1.038223s
Cost: 1; Total time: 1.0225
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 + i^0 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000776s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003942s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009355s
Time used: 0.009198
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004269s
Time used: 4.00356
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004064s
Time used: 4.00002
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.013032s
Time used: 1.00001
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.037482s
Time used: 0.022159
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001839s
Time used: 1.00181

LOG: SAT solveNonLinear - Elapsed time: 1.039321s
Cost: 1; Total time: 1.02397
Termination implied by a set of invariant(s):
Invariant at l11: i^0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 + i^0 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000895s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003474s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010408s
Time used: 0.010239
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003703s
Time used: 4.00303
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004020s
Time used: 4.00002
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006945s
Time used: 1.00002
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.037200s
Time used: 0.022715
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.015971s
Time used: 1.01594

LOG: SAT solveNonLinear - Elapsed time: 1.053170s
Cost: 1; Total time: 1.03866
Quasi-ranking function: 50000 - edgecount^0 + i^0 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001028s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005074s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010218s
Time used: 0.010038
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003341s
Time used: 4.00268
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004148s
Time used: 4.00005
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006868s
Time used: 1.00001
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.038137s
Time used: 0.024013
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001722s
Time used: 1.00169

LOG: SAT solveNonLinear - Elapsed time: 1.039859s
Cost: 1; Total time: 1.0257
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001035s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004564s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011699s
Time used: 0.011521
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003743s
Time used: 4.00303
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004903s
Time used: 4.00012
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007057s
Time used: 1.00003
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.039469s
Time used: 0.024342
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001911s
Time used: 1.00188

LOG: SAT solveNonLinear - Elapsed time: 1.041380s
Cost: 1; Total time: 1.02623
Quasi-ranking function: 50000 + edgecount^0 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001084s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005439s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011465s
Time used: 0.011129
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004013s
Time used: 4.00334
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004804s
Time used: 4.00017
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007483s
Time used: 1.00012
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040643s
Time used: 0.025881
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.019833s
Time used: 1.0198

LOG: SAT solveNonLinear - Elapsed time: 1.060476s
Cost: 1; Total time: 1.04568
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001159s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005065s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011904s
Time used: 0.011565
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004342s
Time used: 4.00354
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003872s
Time used: 4.00006
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007173s
Time used: 1.00005
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.041708s
Time used: 0.026838
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004886s
Time used: 1.00483

LOG: SAT solveNonLinear - Elapsed time: 1.046594s
Cost: 1; Total time: 1.03167
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + i^0 - k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001211s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005344s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012707s
Time used: 0.012342
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005592s
Time used: 4.00485
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007225s
Time used: 4.00006
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007303s
Time used: 1.00009
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.042835s
Time used: 0.027306
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001962s
Time used: 1.00193

LOG: SAT solveNonLinear - Elapsed time: 1.044797s
Cost: 1; Total time: 1.02924
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + i^0 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001245s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005560s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012263s
Time used: 0.011902
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004942s
Time used: 4.00425
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.012597s
Time used: 4.00012
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.011397s
Time used: 1.00002
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.047222s
Time used: 0.030769
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001963s
Time used: 1.00193

LOG: SAT solveNonLinear - Elapsed time: 1.049185s
Cost: 1; Total time: 1.0327
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + i^0 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001238s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006222s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012519s
Time used: 0.012137
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004645s
Time used: 4.00394
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004371s
Time used: 4.00013
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007396s
Time used: 1.00009
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045555s
Time used: 0.02886
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.014541s
Time used: 1.0145

LOG: SAT solveNonLinear - Elapsed time: 1.060095s
Cost: 1; Total time: 1.04337
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 + i^0 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001361s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006631s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013047s
Time used: 0.012677
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005050s
Time used: 4.00434
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004322s
Time used: 4.00002
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007313s
Time used: 1.00002
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052291s
Time used: 0.02835
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002450s
Time used: 1.00242

LOG: SAT solveNonLinear - Elapsed time: 1.054740s
Cost: 1; Total time: 1.03077
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 + i^0 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001373s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006141s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013764s
Time used: 0.013381
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005357s
Time used: 4.00447
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008502s
Time used: 4.00033
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007429s
Time used: 1.00002
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046921s
Time used: 0.029818
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.022458s
Time used: 1.02243

LOG: SAT solveNonLinear - Elapsed time: 1.069380s
Cost: 1; Total time: 1.05225
Quasi-ranking function: 50000 - edgecount^0 + i^0 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001467s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007093s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014105s
Time used: 0.013706
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005142s
Time used: 4.00442
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.013033s
Time used: 4.00006
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007210s
Time used: 1.00006
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048619s
Time used: 0.031113
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.020188s
Time used: 1.02015

LOG: SAT solveNonLinear - Elapsed time: 1.068807s
Cost: 1; Total time: 1.05127
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001504s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007352s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015568s
Time used: 0.015159
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.938598s
Time used: 0.937922
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.982504s
Time used: 0.978149
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999540s
Time used: 0.992479
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048944s
Time used: 0.031474
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.960275s
Time used: 0.960228

LOG: SAT solveNonLinear - Elapsed time: 1.009219s
Cost: 1; Total time: 0.991702
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001498s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007469s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014602s
Time used: 0.014195
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.921297s
Time used: 0.91138
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.988278s
Time used: 0.984146
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000421s
Time used: 0.992609
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050646s
Time used: 0.031958
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.958746s
Time used: 0.958706

LOG: SAT solveNonLinear - Elapsed time: 1.009392s
Cost: 1; Total time: 0.990664
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001583s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007931s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016365s
Time used: 0.015792
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.907760s
Time used: 0.906903
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997623s
Time used: 0.99339
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999551s
Time used: 0.99242
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051112s
Time used: 0.03233
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.959143s
Time used: 0.959116

LOG: SAT solveNonLinear - Elapsed time: 1.010256s
Cost: 1; Total time: 0.991446
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 - k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001658s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007953s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016870s
Time used: 0.016432
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.906617s
Time used: 0.905785
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997934s
Time used: 0.993624
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003016s
Time used: 0.992349
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052379s
Time used: 0.034395
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.953352s
Time used: 0.953325

LOG: SAT solveNonLinear - Elapsed time: 1.005730s
Cost: 1; Total time: 0.98772
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001719s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006656s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016628s
Time used: 0.016197
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.907952s
Time used: 0.90709
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997895s
Time used: 0.99342
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999460s
Time used: 0.992142
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053622s
Time used: 0.035232
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.955878s
Time used: 0.955854

LOG: SAT solveNonLinear - Elapsed time: 1.009500s
Cost: 1; Total time: 0.991086
Termination implied by a set of invariant(s):
Invariant at l11: i^0 <= 1
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - i^0 - 2*k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001824s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007898s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018067s
Time used: 0.0176
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.903539s
Time used: 0.902671
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998112s
Time used: 0.993635
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000069s
Time used: 0.992023
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052915s
Time used: 0.033628
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.956762s
Time used: 0.956735

LOG: SAT solveNonLinear - Elapsed time: 1.009676s
Cost: 1; Total time: 0.990363
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 - i^0 - 2*k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001861s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.018927s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018648s
Time used: 0.018018
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.896276s
Time used: 0.88852
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.991425s
Time used: 0.986824
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000101s
Time used: 0.991988
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053533s
Time used: 0.033655
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.956506s
Time used: 0.956479

LOG: SAT solveNonLinear - Elapsed time: 1.010039s
Cost: 1; Total time: 0.990134
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - i^0 - 2*k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001976s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009505s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018831s
Time used: 0.018211
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.908195s
Time used: 0.907321
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.988171s
Time used: 0.983602
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999376s
Time used: 0.988872
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059622s
Time used: 0.03933
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.948429s
Time used: 0.948399

LOG: SAT solveNonLinear - Elapsed time: 1.008051s
Cost: 1; Total time: 0.987729
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 - i^0 - 2*k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002029s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011924s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019974s
Time used: 0.019337
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.893080s
Time used: 0.892158
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997730s
Time used: 0.993277
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002927s
Time used: 0.991813
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056364s
Time used: 0.036134
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.951379s
Time used: 0.951352

LOG: SAT solveNonLinear - Elapsed time: 1.007742s
Cost: 1; Total time: 0.987486
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + i^0 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - i^0 - 2*k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002107s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010101s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019579s
Time used: 0.019064
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.895155s
Time used: 0.894194
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998142s
Time used: 0.99359
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999888s
Time used: 0.991785
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058010s
Time used: 0.037469
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.967702s
Time used: 0.967676

LOG: SAT solveNonLinear - Elapsed time: 1.025713s
Cost: 1; Total time: 1.00514
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - i^0 - 2*k^0 - nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002142s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.013975s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021106s
Time used: 0.020596
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.885984s
Time used: 0.885049
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.985412s
Time used: 0.980901
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000324s
Time used: 0.992135
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057394s
Time used: 0.037459
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.951578s
Time used: 0.951552

LOG: SAT solveNonLinear - Elapsed time: 1.008973s
Cost: 1; Total time: 0.989011
Quasi-ranking function: 50000 - i^0 - 2*k^0 + nodecount^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002187s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011280s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021712s
Time used: 0.021026
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.911737s
Time used: 0.904599
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.991139s
Time used: 0.986744
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999485s
Time used: 0.992225
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062452s
Time used: 0.041511
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.949380s
Time used: 0.94934

LOG: SAT solveNonLinear - Elapsed time: 1.011832s
Cost: 1; Total time: 0.990851
Termination implied by a set of invariant(s):
Invariant at l11: i^0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 + edgecount^0 - i^0 - 2*k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002264s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.025079s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021680s
Time used: 0.02097
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.875068s
Time used: 0.874121
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997625s
Time used: 0.993344
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999202s
Time used: 0.992059
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063398s
Time used: 0.042579
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.948916s
Time used: 0.948899

LOG: SAT solveNonLinear - Elapsed time: 1.012314s
Cost: 1; Total time: 0.991478
Termination implied by a set of invariant(s):
Invariant at l11: 0 <= 1 + k^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ 0 <= k^0 /\ i^0 <= 1 /\ i^0 <= 1 + k^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Quasi-ranking function: 50000 - edgecount^0 - i^0 - 2*k^0
New Graphs: 
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, k_1^0, nodecount^0
Checking conditional termination of SCC {l11}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002318s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010035s
Trying to remove transition: <l11, l11, edgecount^0 <= 0 /\ edgecount^0 + i^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 0 <= i^0 + k^0 /\ i^0 <= 1 /\ 50001 + edgecount^0 + i^0 <= k^0 /\ 50001 + edgecount^0 + i^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 + i^0 <= k^0 + nodecount^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 + edgecount^0 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 + edgecount^0 <= k^0 /\ 50001 + edgecount^0 + nodecount^0 <= k^0 /\ 50001 + edgecount^0 <= k^0 + nodecount^0 /\ 50001 + i^0 <= edgecount^0 + k^0 /\ 50001 + i^0 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 + i^0 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 + nodecount^0 <= edgecount^0 + i^0 + 2*k^0 /\ 50001 <= edgecount^0 + i^0 + 2*k^0 + nodecount^0 /\ 50001 <= edgecount^0 + k^0 /\ 50001 + nodecount^0 <= edgecount^0 + k^0 /\ 50001 <= edgecount^0 + k^0 + nodecount^0 /\ 50001 + i^0 <= k^0 /\ 50001 + i^0 + nodecount^0 <= k^0 /\ 50001 + i^0 <= k^0 + nodecount^0 /\ 50001 <= i^0 + 2*k^0 /\ 50001 + nodecount^0 <= i^0 + 2*k^0 /\ 50001 <= i^0 + 2*k^0 + nodecount^0 /\ 50001 <= k^0 /\ 50001 + nodecount^0 <= k^0 /\ 50001 <= k^0 + nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021961s
Time used: 0.021242
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.889047s
Time used: 0.88805
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996834s
Time used: 0.993016
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006213s
Time used: 0.99226
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.004761s
Time used: 0.985482
Termination failed. Trying to show unreachability...
Proving unreachability of entry: <l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>

LOG: CALL check - Post:1 <= 0 - Process 1
* Exit transition: <l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, 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 2
* Exit transition: <l1, l3, nodecount^0 <= i^0 /\ nodecount^0 <= 0, {i^0 -> 0, 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: <l0, l1, i^0 = 1, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.007827s

LOG: NarrowEntry size 1
Narrowing transition: 
<l1, l1, 1 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l1, 0 <= 0 /\ i^0 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l1, l1, 1 + i^0 <= nodecount^0 /\ 0 <= 0, {i^0 -> 1 + i^0, rest remain the same}>
END GRAPH:
EXIT: <l1, l3, nodecount^0 <= i^0 /\ nodecount^0 <= 0, {i^0 -> 0, 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.023503s
Time used: 0.023365
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011278s
Time used: 0.011276

LOG: SAT solveNonLinear - Elapsed time: 0.034782s
Cost: 1; Total time: 0.034641
Failed at location 1: 1 <= nodecount^0
Before Improving: 
Quasi-invariant at l1: 1 <= nodecount^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001479s
Remaining time after improvement: 0.999006
Postcondition implied by a set of quasi-invariant(s):
Quasi-invariant at l1: 1 <= nodecount^0
Postcondition: 1 <= nodecount^0

LOG: CALL check - Post:1 <= nodecount^0 - Process 4
* Exit transition: <l0, l1, 0 <= 0 /\ i^0 = 1, {all remain the same}>
* Postcondition  : 1 <= nodecount^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.009547s

LOG: NarrowEntry size 1
INVARIANTS: 
1: 
Quasi-INVARIANTS to narrow Graph: 
1: 1 <= nodecount^0 , 
Narrowing transition: 
<l1, l1, 1 + i^0 <= nodecount^0 /\ 0 <= 0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l1, 0 <= 0 /\ nodecount^0 <= 0 /\ i^0 = 1, {all remain the same}>
END ENTRIES:
GRAPH:
<l1, l1, 1 + i^0 <= nodecount^0 /\ 0 <= 0 /\ nodecount^0 <= 0, {i^0 -> 1 + i^0, rest remain the same}>
END GRAPH:
EXIT: <l1, l3, nodecount^0 <= i^0 /\ nodecount^0 <= 0, {i^0 -> 0, 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.023525s
Time used: 0.023387
Improving Solution with cost 50 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011945s
Time used: 0.011932

LOG: SAT solveNonLinear - Elapsed time: 0.035470s
Cost: 50; Total time: 0.035319
Some transition disabled by a set of invariant(s):
Invariant at l1: 1 + nodecount^0 <= i^0
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l1, l1, 1 + i^0 <= nodecount^0 /\ 0 <= 0 /\ nodecount^0 <= 0, {i^0 -> 1 + i^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001829s
Time used: 0.000917
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014293s
Time used: 0.014227
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002938s
Time used: 1.00281

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

LOG: RETURN check - Elapsed time: 1.175221s

LOG: NarrowEntry size 1
Narrowing transition: 
<l3, l3, 2 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l1, l3, 0 <= 0 /\ nodecount^0 <= i^0 /\ nodecount^0 <= 0, {i^0 -> 0, rest remain the same}>
END ENTRIES:
GRAPH:
<l3, l3, 0 <= 0 /\ nodecount^0 <= 0 /\ 2 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>
END GRAPH:
EXIT: <l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, 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.023504s
Time used: 0.023364
Improving Solution with cost 50 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010631s
Time used: 0.010628

LOG: SAT solveNonLinear - Elapsed time: 0.034135s
Cost: 50; Total time: 0.033992
Some transition disabled by a set of invariant(s):
Invariant at l3: nodecount^0 <= 1 + i^0
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ nodecount^0 <= 0 /\ 2 + i^0 <= nodecount^0, {i^0 -> 1 + i^0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001828s
Time used: 0.000921
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013799s
Time used: 0.013732
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003585s
Time used: 1.00347

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

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

Proving non-termination of subgraph 3
Transitions:
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0, {i^0 -> 1 + i^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l23, nodecount^0 <= j^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0, {j^0 -> 1 + j^0, rest remain the same}>
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0, {h^0 -> 1 + h^0, rest remain the same}>
Variables:
edgecount^0, i^0, k^0, nodecount^0, j^0, k_1^0, sourceflag^0, destflag^0, h^0

Checking conditional non-termination of SCC {l11, l14, l18, l23}...
EXIT TRANSITIONS:
<l11, end, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 2 + k^0 = nodecount^0, {all remain the same}>
<l14, end, 1 <= destflag^0 /\ 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 2 + k^0 = nodecount^0, {all remain the same}>
<l14, end, 1 <= sourceflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ destflag^0 = 0 /\ 2 + k^0 = nodecount^0, {all remain the same}>
<l14, end, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ sourceflag^0 = 0 /\ 2 + k^0 = nodecount^0, {all remain the same}>
<l14, end, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0 /\ 2 + k^0 = nodecount^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.211499s
Time used: 0.210432
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.045573s
Time used: 0.045569

LOG: SAT solveNonLinear - Elapsed time: 0.257072s
Cost: 1; Total time: 0.256001
Failed at location 11: nodecount^0 <= k^0
Before Improving: 
Quasi-invariant at l11: nodecount^0 <= k^0
Quasi-invariant at l14: nodecount^0 <= 1 + k^0
Quasi-invariant at l18: nodecount^0 <= 1 + k^0
Quasi-invariant at l23: nodecount^0 <= 1 + k^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009200s
Remaining time after improvement: 0.993574
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l11: nodecount^0 <= k^0
Quasi-invariant at l14: nodecount^0 <= 1 + k^0
Quasi-invariant at l18: nodecount^0 <= 1 + k^0
Quasi-invariant at l23: nodecount^0 <= 1 + k^0

Strengthening and disabling EXIT transitions...
Closed exits from l11: 1
Closed exits from l14: 4

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l11, l11, edgecount^0 <= 0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l23, 1 <= edgecount^0 /\ edgecount^0 <= i^0 /\ 0 <= i^0 /\ nodecount^0 <= k^0, {h^0 -> 0, k_1^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l11, l11, 1 + i^0 <= edgecount^0 /\ 0 <= i^0 /\ nodecount^0 <= k^0, {i^0 -> 1 + i^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= sourceflag^0 /\ 0 <= destflag^0 /\ nodecount^0 <= j^0 /\ nodecount^0 <= 1 + k^0 /\ 2 + k_1^0 <= edgecount^0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, 1 <= destflag^0 /\ nodecount^0 <= j^0 /\ nodecount^0 <= 1 + k^0 /\ 2 + k_1^0 <= edgecount^0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ nodecount^0 <= 1 + k^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l14, l11, nodecount^0 <= j^0 /\ edgecount^0 <= 1 + k_1^0 /\ 3 + k^0 <= nodecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {i^0 -> 0, k^0 -> 1 + k^0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l23, nodecount^0 <= j^0 /\ nodecount^0 <= 1 + k^0 /\ 2 + k_1^0 <= edgecount^0 /\ destflag^0 = 0 /\ sourceflag^0 = 0, {h^0 -> 0, k_1^0 -> 1 + k_1^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {destflag^0 -> 0, j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l14, l14, 1 + j^0 <= nodecount^0 /\ 0 <= destflag^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l14, 1 + k_1^0 <= h^0 /\ nodecount^0 <= j^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {destflag^0 -> 1, j^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 1 + j^0, sourceflag^0 -> 1, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l18, l18, 1 + k_1^0 <= h^0 /\ 1 + j^0 <= nodecount^0 /\ 0 <= sourceflag^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 1 + j^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l18, 1 + k_1^0 <= edgecount^0 /\ edgecount^0 <= h^0 /\ nodecount^0 <= 1 + k^0, {j^0 -> 0, sourceflag^0 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0 /\ nodecount^0 <= 1 + k^0, {h^0 -> 1 + h^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l23, l23, 1 + h^0 <= edgecount^0 /\ 1 + k_1^0 <= edgecount^0 /\ nodecount^0 <= 1 + k^0, {h^0 -> 1 + h^0, rest remain the same}>

Calling reachability with...
Transition: <l11, end, true, {all remain the same}>
Conditions: nodecount^0 <= k^0, 
Transition: <l11, end, true, {all remain the same}>
Conditions: nodecount^0 <= k^0, 
OPEN EXITS: 
<l11, end, nodecount^0 <= k^0, {all remain the same}>
<l11, end, nodecount^0 <= k^0, {all remain the same}>

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

Calling reachability with...
Transition: <l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= k^0, 
Transition: <l3, l11, nodecount^0 <= 1 + i^0 /\ 2 <= nodecount^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= k^0, 
Transition: <l3, l11, nodecount^0 <= 0 /\ nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= k^0, 
Transition: <l3, l11, nodecount^0 <= 1 + i^0 /\ 2 <= nodecount^0, {i^0 -> 0, k^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= k^0, 
OPEN EXITS: 
<l3, l11, nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}> (condsUp: nodecount^0 <= 0, nodecount^0 <= 0)
<l3, l11, nodecount^0 <= 1 + i^0, {i^0 -> 0, k^0 -> 0, rest remain the same}> (condsUp: nodecount^0 <= 0, nodecount^0 <= 0)

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

Calling reachability with...
Transition: <l1, l3, nodecount^0 <= i^0, {i^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= 1 + i^0, nodecount^0 <= 0, nodecount^0 <= 0, 
Transition: <l1, l3, nodecount^0 <= i^0, {i^0 -> 0, rest remain the same}>
Conditions: nodecount^0 <= 1 + i^0, nodecount^0 <= 0, nodecount^0 <= 0, 
OPEN EXITS: 
<l1, l3, nodecount^0 <= i^0, {i^0 -> 0, rest remain the same}> (condsUp: nodecount^0 <= 1, nodecount^0 <= 0, nodecount^0 <= 0)
<l1, l3, nodecount^0 <= i^0, {i^0 -> 0, rest remain the same}> (condsUp: nodecount^0 <= 1, nodecount^0 <= 0, nodecount^0 <= 0)

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

Calling reachability with...
Transition: <l0, l1, i^0 = 1, {all remain the same}>
Conditions: nodecount^0 <= i^0, nodecount^0 <= 1, nodecount^0 <= 0, nodecount^0 <= 0, 
Transition: <l0, l1, i^0 = 1, {all remain the same}>
Conditions: nodecount^0 <= i^0, nodecount^0 <= 1, nodecount^0 <= 0, nodecount^0 <= 0, 
OPEN EXITS: 
<l0, l1, nodecount^0 <= i^0 /\ nodecount^0 <= 0 /\ i^0 = 1, {all remain the same}>
<l0, l1, nodecount^0 <= i^0 /\ nodecount^0 <= 0 /\ i^0 = 1, {all remain the same}>

> Conditions are reachable!

Program does NOT terminate