NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l8, true>
<l1, l2, (0 <= (0 + k_121^0)) /\ (undef11 = (0 + a_10^0)) /\ ((1 + y_11^0) <= (0 + undef11)), par{x_12^0 -> undef11}>
<l1, l2, (0 <= (0 + k_121^0)) /\ (undef26 = (0 + a_10^0)) /\ ((1 + undef26) <= (0 + y_11^0)), par{x_12^0 -> undef26}>
<l3, l1, (undef59 = 0) /\ (undef56 = undef56) /\ (undef63 = (0 + undef56)) /\ (undef53 = (0 + undef63)) /\ (undef46 = (0 + undef53)) /\ (undef60 = (0 + undef46)) /\ (undef47 = undef47) /\ (undef57 = undef57) /\ (undef64 = (0 + undef57)) /\ (undef54 = (0 + undef64)) /\ (undef48 = (0 + undef54)) /\ (undef38 = 2) /\ (undef61 = (0 + undef48)) /\ (undef49 = undef49) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (undef58 = undef58) /\ (undef65 = (0 + undef58)) /\ (undef55 = (0 + undef65)) /\ (undef50 = (0 + undef55)) /\ (0 <= (0 + undef38)) /\ (undef36 = (1 + undef38)) /\ (undef62 = (0 + undef50)) /\ (undef51 = undef51) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (undef40 = undef40) /\ (undef43 = (0 + undef40)) /\ (undef32 = (0 + undef43)) /\ (undef52 = (0 + undef32)) /\ (0 <= (0 + undef36)) /\ (undef31 = undef31) /\ (0 <= (0 + k_121^0)) /\ (0 <= (0 + k_121^0)), par{Result_4^0 -> undef31, ___cil_tmp5_9^0 -> undef32, k_83^0 -> undef36, len_54^0 -> undef38, tmp_8^0 -> undef40, x_13^0 -> (0 + undef52), x_7^0 -> undef43, y_14^0 -> 0}>
<l2, l4, (0 <= (0 + k_121^0)) /\ ((1 + y_11^0) <= (0 + x_12^0)) /\ (undef81 = undef81) /\ (undef74 = undef74), par{len_181^0 -> 1, lt_15^0 -> undef74, x_12^0 -> (0 + undef81)}>
<l2, l4, (0 <= (0 + k_121^0)) /\ ((1 + x_12^0) <= (0 + y_11^0)) /\ (undef97 = undef97) /\ (undef90 = undef90), par{len_181^0 -> 1, lt_15^0 -> undef90, x_12^0 -> (0 + undef97)}>
<l4, l5, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((0 + y_11^0) <= (0 + x_12^0)) /\ ((0 + x_12^0) <= (0 + y_11^0)) /\ (undef113 = undef113) /\ (0 <= (0 + len_181^0)) /\ (0 <= (0 + len_181^0)) /\ (undef98 = undef98), par{Result_4^0 -> undef98}>
<l4, l6, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((1 + y_11^0) <= (0 + x_12^0)) /\ (undef129 = undef129) /\ (undef122 = undef122), par{len_181^0 -> (1 + len_181^0), lt_15^0 -> undef122, x_12^0 -> (0 + undef129)}>
<l6, l4, true>
<l4, l7, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((1 + x_12^0) <= (0 + y_11^0)) /\ (undef160 = undef160) /\ (undef153 = undef153), par{len_181^0 -> (1 + len_181^0), lt_15^0 -> undef153, x_12^0 -> (0 + undef160)}>
<l7, l4, true>
<l8, l3, true>

Fresh variables:
undef11, undef26, undef31, undef32, undef36, undef38, undef40, undef43, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef74, undef81, undef90, undef97, undef98, undef113, undef122, undef129, undef153, undef160, 

Undef variables:
undef11, undef26, undef31, undef32, undef36, undef38, undef40, undef43, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef74, undef81, undef90, undef97, undef98, undef113, undef122, undef129, undef153, undef160, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l4, (len_181^0 = 1) /\ (undef59 = 0) /\ (undef56 = undef56) /\ (undef63 = (0 + undef56)) /\ (undef53 = (0 + undef63)) /\ (undef46 = (0 + undef53)) /\ (undef60 = (0 + undef46)) /\ (undef47 = undef47) /\ (undef57 = undef57) /\ (undef64 = (0 + undef57)) /\ (undef54 = (0 + undef64)) /\ (undef48 = (0 + undef54)) /\ (undef38 = 2) /\ (undef61 = (0 + undef48)) /\ (undef49 = undef49) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (undef58 = undef58) /\ (undef65 = (0 + undef58)) /\ (undef55 = (0 + undef65)) /\ (undef50 = (0 + undef55)) /\ (0 <= (0 + undef38)) /\ (undef36 = (1 + undef38)) /\ (undef62 = (0 + undef50)) /\ (undef51 = undef51) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (undef40 = undef40) /\ (undef43 = (0 + undef40)) /\ (undef32 = (0 + undef43)) /\ (undef52 = (0 + undef32)) /\ (0 <= (0 + undef36)) /\ (undef31 = undef31) /\ (0 <= (0 + k_121^0)) /\ (0 <= (0 + k_121^0)) /\ (0 <= (0 + k_121^0)) /\ (undef11 = (0 + a_10^0)) /\ ((1 + y_11^0) <= (0 + undef11)) /\ (0 <= (0 + k_121^0)) /\ ((1 + y_11^0) <= (0 + undef11)) /\ (undef81 = undef81) /\ (undef74 = undef74), par{x_12^0 -> (0 + undef81)}>
<l0, l4, (len_181^0 = 1) /\ (undef59 = 0) /\ (undef56 = undef56) /\ (undef63 = (0 + undef56)) /\ (undef53 = (0 + undef63)) /\ (undef46 = (0 + undef53)) /\ (undef60 = (0 + undef46)) /\ (undef47 = undef47) /\ (undef57 = undef57) /\ (undef64 = (0 + undef57)) /\ (undef54 = (0 + undef64)) /\ (undef48 = (0 + undef54)) /\ (undef38 = 2) /\ (undef61 = (0 + undef48)) /\ (undef49 = undef49) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (0 <= (0 + undef38)) /\ (undef58 = undef58) /\ (undef65 = (0 + undef58)) /\ (undef55 = (0 + undef65)) /\ (undef50 = (0 + undef55)) /\ (0 <= (0 + undef38)) /\ (undef36 = (1 + undef38)) /\ (undef62 = (0 + undef50)) /\ (undef51 = undef51) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (0 <= (0 + undef36)) /\ (undef40 = undef40) /\ (undef43 = (0 + undef40)) /\ (undef32 = (0 + undef43)) /\ (undef52 = (0 + undef32)) /\ (0 <= (0 + undef36)) /\ (undef31 = undef31) /\ (0 <= (0 + k_121^0)) /\ (0 <= (0 + k_121^0)) /\ (0 <= (0 + k_121^0)) /\ (undef26 = (0 + a_10^0)) /\ ((1 + undef26) <= (0 + y_11^0)) /\ (0 <= (0 + k_121^0)) /\ ((1 + undef26) <= (0 + y_11^0)) /\ (undef97 = undef97) /\ (undef90 = undef90), par{x_12^0 -> (0 + undef97)}>
<l4, l5, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((0 + y_11^0) <= (0 + x_12^0)) /\ ((0 + x_12^0) <= (0 + y_11^0)) /\ (undef113 = undef113) /\ (0 <= (0 + len_181^0)) /\ (0 <= (0 + len_181^0)) /\ (undef98 = undef98)>
<l4, l4, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((1 + y_11^0) <= (0 + x_12^0)) /\ (undef129 = undef129) /\ (undef122 = undef122), par{len_181^0 -> (1 + len_181^0), x_12^0 -> (0 + undef129)}>
<l4, l4, (0 <= (0 + a_178^0)) /\ (0 <= (0 + len_181^0)) /\ ((1 + x_12^0) <= (0 + y_11^0)) /\ (undef160 = undef160) /\ (undef153 = undef153), par{len_181^0 -> (1 + len_181^0), x_12^0 -> (0 + undef160)}>

