YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l9, true>
<l1, l2, (undef3 = undef3) /\ (undef4 = undef4), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef3, oldX3^0 -> undef4, x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}>
<l3, l2, (undef9 = undef9) /\ (undef10 = undef10), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef9, oldX3^0 -> undef10, x0^0 -> (0 + undef9), x1^0 -> (0 + undef10)}>
<l3, l4, (undef13 = (0 + x0^0)) /\ (undef14 = (0 + x1^0)), par{oldX0^0 -> undef13, oldX1^0 -> undef14, x0^0 -> (1 + undef13), x1^0 -> (~(2) + undef14)}>
<l5, l1, (undef19 = (0 + x0^0)) /\ (undef20 = (0 + x1^0)) /\ ((0 + undef20) <= 2), par{oldX0^0 -> undef19, oldX1^0 -> undef20, x0^0 -> (0 + undef19), x1^0 -> (0 + undef20)}>
<l5, l3, (undef25 = (0 + x0^0)) /\ (undef26 = (0 + x1^0)) /\ (3 <= (0 + undef26)), par{oldX0^0 -> undef25, oldX1^0 -> undef26, x0^0 -> (0 + undef25), x1^0 -> (0 + undef26)}>
<l6, l2, (undef33 = undef33) /\ (undef34 = undef34), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef33, oldX3^0 -> undef34, x0^0 -> (0 + undef33), x1^0 -> (0 + undef34)}>
<l6, l4, (undef37 = (0 + x0^0)) /\ (undef38 = (0 + x1^0)), par{oldX0^0 -> undef37, oldX1^0 -> undef38, x0^0 -> (~(1) + undef37), x1^0 -> (1 + undef38)}>
<l7, l5, (undef43 = (0 + x0^0)) /\ (undef44 = (0 + x1^0)) /\ ((0 + undef43) <= 0), par{oldX0^0 -> undef43, oldX1^0 -> undef44, x0^0 -> (0 + undef43), x1^0 -> (0 + undef44)}>
<l7, l6, (undef49 = (0 + x0^0)) /\ (undef50 = (0 + x1^0)) /\ (1 <= (0 + undef49)), par{oldX0^0 -> undef49, oldX1^0 -> undef50, x0^0 -> (0 + undef49), x1^0 -> (0 + undef50)}>
<l4, l7, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)), par{oldX0^0 -> undef55, oldX1^0 -> undef56, x0^0 -> (0 + undef55), x1^0 -> (0 + undef56)}>
<l8, l1, true>
<l8, l3, true>
<l8, l2, true>
<l8, l5, true>
<l8, l6, true>
<l8, l7, true>
<l8, l4, true>
<l9, l8, true>

Fresh variables:
undef3, undef4, undef9, undef10, undef13, undef14, undef19, undef20, undef25, undef26, undef33, undef34, undef37, undef38, undef43, undef44, undef49, undef50, undef55, undef56, 

