NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l13, true>
<l1, l2, (undef16 = (0 + b_128^0)) /\ ((5 + (~(1) * undef16)) <= 0) /\ (undef10 = undef10) /\ (undef4 = 1) /\ (undef2 = (0 + undef4)) /\ (undef15 = (0 + undef2)) /\ (undef1 = undef1), par{Result_4^0 -> undef1, __cil_tmp2_7^0 -> undef2, __retres1_6^0 -> undef4, lt_13^0 -> undef10, tmp_11^0 -> (0 + undef15)}>
<l1, l3, (undef33 = (0 + b_128^0)) /\ (0 <= (4 + (~(1) * undef33))) /\ (undef26 = undef26) /\ (undef32 = (0 + b_128^0)) /\ (undef25 = undef25) /\ (undef20 = 0) /\ (undef18 = (0 + undef20)) /\ (undef31 = (0 + undef18)) /\ (undef17 = undef17), par{Result_4^0 -> undef17, __cil_tmp2_7^0 -> undef18, __retres1_6^0 -> undef20, lt_12^0 -> undef25, lt_13^0 -> undef26, tmp_11^0 -> (0 + undef31)}>
<l4, l5, (((0 + (~(1) * x_8^0)) + y_9^0) <= 0) /\ (undef34 = undef34), par{Result_4^0 -> undef34}>
<l4, l6, (0 <= ((~(1) + (~(1) * x_8^0)) + y_9^0))>
<l3, l1, ((0 + tmp_11^0) <= 0) /\ (0 <= (0 + tmp_11^0)) /\ (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0))>
<l7, l3, (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef92 = 0) /\ (0 <= (4 + (~(1) * undef92))) /\ (undef85 = undef85) /\ (undef91 = 0) /\ (undef84 = undef84) /\ (undef79 = 0) /\ (undef77 = (0 + undef79)) /\ (undef90 = (0 + undef77)) /\ (undef76 = undef76), par{Result_4^0 -> undef76, __cil_tmp2_7^0 -> undef77, __retres1_6^0 -> undef79, lt_12^0 -> undef84, lt_13^0 -> undef85, tmp_11^0 -> (0 + undef90)}>
<l7, l4, (((0 + (~(1) * y_9^0)) + z_10^0) <= 0), par{x_8^0 -> (1 + x_8^0)}>
<l2, l8, (undef109 = __disjvr_0^0) /\ (__disjvr_0^0 = undef109), par{__disjvr_0^0 -> undef109}>
<l8, l7, true, par{y_9^0 -> (1 + y_9^0)}>
<l6, l3, (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef151 = 0) /\ (0 <= (4 + (~(1) * undef151))) /\ (undef144 = undef144) /\ (undef150 = 0) /\ (undef143 = undef143) /\ (undef138 = 0) /\ (undef136 = (0 + undef138)) /\ (undef149 = (0 + undef136)) /\ (undef135 = undef135), par{Result_4^0 -> undef135, __cil_tmp2_7^0 -> undef136, __retres1_6^0 -> undef138, lt_12^0 -> undef143, lt_13^0 -> undef144, tmp_11^0 -> (0 + undef149)}>
<l6, l4, (((0 + (~(1) * y_9^0)) + z_10^0) <= 0), par{x_8^0 -> (1 + x_8^0)}>
<l9, l4, (undef173 = undef173), par{count_5^0 -> undef173}>
<l10, l3, (undef196 = ~(1)) /\ (0 <= (4 + (~(1) * undef196))) /\ (undef189 = undef189) /\ (undef195 = ~(1)) /\ (undef188 = undef188) /\ (undef183 = 0) /\ (undef181 = (0 + undef183)) /\ (undef194 = (0 + undef181)) /\ (undef180 = undef180), par{Result_4^0 -> undef180, __cil_tmp2_7^0 -> undef181, __retres1_6^0 -> undef183, b_51^0 -> ~(2), lt_12^0 -> undef188, lt_13^0 -> undef189, tmp_11^0 -> (0 + undef194)}>
<l11, l3, (undef213 = (0 + b_51^0)) /\ (0 <= (4 + (~(1) * undef213))) /\ (undef206 = undef206) /\ (undef212 = (0 + b_51^0)) /\ (undef205 = undef205) /\ (undef200 = 0) /\ (undef198 = (0 + undef200)) /\ (undef211 = (0 + undef198)) /\ (undef197 = undef197), par{Result_4^0 -> undef197, __cil_tmp2_7^0 -> undef198, __retres1_6^0 -> undef200, b_76^0 -> (~(1) + b_51^0), lt_12^0 -> undef205, lt_13^0 -> undef206, tmp_11^0 -> (0 + undef211)}>
<l11, l2, (undef229 = (0 + b_51^0)) /\ ((5 + (~(1) * undef229)) <= 0) /\ (undef223 = undef223) /\ (undef217 = 1) /\ (undef215 = (0 + undef217)) /\ (undef228 = (0 + undef215)) /\ (undef214 = undef214), par{Result_4^0 -> undef214, __cil_tmp2_7^0 -> undef215, __retres1_6^0 -> undef217, lt_13^0 -> undef223, tmp_11^0 -> (0 + undef228)}>
<l12, l3, (undef246 = ~(1)) /\ (0 <= (4 + (~(1) * undef246))) /\ (undef239 = undef239) /\ (undef245 = ~(1)) /\ (undef238 = undef238) /\ (undef233 = 0) /\ (undef231 = (0 + undef233)) /\ (undef244 = (0 + undef231)) /\ (undef230 = undef230), par{Result_4^0 -> undef230, __cil_tmp2_7^0 -> undef231, __retres1_6^0 -> undef233, b_128^0 -> ~(2), lt_12^0 -> undef238, lt_13^0 -> undef239, tmp_11^0 -> (0 + undef244)}>
<l13, l9, true>

