Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f10 : A'=free, B'=0, [], cost: 1
      1: f10 -> f10 : B'=1+B, [ C>=1+B ], cost: 1
      9: f10 -> f18 : D'=C, E'=0, [ B>=C ], cost: 1
      2: f18 -> f21 : F'=0, [ D>=2+E ], cost: 1
      8: f18 -> f32 : E'=0, [ 1+E>=D ], cost: 1
      7: f21 -> f18 : E'=1+E, [ 1+E+F>=D ], cost: 1
      3: f21 -> f21 : F'=1+F, [ D>=2+E+F ], cost: 1
      4: f21 -> f21 : F'=1+F, G'=free_1, [ D>=2+E+F ], cost: 1
      5: f32 -> f32 : E'=1+E, [ D>=2+E ], cost: 1
      6: f32 -> f41 : [ 1+E>=D ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f10 : A'=free, B'=0, [], cost: 1
      1: f10 -> f10 : B'=1+B, [ C>=1+B ], cost: 1
      9: f10 -> f18 : D'=C, E'=0, [ B>=C ], cost: 1
      2: f18 -> f21 : F'=0, [ D>=2+E ], cost: 1
      8: f18 -> f32 : E'=0, [ 1+E>=D ], cost: 1
      7: f21 -> f18 : E'=1+E, [ 1+E+F>=D ], cost: 1
      3: f21 -> f21 : F'=1+F, [ D>=2+E+F ], cost: 1
      4: f21 -> f21 : F'=1+F, G'=free_1, [ D>=2+E+F ], cost: 1
      5: f32 -> f32 : E'=1+E, [ D>=2+E ], cost: 1

Eliminating 1 self-loops for location f10
  Self-Loop 1 has the metering function: -B+C, resulting in the new transition 10.
  Removing the self-loops: 1.
Eliminating 2 self-loops for location f21
  Self-Loop 3 has the metering function: -1-E-F+D, resulting in the new transition 11.
  Self-Loop 4 has the metering function: -1-E-F+D, resulting in the new transition 12.
  Removing the self-loops: 3 4.
Eliminating 1 self-loops for location f32
  Self-Loop 5 has the metering function: -1-E+D, resulting in the new transition 13.
  Removing the self-loops: 5.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f10 : A'=free, B'=0, [], cost: 1
     10: f10 -> [6] : B'=C, [ C>=1+B ], cost: -B+C
      2: f18 -> f21 : F'=0, [ D>=2+E ], cost: 1
      8: f18 -> f32 : E'=0, [ 1+E>=D ], cost: 1
     11: f21 -> [7] : F'=-1-E+D, [ D>=2+E+F ], cost: -1-E-F+D
     12: f21 -> [7] : F'=-1-E+D, G'=free_1, [ D>=2+E+F ], cost: -1-E-F+D
     13: f32 -> [8] : E'=-1+D, [ D>=2+E ], cost: -1-E+D
      9: [6] -> f18 : D'=C, E'=0, [ B>=C ], cost: 1
      7: [7] -> f18 : E'=1+E, [ 1+E+F>=D ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f18 : A'=free, B'=C, D'=C, E'=0, [ C>=1 && C>=C ], cost: 2+C
      2: f18 -> f21 : F'=0, [ D>=2+E ], cost: 1
      8: f18 -> [8] : E'=-1+D, [ 1+E>=D && D>=2 ], cost: D
     11: f21 -> [7] : F'=-1-E+D, [ D>=2+E+F ], cost: -1-E-F+D
     12: f21 -> [7] : F'=-1-E+D, G'=free_1, [ D>=2+E+F ], cost: -1-E-F+D
      7: [7] -> f18 : E'=1+E, [ 1+E+F>=D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f18 : A'=free, B'=C, D'=C, E'=0, [ C>=1 && C>=C ], cost: 2+C
     14: f18 -> [7] : F'=-1-E+D, [ D>=2+E && D>=2+E ], cost: -E+D
     15: f18 -> [7] : F'=-1-E+D, G'=free_1, [ D>=2+E && D>=2+E ], cost: -E+D
      8: f18 -> [8] : E'=-1+D, [ 1+E>=D && D>=2 ], cost: D
      7: [7] -> f18 : E'=1+E, [ 1+E+F>=D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f18 : A'=free, B'=C, D'=C, E'=0, [ C>=1 && C>=C ], cost: 2+C
     16: f18 -> f18 : E'=1+E, F'=-1-E+D, [ D>=2+E && D>=2+E && D>=D ], cost: 1-E+D
     17: f18 -> f18 : E'=1+E, F'=-1-E+D, G'=free_1, [ D>=2+E && D>=2+E && D>=D ], cost: 1-E+D
      8: f18 -> [8] : E'=-1+D, [ 1+E>=D && D>=2 ], cost: D

Eliminating 2 self-loops for location f18
  Self-Loop 16 has the metering function: -1-E+D, resulting in the new transition 18.
  Self-Loop 17 has the metering function: -1-E+D, resulting in the new transition 19.
  Removing the self-loops: 16 17.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f18 : A'=free, B'=C, D'=C, E'=0, [ C>=1 && C>=C ], cost: 2+C
     18: f18 -> [9] : E'=-1+D, F'=1, [ D>=2+E ], cost: -3/2-3/2*E-(1+E-D)*D-1/2*(1+E-D)^2+E*(1+E-D)+3/2*D
     19: f18 -> [9] : E'=-1+D, F'=1, G'=free_1, [ D>=2+E ], cost: -3/2-3/2*E-(1+E-D)*D-1/2*(1+E-D)^2+E*(1+E-D)+3/2*D
      8: [9] -> [8] : E'=-1+D, [ 1+E>=D && D>=2 ], cost: D


Applied chaining over branches and pruning:
  Start location: f0
     20: f0 -> [9] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, [ C>=1 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+5/2*C
     21: f0 -> [9] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, G'=free_1, [ C>=1 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+5/2*C
      8: [9] -> [8] : E'=-1+D, [ 1+E>=D && D>=2 ], cost: D


Applied chaining over branches and pruning:
  Start location: f0
     22: f0 -> [8] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, [ C>=1 && C>=C && C>=2 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C
     23: f0 -> [8] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, G'=free_1, [ C>=1 && C>=C && C>=2 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     22: f0 -> [8] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, [ C>=1 && C>=C && C>=2 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C
     23: f0 -> [8] : A'=free, B'=C, D'=C, E'=-1+C, F'=1, G'=free_1, [ C>=1 && C>=C && C>=2 && C>=C && C>=2 ], cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C


Computing complexity for remaining 2 transitions.

  Found configuration with infinitely models for cost: 1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C
  and guard: C>=1 && C>=C && C>=2 && C>=C && C>=2:
  C: Pos

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


The final runtime is determined by this resulting transition:
  Final Guard: C>=1 && C>=C && C>=2 && C>=C && C>=2
  Final Cost:  1/2-1/2*(-1+C)^2+(-1+C)*C+7/2*C

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),?)