Fresh variables:
undef11, undef26, undef31, undef32, undef36, undef38, undef40, undef43, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef74, undef81, undef90, undef97, undef98, undef113, undef122, undef129, undef153, undef160, 

Undef variables:
undef11, undef26, undef31, undef32, undef36, undef38, undef40, undef43, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef74, undef81, undef90, undef97, undef98, undef113, undef122, undef129, undef153, undef160, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0

Graph 2:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
<l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>

Graph 2
<l4, l5, 0 <= a_178^0 /\ 0 <= len_181^0 /\ x_12^0 = y_11^0, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 4 , 1 )
( 5 , 2 )

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

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

Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001041s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003060s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006686s
Time used: 0.006486
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.016150s
Time used: 1.01613

LOG: SAT solveNonLinear - Elapsed time: 1.033168s
Cost: 2; Total time: 1.03254
Failed at location 4: 1 + a_178^0 <= 0
Failed at location 4: 1 + a_178^0 <= 0
Before Improving: 
Quasi-invariant at l4: 1 + a_178^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008678s
Remaining time after improvement: 0.998421
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: 1 + a_178^0 <= 0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
New Graphs: 
Calling Safety with literal 1 + a_178^0 <= 0 and entry <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>

LOG: CALL check - Post:1 + a_178^0 <= 0 - Process 1
* Exit transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
* Postcondition  : 1 + a_178^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001128s
Calling Safety with literal 1 + a_178^0 <= 0 and entry <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>

LOG: CALL check - Post:1 + a_178^0 <= 0 - Process 2
* Exit transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
* Postcondition  : 1 + a_178^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001166s
INVARIANTS: 
4: 
Quasi-INVARIANTS to narrow Graph: 
4: 1 + a_178^0 <= 0 , 
Narrowing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000814s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003059s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005968s
Time used: 0.005713
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.196943s
Time used: 0.191283
Improving Solution with cost 4 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000787s
Time used: 1.00076

LOG: SAT solveNonLinear - Elapsed time: 1.197730s
Cost: 4; Total time: 1.19204
Failed at location 4: y_11^0 <= x_12^0
Failed at location 4: y_11^0 <= x_12^0
Failed at location 4: x_12^0 <= y_11^0
Failed at location 4: x_12^0 <= y_11^0
Before Improving: 
Quasi-invariant at l4: y_11^0 <= x_12^0
Quasi-invariant at l4: x_12^0 <= y_11^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015011s
Remaining time after improvement: 0.997619
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: y_11^0 <= x_12^0
Quasi-invariant at l4: x_12^0 <= y_11^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
New Graphs: 
Calling Safety with literal y_11^0 <= x_12^0 and entry <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>

LOG: CALL check - Post:y_11^0 <= x_12^0 - Process 3
* Exit transition: <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
* Postcondition  : y_11^0 <= x_12^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001458s
Calling Safety with literal x_12^0 <= y_11^0 and entry <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>

LOG: CALL check - Post:x_12^0 <= y_11^0 - Process 4
* Exit transition: <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
* Postcondition  : x_12^0 <= y_11^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001449s
Calling Safety with literal y_11^0 <= x_12^0 and entry <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>

LOG: CALL check - Post:y_11^0 <= x_12^0 - Process 5
* Exit transition: <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
* Postcondition  : y_11^0 <= x_12^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001219s
Calling Safety with literal x_12^0 <= y_11^0 and entry <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>

LOG: CALL check - Post:x_12^0 <= y_11^0 - Process 6
* Exit transition: <l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
* Postcondition  : x_12^0 <= y_11^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001214s
INVARIANTS: 
4: 
Quasi-INVARIANTS to narrow Graph: 
4: x_12^0 <= y_11^0 , y_11^0 <= x_12^0 , 
Narrowing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: Narrow transition size 2
Narrowing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