Fresh variables:
undef1, undef2, undef4, undef10, undef15, undef16, undef17, undef18, undef20, undef25, undef26, undef31, undef32, undef33, undef34, undef76, undef77, undef79, undef84, undef85, undef90, undef91, undef92, undef109, undef135, undef136, undef138, undef143, undef144, undef149, undef150, undef151, undef173, undef180, undef181, undef183, undef188, undef189, undef194, undef195, undef196, undef197, undef198, undef200, undef205, undef206, undef211, undef212, undef213, undef214, undef215, undef217, undef223, undef228, undef229, undef230, undef231, undef233, undef238, undef239, undef244, undef245, undef246, 

Undef variables:
undef1, undef2, undef4, undef10, undef15, undef16, undef17, undef18, undef20, undef25, undef26, undef31, undef32, undef33, undef34, undef76, undef77, undef79, undef84, undef85, undef90, undef91, undef92, undef109, undef135, undef136, undef138, undef143, undef144, undef149, undef150, undef151, undef173, undef180, undef181, undef183, undef188, undef189, undef194, undef195, undef196, undef197, undef198, undef200, undef205, undef206, undef211, undef212, undef213, undef214, undef215, undef217, undef223, undef228, undef229, undef230, undef231, undef233, undef238, undef239, undef244, undef245, undef246, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l4, (undef173 = undef173)>
<l3, l3, ((0 + tmp_11^0) <= 0) /\ (0 <= (0 + tmp_11^0)) /\ (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef16 = (0 + b_128^0)) /\ ((5 + (~(1) * undef16)) <= 0) /\ (undef10 = undef10) /\ (undef4 = 1) /\ (undef2 = (0 + undef4)) /\ (undef15 = (0 + undef2)) /\ (undef1 = undef1) /\ (undef109 = __disjvr_0^0) /\ (__disjvr_0^0 = undef109) /\ (0 <= ((~(1) + (~(1) * (1 + y_9^0))) + z_10^0)) /\ (undef92 = 0) /\ (0 <= (4 + (~(1) * undef92))) /\ (undef85 = undef85) /\ (undef91 = 0) /\ (undef84 = undef84) /\ (undef79 = 0) /\ (undef77 = (0 + undef79)) /\ (undef90 = (0 + undef77)) /\ (undef76 = undef76), par{__disjvr_0^0 -> undef109, tmp_11^0 -> (0 + undef90), y_9^0 -> (1 + y_9^0)}>
<l3, l4, ((0 + tmp_11^0) <= 0) /\ (0 <= (0 + tmp_11^0)) /\ (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef16 = (0 + b_128^0)) /\ ((5 + (~(1) * undef16)) <= 0) /\ (undef10 = undef10) /\ (undef4 = 1) /\ (undef2 = (0 + undef4)) /\ (undef15 = (0 + undef2)) /\ (undef1 = undef1) /\ (undef109 = __disjvr_0^0) /\ (__disjvr_0^0 = undef109) /\ (((0 + (~(1) * (1 + y_9^0))) + z_10^0) <= 0), par{__disjvr_0^0 -> undef109, tmp_11^0 -> (0 + undef15), x_8^0 -> (1 + x_8^0), y_9^0 -> (1 + y_9^0)}>
<l3, l3, ((0 + tmp_11^0) <= 0) /\ (0 <= (0 + tmp_11^0)) /\ (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef33 = (0 + b_128^0)) /\ (0 <= (4 + (~(1) * undef33))) /\ (undef26 = undef26) /\ (undef32 = (0 + b_128^0)) /\ (undef25 = undef25) /\ (undef20 = 0) /\ (undef18 = (0 + undef20)) /\ (undef31 = (0 + undef18)) /\ (undef17 = undef17), par{tmp_11^0 -> (0 + undef31)}>
<l4, l5, (((0 + (~(1) * x_8^0)) + y_9^0) <= 0) /\ (undef34 = undef34)>
<l4, l3, (0 <= ((~(1) + (~(1) * x_8^0)) + y_9^0)) /\ (0 <= ((~(1) + (~(1) * y_9^0)) + z_10^0)) /\ (undef151 = 0) /\ (0 <= (4 + (~(1) * undef151))) /\ (undef144 = undef144) /\ (undef150 = 0) /\ (undef143 = undef143) /\ (undef138 = 0) /\ (undef136 = (0 + undef138)) /\ (undef149 = (0 + undef136)) /\ (undef135 = undef135), par{tmp_11^0 -> (0 + undef149)}>
<l4, l4, (0 <= ((~(1) + (~(1) * x_8^0)) + y_9^0)) /\ (((0 + (~(1) * y_9^0)) + z_10^0) <= 0), par{x_8^0 -> (1 + x_8^0)}>

Fresh variables:
undef1, undef2, undef4, undef10, undef15, undef16, undef17, undef18, undef20, undef25, undef26, undef31, undef32, undef33, undef34, undef76, undef77, undef79, undef84, undef85, undef90, undef91, undef92, undef109, undef135, undef136, undef138, undef143, undef144, undef149, undef150, undef151, undef173, undef180, undef181, undef183, undef188, undef189, undef194, undef195, undef196, undef197, undef198, undef200, undef205, undef206, undef211, undef212, undef213, undef214, undef215, undef217, undef223, undef228, undef229, undef230, undef231, undef233, undef238, undef239, undef244, undef245, undef246, 

Undef variables:
undef1, undef2, undef4, undef10, undef15, undef16, undef17, undef18, undef20, undef25, undef26, undef31, undef32, undef33, undef34, undef76, undef77, undef79, undef84, undef85, undef90, undef91, undef92, undef109, undef135, undef136, undef138, undef143, undef144, undef149, undef150, undef151, undef173, undef180, undef181, undef183, undef188, undef189, undef194, undef195, undef196, undef197, undef198, undef200, undef205, undef206, undef211, undef212, undef213, undef214, undef215, undef217, undef223, undef228, undef229, undef230, undef231, undef233, undef238, undef239, undef244, undef245, undef246, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0

Graph 2:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l4, true, {all remain the same}>

Graph 2
<l4, l5, y_9^0 <= x_8^0, {all remain the same}>

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

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

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

Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003909s
Ranking function: -35 + b_128^0 - 15*y_9^0 + 15*z_10^0
New Graphs: 
Transitions:
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, x_8^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001909s
Ranking function: -71 + 14*b_128^0 - y_9^0 + z_10^0
New Graphs: 
Transitions:
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000501s
Ranking function: -1 - x_8^0 + y_9^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000451s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001910s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.040167s
Time used: 0.040164

LOG: SAT solveNonLinear - Elapsed time: 0.066133s
Cost: 1; Total time: 0.065646
Failed at location 4: 1 + z_10^0 <= x_8^0
Before Improving: 
Quasi-invariant at l3: 1 + tmp_11^0 <= 0
Quasi-invariant at l4: 1 + z_10^0 <= x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007010s
Remaining time after improvement: 0.997523
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 + tmp_11^0 <= 0
Quasi-invariant at l4: 1 + z_10^0 <= x_8^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + z_10^0 <= x_8^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 1 + z_10^0 <= x_8^0 and entry <l0, l4, true, {all remain the same}>

LOG: CALL check - Post:1 + z_10^0 <= x_8^0 - Process 1
* Exit transition: <l0, l4, true, {all remain the same}>
* Postcondition  : 1 + z_10^0 <= x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000325s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 1 + tmp_11^0 <= 0 , 
4: 1 + z_10^0 <= x_8^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003056s
Ranking function: -73 + 14*b_128^0 - 3*y_9^0 + 3*z_10^0
New Graphs: 
Transitions:
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000563s
Ranking function: -x_8^0 + z_10^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000448s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001910s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.029802s
Time used: 0.0298

LOG: SAT solveNonLinear - Elapsed time: 0.050321s
Cost: 1; Total time: 0.049748
Failed at location 4: 1 + y_9^0 <= x_8^0
Before Improving: 
Quasi-invariant at l3: 1 <= tmp_11^0
Quasi-invariant at l4: 1 + y_9^0 <= x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007031s
Remaining time after improvement: 0.997439
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 <= tmp_11^0
Quasi-invariant at l4: 1 + y_9^0 <= x_8^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 1 + y_9^0 <= x_8^0 and entry <l0, l4, x_8^0 <= z_10^0, {all remain the same}>

LOG: CALL check - Post:1 + y_9^0 <= x_8^0 - Process 2
* Exit transition: <l0, l4, x_8^0 <= z_10^0, {all remain the same}>
* Postcondition  : 1 + y_9^0 <= x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000495s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 1 <= tmp_11^0 , 
4: 1 + y_9^0 <= x_8^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003082s
Ranking function: -73 + 14*b_128^0 - 3*y_9^0 + 3*z_10^0
New Graphs: 
Transitions:
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000577s
Ranking function: -x_8^0 + z_10^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000458s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001907s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.036339s
Time used: 0.036336

LOG: SAT solveNonLinear - Elapsed time: 0.059141s
Cost: 1; Total time: 0.058525
Failed at location 4: y_9^0 <= x_8^0
Before Improving: 
Quasi-invariant at l3: 1 + tmp_11^0 <= 0
Quasi-invariant at l4: y_9^0 <= x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006990s
Remaining time after improvement: 0.997606
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 + tmp_11^0 <= 0
Quasi-invariant at l4: y_9^0 <= x_8^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal y_9^0 <= x_8^0 and entry <l0, l4, x_8^0 <= y_9^0 /\ x_8^0 <= z_10^0, {all remain the same}>

LOG: CALL check - Post:y_9^0 <= x_8^0 - Process 3
* Exit transition: <l0, l4, x_8^0 <= y_9^0 /\ x_8^0 <= z_10^0, {all remain the same}>
* Postcondition  : y_9^0 <= x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000546s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 1 + tmp_11^0 <= 0 , 
4: y_9^0 <= x_8^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003094s
Ranking function: -73 + 14*b_128^0 - 3*y_9^0 + 3*z_10^0
New Graphs: 
Transitions:
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000584s
Ranking function: -x_8^0 + z_10^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000454s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001899s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.050309s
Time used: 0.050307

LOG: SAT solveNonLinear - Elapsed time: 0.076098s
Cost: 1; Total time: 0.075468
Failed at location 4: z_10^0 <= x_8^0
Before Improving: 
Quasi-invariant at l3: 1 <= tmp_11^0
Quasi-invariant at l4: z_10^0 <= x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007909s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002780s
Remaining time after improvement: 0.994512
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 <= tmp_11^0
Quasi-invariant at l4: z_10^0 <= 1 + x_8^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal z_10^0 <= 1 + x_8^0 and entry <l0, l4, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0, {all remain the same}>

LOG: CALL check - Post:z_10^0 <= 1 + x_8^0 - Process 4
* Exit transition: <l0, l4, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0, {all remain the same}>
* Postcondition  : z_10^0 <= 1 + x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000409s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 1 <= tmp_11^0 , 
4: z_10^0 <= 1 + x_8^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, x_8^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, x_8^0 <= z_10^0 /\ z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003123s
Ranking function: -71 + 14*b_128^0 - y_9^0 + z_10^0
New Graphs: 
Transitions:
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000597s
Ranking function: -1 - x_8^0 + y_9^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000463s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001902s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.045447s
Time used: 0.045444

LOG: SAT solveNonLinear - Elapsed time: 0.068459s
Cost: 1; Total time: 0.067811
Failed at location 4: 1 + z_10^0 <= y_9^0
Before Improving: 
Quasi-invariant at l3: z_10^0 <= y_9^0
Quasi-invariant at l4: 1 + z_10^0 <= y_9^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007056s
Remaining time after improvement: 0.997575
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: z_10^0 <= y_9^0
Quasi-invariant at l4: 1 + z_10^0 <= y_9^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 1 + z_10^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 1 + z_10^0 <= y_9^0 and entry <l0, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>

LOG: CALL check - Post:1 + z_10^0 <= y_9^0 - Process 5
* Exit transition: <l0, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>
* Postcondition  : 1 + z_10^0 <= y_9^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000424s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: z_10^0 <= y_9^0 , 
4: 1 + z_10^0 <= y_9^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l4, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ y_9^0 = z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003132s
Ranking function: -35 + b_128^0 - 15*y_9^0 + 15*z_10^0
New Graphs: 
Transitions:
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ y_9^0 = z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, x_8^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002119s
Ranking function: -5 + b_128^0 - y_9^0 + z_10^0
New Graphs: 
Transitions:
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ y_9^0 = z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
Variables:
x_8^0, y_9^0, z_10^0
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000597s
Ranking function: -1 - x_8^0 + y_9^0
New Graphs: 
Transitions:
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000458s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001938s
Trying to remove transition: <l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.032102s
Time used: 0.0321

LOG: SAT solveNonLinear - Elapsed time: 0.061832s
Cost: 1; Total time: 0.061198
Failed at location 4: z_10^0 <= y_9^0
Before Improving: 
Quasi-invariant at l3: 1 <= 0
Quasi-invariant at l4: z_10^0 <= y_9^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007556s
Remaining time after improvement: 0.997024
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 <= 0
Quasi-invariant at l4: z_10^0 <= y_9^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: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ y_9^0 = z_10^0, {x_8^0 -> 1 + x_8^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
It's unfeasible. Removing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal z_10^0 <= y_9^0 and entry <l0, l4, y_9^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>

LOG: CALL check - Post:z_10^0 <= y_9^0 - Process 6
* Exit transition: <l0, l4, y_9^0 <= z_10^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>
* Postcondition  : z_10^0 <= y_9^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000464s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 1 <= 0 , 
4: z_10^0 <= y_9^0 , 
Narrowing transition: 
<l3, l3, 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
It's unfeasible. Removing transition: 
<l3, l4, 5 <= undef16 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ 1 + y_9^0 = z_10^0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef15, x_8^0 -> 1 + x_8^0, y_9^0 -> 1 + y_9^0, rest remain the same}>
Narrowing transition: 
<l3, l3, 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
It's unfeasible. Removing transition: 
<l4, l4, 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ y_9^0 = z_10^0, {x_8^0 -> 1 + x_8^0, rest remain the same}>
invGraph after Narrowing: 
Transitions:
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001616s
Ranking function: -1 - y_9^0 + z_10^0
New Graphs: 
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000489s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002026s
Trying to remove transition: <l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.027707s
Time used: 0.027705

LOG: SAT solveNonLinear - Elapsed time: 0.157963s
Cost: 1; Total time: 0.157386
Failed at location 4: 3 + z_10^0 <= b_128^0 + x_8^0
Before Improving: 
Quasi-invariant at l3: 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0
Quasi-invariant at l4: 3 + z_10^0 <= b_128^0 + x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005256s
Remaining time after improvement: 0.997622
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0
Quasi-invariant at l4: 3 + z_10^0 <= b_128^0 + x_8^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 3 + z_10^0 <= b_128^0 + x_8^0 and entry <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>

LOG: CALL check - Post:3 + z_10^0 <= b_128^0 + x_8^0 - Process 7
* Exit transition: <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0, {all remain the same}>
* Postcondition  : 3 + z_10^0 <= b_128^0 + x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000525s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 , 
4: 3 + z_10^0 <= b_128^0 + x_8^0 , 
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002447s
Ranking function: -67 + 13*b_128^0 - y_9^0 + z_10^0
New Graphs: 
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000553s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002548s
Trying to remove transition: <l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.030982s
Time used: 0.03098

LOG: SAT solveNonLinear - Elapsed time: 0.233365s
Cost: 1; Total time: 0.232781
Failed at location 4: 4 + z_10^0 <= b_128^0 + y_9^0
Before Improving: 
Quasi-invariant at l3: 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0
Quasi-invariant at l4: 4 + z_10^0 <= b_128^0 + y_9^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005508s
Remaining time after improvement: 0.997663
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0
Quasi-invariant at l4: 4 + z_10^0 <= b_128^0 + y_9^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: 
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 4 + z_10^0 <= b_128^0 + y_9^0 and entry <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0, {all remain the same}>

LOG: CALL check - Post:4 + z_10^0 <= b_128^0 + y_9^0 - Process 8
* Exit transition: <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0, {all remain the same}>
* Postcondition  : 4 + z_10^0 <= b_128^0 + y_9^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000803s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 , 
4: 4 + z_10^0 <= b_128^0 + y_9^0 , 
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002668s
Ranking function: -19 + b_128^0 - 7*y_9^0 + 7*z_10^0
New Graphs: 
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000609s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002895s
Trying to remove transition: <l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.027828s
Time used: 0.027825

LOG: SAT solveNonLinear - Elapsed time: 0.261001s
Cost: 1; Total time: 0.260316
Failed at location 4: 4 + y_9^0 <= b_128^0 + x_8^0
Before Improving: 
Quasi-invariant at l3: 5 <= b_128^0 + tmp_11^0
Quasi-invariant at l4: 4 + y_9^0 <= b_128^0 + x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006351s
Remaining time after improvement: 0.996799
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 5 <= b_128^0 + tmp_11^0
Quasi-invariant at l4: 4 + y_9^0 <= b_128^0 + x_8^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l3, l3, 0 <= 0 /\ 5 <= b_128^0 + tmp_11^0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 4 + y_9^0 <= b_128^0 + x_8^0 and entry <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>

LOG: CALL check - Post:4 + y_9^0 <= b_128^0 + x_8^0 - Process 9
* Exit transition: <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
* Postcondition  : 4 + y_9^0 <= b_128^0 + x_8^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000632s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 5 <= b_128^0 + tmp_11^0 , 
4: 4 + y_9^0 <= b_128^0 + x_8^0 , 
It's unfeasible. Removing transition: 
<l3, l3, 0 <= 0 /\ 5 <= undef16 /\ 2 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ __disjvr_0^0 = undef109 /\ b_128^0 = undef16 /\ tmp_11^0 = 0 /\ undef2 = undef4 /\ undef2 = undef15 /\ undef77 = undef79 /\ undef77 = undef90 /\ undef79 = 0 /\ undef91 = 0 /\ undef92 = 0 /\ undef4 = 1, {__disjvr_0^0 -> undef109, tmp_11^0 -> undef90, y_9^0 -> 1 + y_9^0, rest remain the same}>
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000655s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003325s
Trying to remove transition: <l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.032005s
Time used: 0.032002

LOG: SAT solveNonLinear - Elapsed time: 0.279236s
Cost: 1; Total time: 0.278643
Failed at location 4: 5 <= b_128^0
Before Improving: 
Quasi-invariant at l3: 5 <= b_128^0
Quasi-invariant at l4: 5 <= b_128^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004799s
Remaining time after improvement: 0.997802
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 5 <= b_128^0
Quasi-invariant at l4: 5 <= b_128^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: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
New Graphs: 
Calling Safety with literal 5 <= b_128^0 and entry <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>

LOG: CALL check - Post:5 <= b_128^0 - Process 10
* Exit transition: <l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
* Postcondition  : 5 <= b_128^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000717s
INVARIANTS: 
3: 
4: 
Quasi-INVARIANTS to narrow Graph: 
3: 5 <= b_128^0 , 
4: 5 <= b_128^0 , 
Narrowing transition: 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0
Checking conditional termination of SCC {l3, l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001408s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.006728s
Trying to remove transition: <l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009132s
Time used: 0.008283
Trying to remove transition: <l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.034409s
Time used: 0.034406

LOG: SAT solveNonLinear - Elapsed time: 0.067365s
Cost: 1; Total time: 0.066247
Failed at location 4: 1 + y_9^0 <= tmp_11^0 + x_8^0
Before Improving: 
Quasi-invariant at l3: 1 + x_8^0 <= y_9^0
Quasi-invariant at l4: 1 + y_9^0 <= tmp_11^0 + x_8^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003723s
Remaining time after improvement: 0.992164
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: x_8^0 <= y_9^0
Quasi-invariant at l4: y_9^0 <= tmp_11^0 + x_8^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l3, l3, 0 <= 0 /\ x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, y_9^0 <= tmp_11^0 + x_8^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, 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): 
<l3, l3, 0 <= 0 /\ x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, y_9^0 <= tmp_11^0 + x_8^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Ranking function: tmp_11^0 + x_8^0 - y_9^0
New Graphs: 
Transitions:
<l3, l3, 0 <= 0 /\ x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Variables:
b_128^0, tmp_11^0, x_8^0, y_9^0, z_10^0
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000741s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003748s
Trying to remove transition: <l3, l3, 0 <= 0 /\ x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022571s
Time used: 0.01388

Proving non-termination of subgraph 1
Transitions:
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>
Variables:
__disjvr_0^0, b_128^0, tmp_11^0, y_9^0, z_10^0, x_8^0

Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005183s
Checking conditional non-termination of SCC {l3, l4}...
EXIT TRANSITIONS:
<l3, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 <= 4, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 <= 4, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 1 <= tmp_11^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ z_10^0 <= y_9^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 1 <= tmp_11^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 1 + tmp_11^0 <= 0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, z_10^0 <= y_9^0 /\ 1 <= tmp_11^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ z_10^0 <= y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ z_10^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 <= 4 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ z_10^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 5 <= b_128^0 /\ 1 + y_9^0 <= z_10^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 1 + y_9^0 <= z_10^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ b_128^0 <= 4 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 1 + y_9^0 <= z_10^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 5 <= b_128^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 5 <= b_128^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l4, end, y_9^0 <= x_8^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.389335s
Time used: 2.38752
Improving Solution with cost 39 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001191s
Time used: 1.00118

LOG: SAT solveNonLinear - Elapsed time: 3.390526s
Cost: 39; Total time: 3.3887
Failed at location 4: 1 + x_8^0 <= y_9^0
Before Improving: 
Quasi-invariant at l3: 1 + y_9^0 <= z_10^0
Quasi-invariant at l4: 1 + x_8^0 <= y_9^0
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

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

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 + y_9^0 <= z_10^0
Quasi-invariant at l4: 1 + x_8^0 <= y_9^0

Strengthening and disabling EXIT transitions...
Closed exits from l3: 11
Closed exits from l4: 9
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^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): 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

Checking conditional non-termination of SCC {l3, l4}...
EXIT TRANSITIONS:
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + z_10^0 <= b_128^0 + tmp_11^0 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, tmp_11^0 <= 0 /\ 5 <= b_128^0 /\ 5 <= b_128^0 + tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 5 <= b_128^0 + tmp_11^0 /\ 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 4 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 <= 4 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + y_9^0 <= b_128^0 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ 3 + z_10^0 <= b_128^0 + x_8^0, {all remain the same}>
<l4, end, 5 <= b_128^0 /\ 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 + x_8^0 <= 2 + z_10^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.893880s
Time used: 0.892712
Improving Solution with cost 15 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.007997s
Time used: 1.00799

LOG: SAT solveNonLinear - Elapsed time: 1.901876s
Cost: 15; Total time: 1.9007
Failed at location 4: b_128^0 <= 0
Before Improving: 
Quasi-invariant at l3: b_128^0 + tmp_11^0 <= 0
Quasi-invariant at l4: b_128^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.020863s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.016818s
Quasi-invariant improved

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

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

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: b_128^0 + tmp_11^0 <= 2
Quasi-invariant at l4: b_128^0 <= 2

Strengthening and disabling EXIT transitions...
Closed exits from l3: 7
Closed exits from l4: 5
Strengthening exit transition (result): 
<l3, end, 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 2 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
Strengthening exit transition (result): 
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^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): 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

Checking conditional non-termination of SCC {l3, l4}...
EXIT TRANSITIONS:
<l3, end, 5 <= b_128^0 /\ 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ 4 + tmp_11^0 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0, {all remain the same}>
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l3, end, 1 + tmp_11^0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ 4 + z_10^0 <= b_128^0 + y_9^0 /\ b_128^0 <= 2 /\ 3 + z_10^0 <= b_128^0 + x_8^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ z_10^0 <= 1 + x_8^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>
<l4, end, z_10^0 <= y_9^0 /\ 1 + x_8^0 <= y_9^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.441950s
Time used: 0.440917
Improving Solution with cost 3 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.587013s
Time used: 0.58701

LOG: SAT solveNonLinear - Elapsed time: 1.028963s
Cost: 3; Total time: 1.02793
Failed at location 4: 1 + y_9^0 <= z_10^0
Before Improving: 
Quasi-invariant at l3: 0 <= tmp_11^0
Quasi-invariant at l4: 1 + y_9^0 <= z_10^0
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

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

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 0 <= tmp_11^0
Quasi-invariant at l4: 1 + y_9^0 <= z_10^0

Strengthening and disabling EXIT transitions...
Closed exits from l3: 3
Closed exits from l4: 3
Strengthening exit transition (result): 
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^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): 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

Checking conditional non-termination of SCC {l3, l4}...
EXIT TRANSITIONS:
<l3, end, 1 <= tmp_11^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174484s
Time used: 0.174407

LOG: SAT solveNonLinear - Elapsed time: 0.174484s
Cost: 0; Total time: 0.174407
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

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

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

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

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l3, l3, 0 <= 0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 + tmp_11^0 <= 2 /\ b_128^0 <= 4 /\ undef33 <= 4 /\ b_128^0 + tmp_11^0 + y_9^0 <= 3 + z_10^0 /\ b_128^0 + y_9^0 <= 3 + tmp_11^0 + z_10^0 /\ b_128^0 = undef32 /\ b_128^0 = undef33 /\ tmp_11^0 = 0 /\ undef18 = undef20 /\ undef18 = undef31 /\ undef20 = 0, {tmp_11^0 -> undef31, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l3, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ 2 + x_8^0 <= z_10^0 /\ b_128^0 <= 2 /\ b_128^0 + x_8^0 <= 2 + z_10^0 /\ b_128^0 + x_8^0 <= 3 + y_9^0 /\ b_128^0 + y_9^0 <= 3 + z_10^0 /\ undef136 = undef138 /\ undef136 = undef149 /\ undef138 = 0 /\ undef150 = 0 /\ undef151 = 0, {tmp_11^0 -> undef149, rest remain the same}>

Calling reachability with...
Transition: <l4, end, true, {all remain the same}>
Conditions: 1 + x_8^0 <= y_9^0, b_128^0 <= 2, 1 + y_9^0 <= z_10^0, 
OPEN EXITS: 
<l4, end, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0, {all remain the same}> (condsUp: b_128^0 <= 2)

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

Calling reachability with...
Transition: <l0, l4, true, {all remain the same}>
Conditions: 1 + x_8^0 <= y_9^0, 1 + y_9^0 <= z_10^0, b_128^0 <= 2, 
OPEN EXITS: 
<l0, l4, 1 + x_8^0 <= y_9^0 /\ 1 + y_9^0 <= z_10^0 /\ b_128^0 <= 2, {all remain the same}>

> Conditions are reachable!

Program does NOT terminate