Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb8in : A'=B, B'=A, [], cost: 1
      2: evalfbb8in -> evalfbb2in : C'=A, [ B>=0 ], cost: 1
      3: evalfbb8in -> evalfreturnin : [ 0>=1+B ], cost: 1
      4: evalfbb2in -> evalfbb4in : [ 0>=1+C ], cost: 1
      5: evalfbb2in -> evalfbb3in : [ C>=0 ], cost: 1
     17: evalfreturnin -> evalfstop : [], cost: 1
     10: evalfbb4in -> evalfbb6in : D'=-1+B, E'=C, [], cost: 1
      8: evalfbb3in -> evalfbb4in : [], cost: 1
      6: evalfbb3in -> evalfbb1in : [ 0>=1+free ], cost: 1
      7: evalfbb3in -> evalfbb1in : [ free_1>=1 ], cost: 1
      9: evalfbb1in -> evalfbb2in : C'=-1+C, [], cost: 1
     11: evalfbb6in -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     12: evalfbb6in -> evalfbb7in : [ F>=E ], cost: 1
     15: evalfbb7in -> evalfbb8in : A'=E, B'=D, [], cost: 1
     13: evalfbb7in -> evalfbb5in : [ 0>=1+free_2 ], cost: 1
     14: evalfbb7in -> evalfbb5in : [ free_3>=1 ], cost: 1
     16: evalfbb5in -> evalfbb6in : E'=1+E, [], cost: 1

Removing duplicate transition: 6.
Removing duplicate transition: 13.

Simplified the transitions:
  Start location: evalfstart
      0: evalfstart -> evalfentryin : [], cost: 1
      1: evalfentryin -> evalfbb8in : A'=B, B'=A, [], cost: 1
      2: evalfbb8in -> evalfbb2in : C'=A, [ B>=0 ], cost: 1
      4: evalfbb2in -> evalfbb4in : [ 0>=1+C ], cost: 1
      5: evalfbb2in -> evalfbb3in : [ C>=0 ], cost: 1
     10: evalfbb4in -> evalfbb6in : D'=-1+B, E'=C, [], cost: 1
      8: evalfbb3in -> evalfbb4in : [], cost: 1
      7: evalfbb3in -> evalfbb1in : [], cost: 1
      9: evalfbb1in -> evalfbb2in : C'=-1+C, [], cost: 1
     11: evalfbb6in -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     12: evalfbb6in -> evalfbb7in : [ F>=E ], cost: 1
     15: evalfbb7in -> evalfbb8in : A'=E, B'=D, [], cost: 1
     14: evalfbb7in -> evalfbb5in : [], cost: 1
     16: evalfbb5in -> evalfbb6in : E'=1+E, [], cost: 1


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
      2: evalfbb8in -> evalfbb2in : C'=A, [ B>=0 ], cost: 1
      4: evalfbb2in -> evalfbb4in : [ 0>=1+C ], cost: 1
      5: evalfbb2in -> evalfbb3in : [ C>=0 ], cost: 1
     10: evalfbb4in -> evalfbb6in : D'=-1+B, E'=C, [], cost: 1
      7: evalfbb3in -> evalfbb2in : C'=-1+C, [], cost: 2
      8: evalfbb3in -> evalfbb4in : [], cost: 1
     11: evalfbb6in -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     12: evalfbb6in -> evalfbb7in : [ F>=E ], cost: 1
     15: evalfbb7in -> evalfbb8in : A'=E, B'=D, [], cost: 1
     14: evalfbb7in -> evalfbb6in : E'=1+E, [], cost: 2


Applied chaining over branches and pruning:
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
      2: evalfbb8in -> evalfbb2in : C'=A, [ B>=0 ], cost: 1
     18: evalfbb2in -> evalfbb2in : C'=-1+C, [ C>=0 ], cost: 3
      4: evalfbb2in -> evalfbb4in : [ 0>=1+C ], cost: 1
     19: evalfbb2in -> evalfbb4in : [ C>=0 ], cost: 2
     10: evalfbb4in -> evalfbb6in : D'=-1+B, E'=C, [], cost: 1
     11: evalfbb6in -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     20: evalfbb6in -> evalfbb8in : A'=E, B'=D, [ F>=E ], cost: 2
     21: evalfbb6in -> evalfbb6in : E'=1+E, [ F>=E ], cost: 3

Eliminating 1 self-loops for location evalfbb2in
  Self-Loop 18 has the metering function: 1+C, resulting in the new transition 22.
  Removing the self-loops: 18.
Eliminating 1 self-loops for location evalfbb6in
  Self-Loop 21 has the metering function: 1-E+F, resulting in the new transition 23.
  Removing the self-loops: 21.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
      2: evalfbb8in -> evalfbb2in : C'=A, [ B>=0 ], cost: 1
     22: evalfbb2in -> [12] : C'=-1, [ C>=0 ], cost: 3+3*C
     10: evalfbb4in -> evalfbb6in : D'=-1+B, E'=C, [], cost: 1
     23: evalfbb6in -> [13] : E'=1+F, [ F>=E ], cost: 3-3*E+3*F
      4: [12] -> evalfbb4in : [ 0>=1+C ], cost: 1
     19: [12] -> evalfbb4in : [ C>=0 ], cost: 2
     11: [13] -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     20: [13] -> evalfbb8in : A'=E, B'=D, [ F>=E ], cost: 2


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
      2: evalfbb8in -> [12] : C'=-1, [ B>=0 && A>=0 ], cost: 4+3*A
     10: evalfbb4in -> [13] : D'=-1+B, E'=1+F, [ F>=C ], cost: 4+3*F-3*C
      4: [12] -> evalfbb4in : [ 0>=1+C ], cost: 1
     19: [12] -> evalfbb4in : [ C>=0 ], cost: 2
     11: [13] -> evalfbb8in : A'=E, B'=D, [ E>=1+F ], cost: 1
     20: [13] -> evalfbb8in : A'=E, B'=D, [ F>=E ], cost: 2


Applied chaining over branches and pruning:
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
     24: evalfbb8in -> evalfbb4in : C'=-1, [ B>=0 && A>=0 && 0>=0 ], cost: 5+3*A
     25: evalfbb8in -> [14] : C'=-1, [ B>=0 && A>=0 ], cost: 4+3*A
     26: evalfbb4in -> evalfbb8in : A'=1+F, B'=-1+B, D'=-1+B, E'=1+F, [ F>=C && 1+F>=1+F ], cost: 5+3*F-3*C
     27: evalfbb4in -> [15] : D'=-1+B, E'=1+F, [ F>=C ], cost: 4+3*F-3*C


Applied chaining over branches and pruning:
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
     28: evalfbb8in -> evalfbb8in : A'=1+F, B'=-1+B, C'=-1, D'=-1+B, E'=1+F, [ B>=0 && A>=0 && 0>=0 && F>=-1 && 1+F>=1+F ], cost: 13+3*F+3*A
     25: evalfbb8in -> [14] : C'=-1, [ B>=0 && A>=0 ], cost: 4+3*A
     29: evalfbb8in -> [15] : C'=-1, D'=-1+B, E'=1+F, [ B>=0 && A>=0 && 0>=0 && F>=-1 ], cost: 12+3*F+3*A

Eliminating 1 self-loops for location evalfbb8in
  Self-Loop 28 has the metering function: 1+B, resulting in the new transition 30.
  Removing the self-loops: 28.

Removed all Self-loops using metering functions (where possible):
  Start location: evalfstart
      0: evalfstart -> evalfbb8in : A'=B, B'=A, [], cost: 2
     30: evalfbb8in -> [16] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ B>=0 && A>=0 && F>=-1 ], cost: 16+16*B+6*(1+B)*F
     25: [16] -> [14] : C'=-1, [ B>=0 && A>=0 ], cost: 4+3*A
     29: [16] -> [15] : C'=-1, D'=-1+B, E'=1+F, [ B>=0 && A>=0 && 0>=0 && F>=-1 ], cost: 12+3*F+3*A


Applied simple chaining:
  Start location: evalfstart
      0: evalfstart -> [16] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ A>=0 && B>=0 && F>=-1 ], cost: 18+6*(1+A)*F+16*A
     25: [16] -> [14] : C'=-1, [ B>=0 && A>=0 ], cost: 4+3*A
     29: [16] -> [15] : C'=-1, D'=-1+B, E'=1+F, [ B>=0 && A>=0 && 0>=0 && F>=-1 ], cost: 12+3*F+3*A


Applied chaining over branches and pruning:
  Start location: evalfstart
     31: evalfstart -> [17] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ A>=0 && B>=0 && F>=-1 ], cost: 18+6*(1+A)*F+16*A
     32: evalfstart -> [18] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ A>=0 && B>=0 && F>=-1 ], cost: 18+6*(1+A)*F+16*A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalfstart
     31: evalfstart -> [17] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ A>=0 && B>=0 && F>=-1 ], cost: 18+6*(1+A)*F+16*A
     32: evalfstart -> [18] : A'=1+F, B'=-1, C'=-1, D'=-1, E'=1+F, [ A>=0 && B>=0 && F>=-1 ], cost: 18+6*(1+A)*F+16*A


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 18+6*(1+A)*F+16*A
  and guard: A>=0 && B>=0 && F>=-1:
  B: Pos, F: Pos, A: Pos

Found new complexity n^2, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: A>=0 && B>=0 && F>=-1
  Final Cost:  18+6*(1+A)*F+16*A

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

WORST_CASE(Omega(n^2),?)