LOG: Narrow transition size 2
invGraph after Narrowing: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000879s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003265s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006376s
Time used: 0.006036
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000823s
Time used: 1.0008

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 - len_181^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000682s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003729s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007518s
Time used: 0.007182
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001016s
Time used: 1.00099

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 + a_178^0 - len_181^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000809s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004458s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008277s
Time used: 0.007965
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000895s
Time used: 1.00087

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 - a_178^0 - len_181^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000902s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005014s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010064s
Time used: 0.009655
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001765s
Time used: 1.00174

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 + a_178^0 - len_181^0 + y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001083s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006264s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009285s
Time used: 0.008679
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

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

LOG: SAT solveNonLinear - Elapsed time: 1.036477s
Cost: 1; Total time: 1.02162
Quasi-ranking function: 50000 + a_178^0 - len_181^0 - y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001184s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006983s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010726s
Time used: 0.010048
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001555s
Time used: 1.00153

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 - a_178^0 - len_181^0 + y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001319s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007399s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010638s
Time used: 0.010071
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001736s
Time used: 1.00171

LOG: SAT solveNonLinear - Elapsed time: 1.038464s
Cost: 1; Total time: 1.02374
Quasi-ranking function: 50000 - len_181^0 + y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001476s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007423s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010140s
Time used: 0.009561
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001613s
Time used: 1.00159

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= a_178^0 + len_181^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, 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): 
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Quasi-ranking function: 50000 - a_178^0 - len_181^0 - y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001576s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008102s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012452s
Time used: 0.01184
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001766s
Time used: 1.00174

LOG: SAT solveNonLinear - Elapsed time: 1.040615s
Cost: 1; Total time: 1.02649
Quasi-ranking function: 50000 - len_181^0 - y_11^0
New Graphs: 
Transitions:
<l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0 /\ 50001 <= len_181^0 + y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0 /\ 50001 <= len_181^0 + y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001695s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007901s
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + x_12^0 <= y_11^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0 /\ 50001 <= len_181^0 + y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013131s
Time used: 0.012518
Trying to remove transition: <l4, l4, 0 <= a_178^0 /\ 1 + y_11^0 <= x_12^0 /\ 50001 + a_178^0 <= len_181^0 /\ 50001 + a_178^0 + y_11^0 <= len_181^0 /\ 50001 + a_178^0 <= len_181^0 + y_11^0 /\ 50001 <= a_178^0 + len_181^0 /\ 50001 + y_11^0 <= a_178^0 + len_181^0 /\ 50001 <= a_178^0 + len_181^0 + y_11^0 /\ 50001 <= len_181^0 /\ 50001 + y_11^0 <= len_181^0 /\ 50001 <= len_181^0 + y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.019725s
Time used: 4.00492

Proving non-termination of subgraph 1
Transitions:
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>
Variables:
a_178^0, len_181^0, x_12^0, y_11^0

Checking conditional non-termination of SCC {l4}...
EXIT TRANSITIONS:
<l4, end, 0 <= a_178^0 /\ 0 <= len_181^0 /\ x_12^0 = y_11^0, {all remain the same}>
<l4, end, 0 <= a_178^0 /\ 1 + len_181^0 <= 0 /\ 1 + y_11^0 <= x_12^0, {all remain the same}>
<l4, end, 0 <= a_178^0 /\ x_12^0 <= y_11^0 /\ 1 + len_181^0 <= 0, {all remain the same}>
<l4, end, 1 + a_178^0 <= 0 /\ 1 + y_11^0 <= x_12^0, {all remain the same}>
<l4, end, x_12^0 <= y_11^0 /\ 1 + a_178^0 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027285s
Time used: 0.027004
Improving Solution with cost 5 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.042821s
Time used: 0.042817

LOG: SAT solveNonLinear - Elapsed time: 0.070105s
Cost: 5; Total time: 0.069821
Failed at location 4: 1 + x_12^0 <= y_11^0
Failed at location 4: 1 + x_12^0 <= y_11^0
Before Improving: 
Quasi-invariant at l4: 1 + x_12^0 <= y_11^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011889s
Remaining time after improvement: 0.996876
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.006442s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: 1 + x_12^0 <= y_11^0
Constraint over undef 'undef160 <= x_12^0' in transition:
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