Undef variables:
undef3, undef4, undef9, undef10, undef13, undef14, undef19, undef20, undef25, undef26, undef33, undef34, undef37, undef38, undef43, undef44, undef49, undef50, undef55, undef56, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (undef3 = undef3) /\ (undef4 = undef4), par{x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}>
<l0, l2, (undef9 = undef9) /\ (undef10 = undef10), par{x0^0 -> (0 + undef9), x1^0 -> (0 + undef10)}>
<l0, l4, (undef13 = (0 + x0^0)) /\ (undef14 = (0 + x1^0)), par{x0^0 -> (1 + undef13), x1^0 -> (~(2) + undef14)}>
<l0, l2, true>
<l0, l2, (undef19 = (0 + x0^0)) /\ (undef20 = (0 + x1^0)) /\ ((0 + undef20) <= 2) /\ (undef3 = undef3) /\ (undef4 = undef4), par{x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}>
<l0, l2, (undef25 = (0 + x0^0)) /\ (undef26 = (0 + x1^0)) /\ (3 <= (0 + undef26)) /\ (undef9 = undef9) /\ (undef10 = undef10), par{x0^0 -> (0 + undef9), x1^0 -> (0 + undef10)}>
<l0, l4, (undef25 = (0 + x0^0)) /\ (undef26 = (0 + x1^0)) /\ (3 <= (0 + undef26)) /\ (undef13 = (0 + (0 + undef25))) /\ (undef14 = (0 + (0 + undef26))), par{x0^0 -> (1 + undef13), x1^0 -> (~(2) + undef14)}>
<l0, l2, (undef33 = undef33) /\ (undef34 = undef34), par{x0^0 -> (0 + undef33), x1^0 -> (0 + undef34)}>
<l0, l4, (undef37 = (0 + x0^0)) /\ (undef38 = (0 + x1^0)), par{x0^0 -> (~(1) + undef37), x1^0 -> (1 + undef38)}>
<l0, l2, (undef43 = (0 + x0^0)) /\ (undef44 = (0 + x1^0)) /\ ((0 + undef43) <= 0) /\ (undef19 = (0 + (0 + undef43))) /\ (undef20 = (0 + (0 + undef44))) /\ ((0 + undef20) <= 2) /\ (undef3 = undef3) /\ (undef4 = undef4), par{x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}>
<l0, l2, (undef43 = (0 + x0^0)) /\ (undef44 = (0 + x1^0)) /\ ((0 + undef43) <= 0) /\ (undef25 = (0 + (0 + undef43))) /\ (undef26 = (0 + (0 + undef44))) /\ (3 <= (0 + undef26)) /\ (undef9 = undef9) /\ (undef10 = undef10), par{x0^0 -> (0 + undef9), x1^0 -> (0 + undef10)}>
<l0, l4, (undef43 = (0 + x0^0)) /\ (undef44 = (0 + x1^0)) /\ ((0 + undef43) <= 0) /\ (undef25 = (0 + (0 + undef43))) /\ (undef26 = (0 + (0 + undef44))) /\ (3 <= (0 + undef26)) /\ (undef13 = (0 + (0 + undef25))) /\ (undef14 = (0 + (0 + undef26))), par{x0^0 -> (1 + undef13), x1^0 -> (~(2) + undef14)}>
<l0, l2, (undef49 = (0 + x0^0)) /\ (undef50 = (0 + x1^0)) /\ (1 <= (0 + undef49)) /\ (undef33 = undef33) /\ (undef34 = undef34), par{x0^0 -> (0 + undef33), x1^0 -> (0 + undef34)}>
<l0, l4, (undef49 = (0 + x0^0)) /\ (undef50 = (0 + x1^0)) /\ (1 <= (0 + undef49)) /\ (undef37 = (0 + (0 + undef49))) /\ (undef38 = (0 + (0 + undef50))), par{x0^0 -> (~(1) + undef37), x1^0 -> (1 + undef38)}>
<l0, l4, true>
<l4, l2, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)) /\ (undef43 = (0 + (0 + undef55))) /\ (undef44 = (0 + (0 + undef56))) /\ ((0 + undef43) <= 0) /\ (undef19 = (0 + (0 + undef43))) /\ (undef20 = (0 + (0 + undef44))) /\ ((0 + undef20) <= 2) /\ (undef3 = undef3) /\ (undef4 = undef4), par{x0^0 -> (0 + undef3), x1^0 -> (0 + undef4)}>
<l4, l2, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)) /\ (undef43 = (0 + (0 + undef55))) /\ (undef44 = (0 + (0 + undef56))) /\ ((0 + undef43) <= 0) /\ (undef25 = (0 + (0 + undef43))) /\ (undef26 = (0 + (0 + undef44))) /\ (3 <= (0 + undef26)) /\ (undef9 = undef9) /\ (undef10 = undef10), par{x0^0 -> (0 + undef9), x1^0 -> (0 + undef10)}>
<l4, l4, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)) /\ (undef43 = (0 + (0 + undef55))) /\ (undef44 = (0 + (0 + undef56))) /\ ((0 + undef43) <= 0) /\ (undef25 = (0 + (0 + undef43))) /\ (undef26 = (0 + (0 + undef44))) /\ (3 <= (0 + undef26)) /\ (undef13 = (0 + (0 + undef25))) /\ (undef14 = (0 + (0 + undef26))), par{x0^0 -> (1 + undef13), x1^0 -> (~(2) + undef14)}>
<l4, l2, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)) /\ (undef49 = (0 + (0 + undef55))) /\ (undef50 = (0 + (0 + undef56))) /\ (1 <= (0 + undef49)) /\ (undef33 = undef33) /\ (undef34 = undef34), par{x0^0 -> (0 + undef33), x1^0 -> (0 + undef34)}>
<l4, l4, (undef55 = (0 + x0^0)) /\ (undef56 = (0 + x1^0)) /\ (undef49 = (0 + (0 + undef55))) /\ (undef50 = (0 + (0 + undef56))) /\ (1 <= (0 + undef49)) /\ (undef37 = (0 + (0 + undef49))) /\ (undef38 = (0 + (0 + undef50))), par{x0^0 -> (~(1) + undef37), x1^0 -> (1 + undef38)}>

Fresh variables:
undef3, undef4, undef9, undef10, undef13, undef14, undef19, undef20, undef25, undef26, undef33, undef34, undef37, undef38, undef43, undef44, undef49, undef50, undef55, undef56, 

Undef variables:
undef3, undef4, undef9, undef10, undef13, undef14, undef19, undef20, undef25, undef26, undef33, undef34, undef37, undef38, undef43, undef44, undef49, undef50, undef55, undef56, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
<l4, l4, 1 <= undef49 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
Variables:
x0^0, x1^0

Graph 2:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l4, x0^0 = undef13 /\ x1^0 = undef14, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
<l0, l4, 3 <= undef26 /\ x0^0 = undef25 /\ x1^0 = undef26 /\ undef13 = undef25 /\ undef14 = undef26, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
<l0, l4, x0^0 = undef37 /\ x1^0 = undef38, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
<l0, l4, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef43 /\ x1^0 = undef44 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
<l0, l4, 1 <= undef49 /\ x0^0 = undef49 /\ x1^0 = undef50 /\ undef37 = undef49 /\ undef38 = undef50, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
<l0, l4, true, {all remain the same}>

Graph 2
<l0, l2, true, {x0^0 -> undef3, x1^0 -> undef4, rest remain the same}>
<l0, l2, true, {x0^0 -> undef9, x1^0 -> undef10, rest remain the same}>
<l0, l2, true, {all remain the same}>
<l0, l2, undef20 <= 2 /\ x0^0 = undef19 /\ x1^0 = undef20, {x0^0 -> undef3, x1^0 -> undef4, rest remain the same}>
<l0, l2, 3 <= undef26 /\ x0^0 = undef25 /\ x1^0 = undef26, {x0^0 -> undef9, x1^0 -> undef10, rest remain the same}>
<l0, l2, true, {x0^0 -> undef33, x1^0 -> undef34, rest remain the same}>
<l0, l2, undef43 <= 0 /\ undef20 <= 2 /\ x0^0 = undef43 /\ x1^0 = undef44 /\ undef19 = undef43 /\ undef20 = undef44, {x0^0 -> undef3, x1^0 -> undef4, rest remain the same}>
<l0, l2, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef43 /\ x1^0 = undef44 /\ undef25 = undef43 /\ undef26 = undef44, {x0^0 -> undef9, x1^0 -> undef10, rest remain the same}>
<l0, l2, 1 <= undef49 /\ x0^0 = undef49 /\ x1^0 = undef50, {x0^0 -> undef33, x1^0 -> undef34, rest remain the same}>
<l4, l2, undef43 <= 0 /\ undef20 <= 2 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef19 = undef43 /\ undef20 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> undef3, x1^0 -> undef4, rest remain the same}>
<l4, l2, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> undef9, x1^0 -> undef10, rest remain the same}>
<l4, l2, 1 <= undef49 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> undef33, x1^0 -> undef34, rest remain the same}>

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

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

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

Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001071s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010116s
Trying to remove transition: <l4, l4, 1 <= undef49 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017937s
Time used: 0.017346
Trying to remove transition: <l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.026795s
Time used: 0.026793

LOG: SAT solveNonLinear - Elapsed time: 0.044722s
Cost: 4; Total time: 0.043912
Failed at location 4: 1 <= x1^0
Failed at location 4: 1 <= x1^0
Failed at location 4: 1 <= x1^0
Failed at location 4: 1 <= x1^0
Before Improving: 
Quasi-invariant at l4: 1 <= x1^0
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solveLinear

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

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ 0 <= 300 + x1^0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 <= undef49 /\ 0 <= 300 + x1^0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ 0 <= 300 + x1^0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l4, l4, 1 <= undef49 /\ 0 <= 300 + x1^0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
Ranking function: 596 + 4*x0^0 + 2*x1^0
New Graphs: 
Transitions:
<l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ 0 <= 300 + x1^0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
Variables:
x0^0, x1^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000863s
Ranking function: -x0^0
New Graphs: 
Calling Safety with literal 0 <= 300 + x1^0 and entry <l0, l4, x0^0 = undef13 /\ x1^0 = undef14, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>

LOG: CALL check - Post:0 <= 300 + x1^0 - Process 1
* Exit transition: <l0, l4, x0^0 = undef13 /\ x1^0 = undef14, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
* Postcondition  : 0 <= 300 + x1^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000467s
Calling Safety with literal 0 <= 300 + x1^0 and entry <l0, l4, x0^0 = undef37 /\ x1^0 = undef38, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>

LOG: CALL check - Post:0 <= 300 + x1^0 - Process 2
* Exit transition: <l0, l4, x0^0 = undef37 /\ x1^0 = undef38, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
* Postcondition  : 0 <= 300 + x1^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000454s
Calling Safety with literal 0 <= 300 + x1^0 and entry <l0, l4, 1 <= undef49 /\ x0^0 = undef49 /\ x1^0 = undef50 /\ undef37 = undef49 /\ undef38 = undef50, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>

LOG: CALL check - Post:0 <= 300 + x1^0 - Process 3
* Exit transition: <l0, l4, 1 <= undef49 /\ x0^0 = undef49 /\ x1^0 = undef50 /\ undef37 = undef49 /\ undef38 = undef50, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
* Postcondition  : 0 <= 300 + x1^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000531s
Calling Safety with literal 0 <= 300 + x1^0 and entry <l0, l4, true, {all remain the same}>

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

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000351s
INVARIANTS: 
4: 
Quasi-INVARIANTS to narrow Graph: 
4: 0 <= 300 + x1^0 , 
It's unfeasible. Removing transition: 
<l4, l4, undef43 <= 0 /\ 3 <= undef26 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef13 = undef25 /\ undef14 = undef26 /\ undef25 = undef43 /\ undef26 = undef44 /\ undef43 = undef55 /\ undef44 = undef56, {x0^0 -> 1 + undef13, x1^0 -> -2 + undef14, rest remain the same}>
Narrowing transition: 
<l4, l4, 1 <= undef49 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l4, l4, 1 <= undef49 /\ 301 + x1^0 <= 0 /\ x0^0 = undef55 /\ x1^0 = undef56 /\ undef37 = undef49 /\ undef38 = undef50 /\ undef49 = undef55 /\ undef50 = undef56, {x0^0 -> -1 + undef37, x1^0 -> 1 + undef38, rest remain the same}>
Variables:
x0^0, x1^0
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000776s
Ranking function: -1 + x0^0
New Graphs: 
Proving termination of subgraph 2
Analyzing SCC {l2}...
No cycles found.

Program Terminates