Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalrealshellsortstart
      0: evalrealshellsortstart -> evalrealshellsortentryin : [], cost: 1
      1: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 1
      2: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 1
      3: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 1
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
      5: evalrealshellsortbb8in -> evalrealshellsortreturnin : [ 0>=B ], cost: 1
      6: evalrealshellsortbb6in -> evalrealshellsortbb1in : [ A>=1+C ], cost: 1
      7: evalrealshellsortbb6in -> evalrealshellsortbb7in : [ C>=A ], cost: 1
     18: evalrealshellsortreturnin -> evalrealshellsortstop : [], cost: 1
      8: evalrealshellsortbb1in -> evalrealshellsortbb3in : D'=free_2, E'=C, [], cost: 1
     15: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=0, [ B==0 ], cost: 1
     16: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_5, [ B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 1
     17: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_6, [ 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 1
      9: evalrealshellsortbb3in -> evalrealshellsortbb5in : [ B>=1+E ], cost: 1
     10: evalrealshellsortbb3in -> evalrealshellsortbb4in : [ E>=B ], cost: 1
     14: evalrealshellsortbb5in -> evalrealshellsortbb6in : C'=1+C, [], cost: 1
     12: evalrealshellsortbb4in -> evalrealshellsortbb5in : [ D>=free_4 ], cost: 1
     11: evalrealshellsortbb4in -> evalrealshellsortbb2in : [ free_3>=1+D ], cost: 1
     13: evalrealshellsortbb2in -> evalrealshellsortbb3in : E'=E-B, [], cost: 1


Simplified the transitions:
  Start location: evalrealshellsortstart
      0: evalrealshellsortstart -> evalrealshellsortentryin : [], cost: 1
      1: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 1
      2: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 1
      3: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 1
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
      6: evalrealshellsortbb6in -> evalrealshellsortbb1in : [ A>=1+C ], cost: 1
      7: evalrealshellsortbb6in -> evalrealshellsortbb7in : [ C>=A ], cost: 1
      8: evalrealshellsortbb1in -> evalrealshellsortbb3in : D'=free_2, E'=C, [], cost: 1
     15: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=0, [ B==0 ], cost: 1
     16: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_5, [ B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 1
     17: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_6, [ 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 1
      9: evalrealshellsortbb3in -> evalrealshellsortbb5in : [ B>=1+E ], cost: 1
     10: evalrealshellsortbb3in -> evalrealshellsortbb4in : [ E>=B ], cost: 1
     14: evalrealshellsortbb5in -> evalrealshellsortbb6in : C'=1+C, [], cost: 1
     12: evalrealshellsortbb4in -> evalrealshellsortbb5in : [], cost: 1
     11: evalrealshellsortbb4in -> evalrealshellsortbb2in : [], cost: 1
     13: evalrealshellsortbb2in -> evalrealshellsortbb3in : E'=E-B, [], cost: 1


Applied simple chaining:
  Start location: evalrealshellsortstart
      0: evalrealshellsortstart -> evalrealshellsortentryin : [], cost: 1
      1: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 1
      2: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 1
      3: evalrealshellsortentryin -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 1
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
      7: evalrealshellsortbb6in -> evalrealshellsortbb7in : [ C>=A ], cost: 1
      6: evalrealshellsortbb6in -> evalrealshellsortbb3in : D'=free_2, E'=C, [ A>=1+C ], cost: 2
     15: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=0, [ B==0 ], cost: 1
     16: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_5, [ B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 1
     17: evalrealshellsortbb7in -> evalrealshellsortbb8in : B'=free_6, [ 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 1
      9: evalrealshellsortbb3in -> evalrealshellsortbb5in : [ B>=1+E ], cost: 1
     10: evalrealshellsortbb3in -> evalrealshellsortbb4in : [ E>=B ], cost: 1
     14: evalrealshellsortbb5in -> evalrealshellsortbb6in : C'=1+C, [], cost: 1
     11: evalrealshellsortbb4in -> evalrealshellsortbb3in : E'=E-B, [], cost: 2
     12: evalrealshellsortbb4in -> evalrealshellsortbb5in : [], cost: 1


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
     22: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2
      6: evalrealshellsortbb6in -> evalrealshellsortbb3in : D'=free_2, E'=C, [ A>=1+C ], cost: 2
     25: evalrealshellsortbb3in -> evalrealshellsortbb3in : E'=E-B, [ E>=B ], cost: 3
      9: evalrealshellsortbb3in -> evalrealshellsortbb5in : [ B>=1+E ], cost: 1
     26: evalrealshellsortbb3in -> evalrealshellsortbb5in : [ E>=B ], cost: 2
     14: evalrealshellsortbb5in -> evalrealshellsortbb6in : C'=1+C, [], cost: 1

Eliminating 1 self-loops for location evalrealshellsortbb3in
  Removing the self-loops: 25.
Adding an epsilon transition (to model nonexecution of the loops): 28.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
     22: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2
      6: evalrealshellsortbb6in -> evalrealshellsortbb3in : D'=free_2, E'=C, [ A>=1+C ], cost: 2
     27: evalrealshellsortbb3in -> [12] : E'=E-B, [ E>=B ], cost: 3
     28: evalrealshellsortbb3in -> [12] : [], cost: 0
     14: evalrealshellsortbb5in -> evalrealshellsortbb6in : C'=1+C, [], cost: 1
      9: [12] -> evalrealshellsortbb5in : [ B>=1+E ], cost: 1
     26: [12] -> evalrealshellsortbb5in : [ E>=B ], cost: 2


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
     22: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2
     29: evalrealshellsortbb6in -> [12] : D'=free_2, E'=-B+C, [ A>=1+C && C>=B ], cost: 5
     30: evalrealshellsortbb6in -> [12] : D'=free_2, E'=C, [ A>=1+C ], cost: 2
     31: [12] -> evalrealshellsortbb6in : C'=1+C, [ B>=1+E ], cost: 2
     32: [12] -> evalrealshellsortbb6in : C'=1+C, [ E>=B ], cost: 3


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
     22: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: evalrealshellsortbb6in -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2
     33: evalrealshellsortbb6in -> evalrealshellsortbb6in : C'=1+C, D'=free_2, E'=-B+C, [ A>=1+C && C>=B && B>=1-B+C ], cost: 7
     34: evalrealshellsortbb6in -> evalrealshellsortbb6in : C'=1+C, D'=free_2, E'=-B+C, [ A>=1+C && C>=B && -B+C>=B ], cost: 8
     35: evalrealshellsortbb6in -> evalrealshellsortbb6in : C'=1+C, D'=free_2, E'=C, [ A>=1+C && B>=1+C ], cost: 4
     36: evalrealshellsortbb6in -> evalrealshellsortbb6in : C'=1+C, D'=free_2, E'=C, [ A>=1+C && C>=B ], cost: 5

Eliminating 4 self-loops for location evalrealshellsortbb6in
  Self-Loop 34 has the metering function: -C+A, resulting in the new transition 38.
  Self-Loop 36 has the metering function: -C+A, resulting in the new transition 40.
  Removing the self-loops: 33 34 35 36.
Adding an epsilon transition (to model nonexecution of the loops): 41.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
      4: evalrealshellsortbb8in -> evalrealshellsortbb6in : C'=0, [ B>=1 ], cost: 1
     37: evalrealshellsortbb6in -> [13] : C'=1+C, D'=free_2, E'=-B+C, [ A>=1+C && C>=B && B>=1-B+C ], cost: 7
     38: evalrealshellsortbb6in -> [13] : C'=A, D'=free_2, E'=-1-B+A, [ A>=1+C && C>=B && -B+C>=B ], cost: -8*C+8*A
     39: evalrealshellsortbb6in -> [13] : C'=1+C, D'=free_2, E'=C, [ A>=1+C && B>=1+C ], cost: 4
     40: evalrealshellsortbb6in -> [13] : C'=A, D'=free_2, E'=-1+A, [ A>=1+C && C>=B ], cost: -5*C+5*A
     41: evalrealshellsortbb6in -> [13] : [], cost: 0
     22: [13] -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: [13] -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: [13] -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
     42: evalrealshellsortbb8in -> [13] : C'=1, D'=free_2, E'=0, [ B>=1 && A>=1 && B>=1 ], cost: 5
     43: evalrealshellsortbb8in -> [13] : C'=0, [ B>=1 ], cost: 1
     22: [13] -> evalrealshellsortbb8in : B'=0, [ C>=A && B==0 ], cost: 2
     23: [13] -> evalrealshellsortbb8in : B'=free_5, [ C>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 2
     24: [13] -> evalrealshellsortbb8in : B'=free_6, [ C>=A && 0>=1+B && 0>=free_6 && 2*free_6>=B && 1+B>=2*free_6 ], cost: 2


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
     44: evalrealshellsortbb8in -> evalrealshellsortbb8in : B'=free_5, C'=1, D'=free_2, E'=0, [ B>=1 && A>=1 && B>=1 && 1>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 7
     45: evalrealshellsortbb8in -> evalrealshellsortbb8in : B'=free_5, C'=0, [ B>=1 && 0>=A && B>=1 && free_5>=0 && B>=2*free_5 && 1+2*free_5>=B ], cost: 3

Eliminating 2 self-loops for location evalrealshellsortbb8in
  Self-Loop 44 has the metering function: B, resulting in the new transition 46.
  Self-Loop 45 has the metering function: B, resulting in the new transition 47.
  Removing the self-loops: 44 45.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealshellsortstart
     19: evalrealshellsortstart -> evalrealshellsortbb8in : B'=0, [ A==0 ], cost: 2
     20: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free, [ A>=1 && free>=0 && A>=2*free && 1+2*free>=A ], cost: 2
     21: evalrealshellsortstart -> evalrealshellsortbb8in : B'=free_1, [ 0>=1+A && 0>=free_1 && 2*free_1>=A && 1+A>=2*free_1 ], cost: 2
     46: evalrealshellsortbb8in -> [14] : B'=0, C'=1, D'=free_2, E'=0, [ B>=1 && 1-A==0 && 0>=0 && B>=0 && 1>=B ], cost: 7*B
     47: evalrealshellsortbb8in -> [14] : B'=0, C'=0, [ B>=1 && 0>=A && 0>=0 && B>=0 && 1>=B ], cost: 3*B


Applied chaining over branches and pruning:
  Start location: evalrealshellsortstart
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalrealshellsortstart
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: const
  Complexity value: 0

WORST_CASE(Omega(1),?)