Strengthening and disabling EXIT transitions...
Closed exits from l4: 3
Strengthening exit transition (result): 
<l4, end, 0 <= a_178^0 /\ 1 + len_181^0 <= 0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, 1 + a_178^0 <= 0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ 1 + y_11^0 <= x_12^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef129, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ 0 <= len_181^0 /\ undef160 <= x_12^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

Checking conditional non-termination of SCC {l4}...
EXIT TRANSITIONS:
<l4, end, 0 <= a_178^0 /\ 1 + len_181^0 <= 0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>
<l4, end, 1 + a_178^0 <= 0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.023087s
Time used: 0.023084

LOG: SAT solveNonLinear - Elapsed time: 0.040475s
Cost: 2; Total time: 0.040139
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.013723s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: 1 <= len_181^0

Strengthening and disabling EXIT transitions...
Closed exits from l4: 1
Strengthening exit transition (result): 
<l4, end, 1 + a_178^0 <= 0 /\ 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ undef160 <= x_12^0 /\ 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

Checking conditional non-termination of SCC {l4}...
EXIT TRANSITIONS:
<l4, end, 1 + a_178^0 <= 0 /\ 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.040421s
Time used: 0.040418

LOG: SAT solveNonLinear - Elapsed time: 0.059181s
Cost: 2; Total time: 0.058927
Failed at location 4: 0 <= a_178^0
Failed at location 4: 0 <= a_178^0
Before Improving: 
Quasi-invariant at l4: 0 <= a_178^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007876s
Remaining time after improvement: 0.997384
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.005782s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: 0 <= a_178^0

Strengthening and disabling EXIT transitions...
Closed exits from l4: 1

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 0 <= a_178^0 /\ undef160 <= x_12^0 /\ 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {len_181^0 -> 1 + len_181^0, x_12^0 -> undef160, rest remain the same}>

Calling reachability with...
Transition: <l4, end, true, {all remain the same}>
Conditions: 1 + x_12^0 <= y_11^0, 1 <= len_181^0, 0 <= a_178^0, 
Transition: <l4, end, true, {all remain the same}>
Conditions: 1 + x_12^0 <= y_11^0, 1 <= len_181^0, 0 <= a_178^0, 
OPEN EXITS: 
<l4, end, 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}> (condsUp: 0 <= a_178^0)
<l4, end, 1 <= len_181^0 /\ 1 + x_12^0 <= y_11^0, {all remain the same}> (condsUp: 0 <= a_178^0)

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

Calling reachability with...
Transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
Conditions: 1 <= len_181^0, 1 + x_12^0 <= y_11^0, 0 <= a_178^0, 
Transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
Conditions: 1 <= len_181^0, 1 + x_12^0 <= y_11^0, 0 <= a_178^0, 
Transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
Conditions: 1 <= len_181^0, 1 + x_12^0 <= y_11^0, 0 <= a_178^0, 
Transition: <l0, l4, 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
Conditions: 1 <= len_181^0, 1 + x_12^0 <= y_11^0, 0 <= a_178^0, 
OPEN EXITS: 
<l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ 1 + undef81 <= y_11^0 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
<l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ 1 + undef97 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>
<l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + y_11^0 <= undef11 /\ 1 + undef81 <= y_11^0 /\ a_10^0 = undef11 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef81, rest remain the same}>
<l0, l4, 0 <= a_178^0 /\ 0 <= k_121^0 /\ 0 <= undef36 /\ 1 + undef26 <= y_11^0 /\ 1 + undef97 <= y_11^0 /\ a_10^0 = undef26 /\ undef32 = undef43 /\ undef32 = undef52 /\ undef40 = undef43 /\ undef46 = undef53 /\ undef46 = undef60 /\ undef48 = undef54 /\ undef48 = undef61 /\ undef50 = undef55 /\ undef50 = undef62 /\ undef53 = undef63 /\ undef54 = undef64 /\ undef55 = undef65 /\ undef56 = undef63 /\ undef57 = undef64 /\ undef58 = undef65 /\ undef59 = 0 /\ len_181^0 = 1 /\ undef36 = 1 + undef38 /\ undef38 = 2, {x_12^0 -> undef97, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate