NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l9, true>
<l1, l2, (undef1 > 3) /\ (undef2 > 3) /\ (undef4 > 3) /\ (undef3 > 3), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4}>
<l2, l2, ((undef5 + 1) <= arg2) /\ (undef6 <= arg1) /\ (undef6 <= arg3) /\ (undef6 <= arg4) /\ (arg2 >= (undef7 + 1)) /\ (arg2 >= (undef8 + 1)) /\ (arg1 > 0) /\ (arg2 > 0) /\ (arg3 > 0) /\ (arg4 > 0) /\ (undef5 > ~(1)) /\ (undef6 > 0) /\ (undef7 > ~(1)) /\ (undef8 > ~(1)), par{arg1 -> undef5, arg2 -> undef6, arg3 -> undef7, arg4 -> undef8}>
<l1, l3, (undef9 > 3) /\ (undef11 > ~(1)) /\ (undef10 > 4), par{arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12}>
<l3, l3, (undef14 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (arg3 > 0) /\ (undef13 > 0) /\ (undef14 > 0) /\ (undef15 > ~(1)), par{arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16}>
<l1, l4, (undef18 > 1) /\ (undef17 > 3), par{arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20}>
<l4, l4, ((undef21 + 2) <= arg1) /\ (undef21 <= arg2) /\ ((undef22 + 3) <= arg1) /\ ((undef22 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef21 > 0) /\ (undef22 > ~(1)), par{arg1 -> undef21, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}>
<l1, l5, (undef26 > 1) /\ (undef25 > 3), par{arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> undef28}>
<l5, l5, ((undef29 + 2) <= arg1) /\ (undef29 <= arg2) /\ ((undef30 + 3) <= arg1) /\ ((undef30 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef29 > 0) /\ (undef30 > ~(1)), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32}>
<l1, l6, (undef34 > 1) /\ (undef33 > 3), par{arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36}>
<l6, l6, ((undef37 + 2) <= arg1) /\ (undef37 <= arg2) /\ ((undef38 + 3) <= arg1) /\ ((undef38 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef37 > 0) /\ (undef38 > ~(1)), par{arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40}>
<l6, l3, ((undef41 + 1) <= arg1) /\ ((undef41 - 1) <= arg2) /\ ((undef42 + 1) <= arg1) /\ ((undef42 - 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef41 > 1) /\ (undef42 > 1) /\ (undef43 > ~(1)), par{arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44}>
<l6, l7, (arg1 > 2) /\ (arg2 > 0) /\ (undef45 > 4), par{arg1 -> undef45, arg2 -> undef46, arg3 -> undef47, arg4 -> undef48}>
<l6, l7, (arg1 > 2) /\ (arg2 > 0) /\ (undef49 > 2), par{arg1 -> undef49, arg2 -> undef50, arg3 -> undef51, arg4 -> undef52}>
<l8, l7, (undef53 <= arg1) /\ (arg1 > 2) /\ (undef53 > 2) /\ ((arg2 + 4) <= arg1), par{arg1 -> undef53, arg2 -> undef54, arg3 -> undef55, arg4 -> undef56}>
<l7, l3, (undef57 <= arg1) /\ ((undef58 + 1) <= arg1) /\ (arg1 > 2) /\ (undef57 > 2) /\ (undef58 > 1) /\ (undef59 > ~(1)), par{arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60}>
<l9, l1, true, par{arg1 -> undef61, arg2 -> undef62, arg3 -> undef63, arg4 -> undef64}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (undef1 > 3) /\ (undef2 > 3) /\ (undef4 > 3) /\ (undef3 > 3), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4}>
<l0, l3, (undef9 > 3) /\ (undef11 > ~(1)) /\ (undef10 > 4), par{arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12}>
<l0, l4, (undef18 > 1) /\ (undef17 > 3), par{arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20}>
<l0, l5, (undef26 > 1) /\ (undef25 > 3), par{arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> undef28}>
<l0, l6, (undef34 > 1) /\ (undef33 > 3), par{arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36}>
<l2, l2, ((undef5 + 1) <= arg2) /\ (undef6 <= arg1) /\ (undef6 <= arg3) /\ (undef6 <= arg4) /\ (arg2 >= (undef7 + 1)) /\ (arg2 >= (undef8 + 1)) /\ (arg1 > 0) /\ (arg2 > 0) /\ (arg3 > 0) /\ (arg4 > 0) /\ (undef5 > ~(1)) /\ (undef6 > 0) /\ (undef7 > ~(1)) /\ (undef8 > ~(1)), par{arg1 -> undef5, arg2 -> undef6, arg3 -> undef7, arg4 -> undef8}>
<l3, l3, (undef14 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (arg3 > 0) /\ (undef13 > 0) /\ (undef14 > 0) /\ (undef15 > ~(1)), par{arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16}>
<l4, l4, ((undef21 + 2) <= arg1) /\ (undef21 <= arg2) /\ ((undef22 + 3) <= arg1) /\ ((undef22 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef21 > 0) /\ (undef22 > ~(1)), par{arg1 -> undef21, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}>
<l5, l5, ((undef29 + 2) <= arg1) /\ (undef29 <= arg2) /\ ((undef30 + 3) <= arg1) /\ ((undef30 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef29 > 0) /\ (undef30 > ~(1)), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32}>
<l6, l6, ((undef37 + 2) <= arg1) /\ (undef37 <= arg2) /\ ((undef38 + 3) <= arg1) /\ ((undef38 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef37 > 0) /\ (undef38 > ~(1)), par{arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40}>
<l6, l3, ((undef41 + 1) <= arg1) /\ ((undef41 - 1) <= arg2) /\ ((undef42 + 1) <= arg1) /\ ((undef42 - 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef41 > 1) /\ (undef42 > 1) /\ (undef43 > ~(1)), par{arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44}>
<l6, l3, (arg1 > 2) /\ (arg2 > 0) /\ (undef45 > 4) /\ (undef57 <= undef45) /\ ((undef58 + 1) <= undef45) /\ (undef45 > 2) /\ (undef57 > 2) /\ (undef58 > 1) /\ (undef59 > ~(1)), par{arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60}>
<l6, l3, (arg1 > 2) /\ (arg2 > 0) /\ (undef49 > 2) /\ (undef57 <= undef49) /\ ((undef58 + 1) <= undef49) /\ (undef49 > 2) /\ (undef57 > 2) /\ (undef58 > 1) /\ (undef59 > ~(1)), par{arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Graph 2:
Transitions:
<l5, l5, 3 <= arg1 /\ 3 + undef30 <= arg1 /\ 1 <= arg2 /\ 1 + undef30 <= arg2 /\ 1 <= undef29 /\ undef29 <= arg2 /\ 0 <= undef30 /\ 2 + undef29 <= arg1, {arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Graph 3:
Transitions:
<l4, l4, 3 <= arg1 /\ 3 + undef22 <= arg1 /\ 1 <= arg2 /\ 1 + undef22 <= arg2 /\ 1 <= undef21 /\ undef21 <= arg2 /\ 0 <= undef22 /\ 2 + undef21 <= arg1, {arg1 -> undef21, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Graph 4:
Transitions:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Graph 5:
Transitions:
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 + undef5 <= arg2 /\ 1 + undef7 <= arg2 /\ 1 + undef8 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= undef6 /\ undef6 <= arg1 /\ undef6 <= arg3 /\ undef6 <= arg4 /\ 0 <= undef5 /\ 0 <= undef7 /\ 0 <= undef8, {arg1 -> undef5, arg2 -> undef6, arg3 -> undef7, arg4 -> undef8, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Precedence: 
Graph 0

Graph 1
<l0, l6, 4 <= undef33 /\ 2 <= undef34, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>

Graph 2
<l0, l5, 4 <= undef25 /\ 2 <= undef26, {arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> undef28, rest remain the same}>

Graph 3
<l0, l4, 4 <= undef17 /\ 2 <= undef18, {arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20, rest remain the same}>

Graph 4
<l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
<l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 0 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>
<l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ undef57 <= undef45 /\ 0 <= undef59 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
<l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ undef57 <= undef49 /\ 0 <= undef59 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>

Graph 5
<l0, l2, 4 <= undef1 /\ 4 <= undef2 /\ 4 <= undef3 /\ 4 <= undef4, {arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, rest remain the same}>

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

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

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

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000973s
Ranking function: (~(4) / 3) + (1 / 3)*arg1 + (1 / 3)*arg2
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.00174

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000760s
Ranking function: (~(4) / 3) + (1 / 3)*arg1 + (1 / 3)*arg2
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.00155

Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000754s
Ranking function: (~(4) / 3) + (1 / 3)*arg1 + (1 / 3)*arg2
New Graphs: 
Proving termination of subgraph 4
Checking unfeasibility...
Time used: 0.002444

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000577s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002435s
Trying to remove transition: <l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015855s
Time used: 0.015853

LOG: SAT solveNonLinear - Elapsed time: 0.028574s
Cost: 4; Total time: 0.028157
Failed at location 3: arg3 <= 0
Failed at location 3: arg3 <= 0
Failed at location 3: arg3 <= 0
Failed at location 3: arg3 <= 0
Before Improving: 
Quasi-invariant at l3: arg3 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002233s
Remaining time after improvement: 0.998947
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: arg3 <= 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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
New Graphs: 
Calling Safety with literal arg3 <= 0 and entry <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>

LOG: CALL check - Post:arg3 <= 0 - Process 1
* Exit transition: <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
* Postcondition  : arg3 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000365s
Calling Safety with literal arg3 <= 0 and entry <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 0 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>

LOG: CALL check - Post:arg3 <= 0 - Process 2
* Exit transition: <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 0 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>
* Postcondition  : arg3 <= 0
Postcodition moved up: undef43 <= 0

LOG: Try proving POST
Postcondition: undef43 <= 0

LOG: CALL check - Post:undef43 <= 0 - Process 3
* Exit transition: <l0, l6, 0 <= undef43 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef43 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000340s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 1 <= undef43 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 <= undef43 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 0 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>
POST: arg3 <= 0


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001241s
Time used: 1.00006

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

LOG: RETURN check - Elapsed time: 5.020456s
Calling Safety with literal arg3 <= 0 and entry <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ undef57 <= undef45 /\ 0 <= undef59 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>

LOG: CALL check - Post:arg3 <= 0 - Process 4
* Exit transition: <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ undef57 <= undef45 /\ 0 <= undef59 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
* Postcondition  : arg3 <= 0
Postcodition moved up: undef59 <= 0

LOG: Try proving POST
Postcondition: undef59 <= 0

LOG: CALL check - Post:undef59 <= 0 - Process 5
* Exit transition: <l0, l6, 3 <= undef57 /\ 1 + undef58 <= undef45 /\ undef57 <= undef45 /\ 0 <= undef59 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef59 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000475s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 3 <= undef57 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef37 <= arg2 /\ 0 <= undef38 /\ undef57 <= undef45 /\ 2 + undef37 <= arg1 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ undef57 <= undef45 /\ 0 <= undef59 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
POST: arg3 <= 0


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001442s
Time used: 1.00005

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

LOG: RETURN check - Elapsed time: 5.028293s
Calling Safety with literal arg3 <= 0 and entry <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ undef57 <= undef49 /\ 0 <= undef59 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>

LOG: CALL check - Post:arg3 <= 0 - Process 6
* Exit transition: <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ undef57 <= undef49 /\ 0 <= undef59 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
* Postcondition  : arg3 <= 0
Postcodition moved up: undef59 <= 0

LOG: Try proving POST
Postcondition: undef59 <= 0

LOG: CALL check - Post:undef59 <= 0 - Process 7
* Exit transition: <l0, l6, 3 <= undef49 /\ 3 <= undef57 /\ 1 + undef58 <= undef49 /\ undef57 <= undef49 /\ 0 <= undef59 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef59 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000507s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 3 <= undef49 /\ 3 <= undef57 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef37 <= arg2 /\ 0 <= undef38 /\ undef57 <= undef49 /\ 2 + undef37 <= arg1 /\ 2 <= undef58, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ undef57 <= undef49 /\ 0 <= undef59 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
POST: arg3 <= 0


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001605s
Time used: 1.00001

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

LOG: RETURN check - Elapsed time: 5.027510s
INVARIANTS: 
3: 
Quasi-INVARIANTS to narrow Graph: 
3: arg3 <= 0 , 
Narrowing transition: 
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000565s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002520s
Trying to remove transition: <l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.020956s
Time used: 0.020954

LOG: SAT solveNonLinear - Elapsed time: 0.050864s
Cost: 4; Total time: 0.050318
Failed at location 3: arg1 <= 2
Failed at location 3: arg1 <= 2
Failed at location 3: arg1 <= 2
Failed at location 3: arg1 <= 2
Before Improving: 
Quasi-invariant at l3: arg1 <= 2
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002849s
Remaining time after improvement: 0.998778
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: arg1 <= 2
[ 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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, 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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
New Graphs: 
Calling Safety with literal arg1 <= 2 and entry <l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>

LOG: CALL check - Post:arg1 <= 2 - Process 8
* Exit transition: <l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
* Postcondition  : arg1 <= 2

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000544s
Calling Safety with literal arg1 <= 2 and entry <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 1 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>

LOG: CALL check - Post:arg1 <= 2 - Process 9
* Exit transition: <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 1 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>
* Postcondition  : arg1 <= 2
Postcodition moved up: undef41 <= 2

LOG: Try proving POST
Postcondition: undef41 <= 2

LOG: CALL check - Post:undef41 <= 2 - Process 10
* Exit transition: <l0, l6, 1 <= undef43 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef41 <= 2

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000421s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 3 <= undef41 /\ 1 <= undef43 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef42, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 3 <= undef41 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 <= undef43 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1 /\ 2 <= undef42, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 1 + undef41 <= arg1 /\ 1 + undef42 <= arg1 /\ 1 <= arg2 /\ 1 <= undef43 /\ undef41 <= 1 + arg2 /\ undef42 <= 1 + arg2 /\ 2 <= undef41 /\ 2 <= undef42, {arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44, rest remain the same}>
POST: arg1 <= 2


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001394s
Time used: 1.00006

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

LOG: RETURN check - Elapsed time: 5.026743s
Calling Safety with literal arg1 <= 2 and entry <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>

LOG: CALL check - Post:arg1 <= 2 - Process 11
* Exit transition: <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
* Postcondition  : arg1 <= 2
Postcodition moved up: undef57 <= 2

LOG: Try proving POST
Postcondition: undef57 <= 2

LOG: CALL check - Post:undef57 <= 2 - Process 12
* Exit transition: <l0, l6, 3 <= undef57 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef57 <= 2

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000536s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 3 <= undef57 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef37 <= arg2 /\ 0 <= undef38 /\ undef57 <= undef45 /\ 2 + undef37 <= arg1 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef45 /\ 1 <= undef59 /\ undef57 <= undef45 /\ 2 <= undef58 /\ 5 <= undef45, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
POST: arg1 <= 2


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001873s
Time used: 1.00004

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

LOG: RETURN check - Elapsed time: 5.027690s
Calling Safety with literal arg1 <= 2 and entry <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>

LOG: CALL check - Post:arg1 <= 2 - Process 13
* Exit transition: <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
* Postcondition  : arg1 <= 2
Postcodition moved up: undef57 <= 2

LOG: Try proving POST
Postcondition: undef57 <= 2

LOG: CALL check - Post:undef57 <= 2 - Process 14
* Exit transition: <l0, l6, 3 <= undef49 /\ 3 <= undef57 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
* Postcondition  : undef57 <= 2

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000538s

LOG: NarrowEntry size 1
Narrowing transition: 
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ undef37 <= arg2 /\ 0 <= undef38 /\ 2 + undef37 <= arg1, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l6, 3 <= undef49 /\ 3 <= undef57 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 4 <= undef33 /\ 2 <= undef34 /\ 2 <= undef58, {arg1 -> undef33, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}>
END ENTRIES:
GRAPH:
<l6, l6, 3 <= arg1 /\ 3 + undef38 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef38 <= arg2 /\ 1 <= undef37 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef37 <= arg2 /\ 0 <= undef38 /\ undef57 <= undef49 /\ 2 + undef37 <= arg1 /\ 2 <= undef58, {arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}>
END GRAPH:
EXIT: <l6, l3, 3 <= arg1 /\ 3 <= undef49 /\ 3 <= undef57 /\ 1 <= arg2 /\ 1 + undef58 <= undef49 /\ 1 <= undef59 /\ undef57 <= undef49 /\ 2 <= undef58, {arg1 -> undef57, arg2 -> undef58, arg3 -> undef59, arg4 -> undef60, rest remain the same}>
POST: arg1 <= 2


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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.001915s
Time used: 1.00011

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

LOG: RETURN check - Elapsed time: 5.034238s
INVARIANTS: 
3: 
Quasi-INVARIANTS to narrow Graph: 
3: arg1 <= 2 , 
Narrowing transition: 
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000567s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002561s
Trying to remove transition: <l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011421s
Time used: 0.006973

Proving non-termination of subgraph 4
Transitions:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000796s
Checking conditional non-termination of SCC {l3}...
EXIT TRANSITIONS:
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ arg3 <= 0, {all remain the same}>
<l3, end, 3 <= arg1 /\ arg2 <= 0, {all remain the same}>
<l3, end, arg1 <= 2, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.063514s
Time used: 0.06351

LOG: SAT solveNonLinear - Elapsed time: 0.099346s
Cost: 4; Total time: 0.099082
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

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

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 <= arg2

Strengthening and disabling EXIT transitions...
Closed exits from l3: 1
Strengthening exit transition (result): 
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ arg3 <= 0, {all remain the same}>
Strengthening exit transition (result): 
<l3, end, 1 <= arg2 /\ arg1 <= 2, {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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

Checking conditional non-termination of SCC {l3}...
EXIT TRANSITIONS:
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ arg3 <= 0, {all remain the same}>
<l3, end, 1 <= arg2 /\ arg1 <= 2, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054429s
Time used: 0.054204
Improving Solution with cost 7 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.347607s
Time used: 0.347602
Improving Solution with cost 2 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.040179s
Time used: 0.040177

LOG: SAT solveNonLinear - Elapsed time: 0.442215s
Cost: 2; Total time: 0.441983
Failed at location 3: 3 <= arg1
Before Improving: 
Quasi-invariant at l3: 3 <= arg1
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.003499s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 3 <= arg1
Constraint over undef '7 <= undef13' in transition:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef13 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

Strengthening and disabling EXIT transitions...
Closed exits from l3: 1
Strengthening exit transition (result): 
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ arg3 <= 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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15 /\ 7 <= undef13, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

Checking conditional non-termination of SCC {l3}...
EXIT TRANSITIONS:
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ arg3 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.034286s
Time used: 0.034283

LOG: SAT solveNonLinear - Elapsed time: 0.077520s
Cost: 4; Total time: 0.077295
Failed at location 3: 1 <= arg3
Failed at location 3: 1 <= arg3
Failed at location 3: 1 <= arg3
Failed at location 3: 1 <= arg3
Before Improving: 
Quasi-invariant at l3: 1 <= arg3
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.002967s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l3: 1 <= arg3
Constraint over undef '1 <= undef15' in transition:
<l3, l3, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef14 /\ undef14 <= arg2 /\ 0 <= undef15 /\ 7 <= undef13, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

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, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef14 /\ 1 <= undef15 /\ undef14 <= arg2 /\ 7 <= undef13, {arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16, rest remain the same}>

Calling reachability with...
Transition: <l3, end, true, {all remain the same}>
Conditions: 1 <= arg2, 3 <= arg1, 1 <= arg3, 
Transition: <l3, end, true, {all remain the same}>
Conditions: 1 <= arg2, 3 <= arg1, 1 <= arg3, 
Transition: <l3, end, true, {all remain the same}>
Conditions: 1 <= arg2, 3 <= arg1, 1 <= arg3, 
Transition: <l3, end, true, {all remain the same}>
Conditions: 1 <= arg2, 3 <= arg1, 1 <= arg3, 
OPEN EXITS: 
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3, {all remain the same}>
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3, {all remain the same}>
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3, {all remain the same}>
<l3, end, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3, {all remain the same}>

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

Calling reachability with...
Transition: <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
Conditions: 3 <= arg1, 1 <= arg2, 1 <= arg3, 
Transition: <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
Conditions: 3 <= arg1, 1 <= arg2, 1 <= arg3, 
Transition: <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
Conditions: 3 <= arg1, 1 <= arg2, 1 <= arg3, 
Transition: <l0, l3, 0 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
Conditions: 3 <= arg1, 1 <= arg2, 1 <= arg3, 
OPEN EXITS: 
<l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
<l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
<l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>
<l0, l3, 1 <= undef11 /\ 4 <= undef9 /\ 5 <= undef10, {arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate