Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      8: f6 -> f25 : [ 0>=A ], cost: 1
      7: f10 -> f6 : [ 0>=B ], cost: 1
      2: f10 -> f14 : B'=-1+B, C'=-1+A, [ B>=1 ], cost: 1
      6: f14 -> f10 : [ 0>=C ], cost: 1
      3: f14 -> f14 : C'=-1+C, D'=0, [ C>=1 ], cost: 1
      4: f14 -> f14 : A'=-1+A, B'=1+B, C'=-1+C, D'=free_1, [ C>=1 && 0>=1+free_1 ], cost: 1
      5: f14 -> f14 : A'=-1+A, B'=1+B, C'=-1+C, D'=free_2, [ C>=1 && free_2>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      7: f10 -> f6 : [ 0>=B ], cost: 1
      2: f10 -> f14 : B'=-1+B, C'=-1+A, [ B>=1 ], cost: 1
      6: f14 -> f10 : [ 0>=C ], cost: 1
      3: f14 -> f14 : C'=-1+C, D'=0, [ C>=1 ], cost: 1
      4: f14 -> f14 : A'=-1+A, B'=1+B, C'=-1+C, D'=free_1, [ C>=1 && 0>=1+free_1 ], cost: 1
      5: f14 -> f14 : A'=-1+A, B'=1+B, C'=-1+C, D'=free_2, [ C>=1 && free_2>=1 ], cost: 1

Eliminating 3 self-loops for location f14
  Self-Loop 3 has the metering function: C, resulting in the new transition 9.
  Self-Loop 4 has the metering function: C, resulting in the new transition 10.
  Self-Loop 5 has the metering function: C, resulting in the new transition 11.
  Removing the self-loops: 3 4 5.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      7: f10 -> f6 : [ 0>=B ], cost: 1
      2: f10 -> f14 : B'=-1+B, C'=-1+A, [ B>=1 ], cost: 1
      9: f14 -> [5] : C'=0, D'=0, [ C>=1 ], cost: C
     10: f14 -> [5] : A'=-C+A, B'=B+C, C'=0, D'=free_1, [ C>=1 && 0>=1+free_1 ], cost: C
     11: f14 -> [5] : A'=-C+A, B'=B+C, C'=0, D'=free_2, [ C>=1 && free_2>=1 ], cost: C
      6: [5] -> f10 : [ 0>=C ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      7: f10 -> f6 : [ 0>=B ], cost: 1
     12: f10 -> [5] : B'=-1+B, C'=0, D'=0, [ B>=1 && -1+A>=1 ], cost: A
     13: f10 -> [5] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ B>=1 && -1+A>=1 && 0>=1+free_1 ], cost: A
     14: f10 -> [5] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ B>=1 && -1+A>=1 && free_2>=1 ], cost: A
      6: [5] -> f10 : [ 0>=C ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      7: f10 -> f6 : [ 0>=B ], cost: 1
     15: f10 -> f10 : B'=-1+B, C'=0, D'=0, [ B>=1 && -1+A>=1 && 0>=0 ], cost: 1+A
     16: f10 -> f10 : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ B>=1 && -1+A>=1 && 0>=1+free_1 && 0>=0 ], cost: 1+A
     17: f10 -> f10 : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ B>=1 && -1+A>=1 && free_2>=1 && 0>=0 ], cost: 1+A

Eliminating 3 self-loops for location f10
  Self-Loop 15 has the metering function: B, resulting in the new transition 18.
  Removing the self-loops: 15 16 17.
Adding an epsilon transition (to model nonexecution of the loops): 21.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
      1: f6 -> f10 : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
     18: f10 -> [6] : B'=0, C'=0, D'=0, [ B>=1 && -1+A>=1 ], cost: B+B*A
     19: f10 -> [6] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ B>=1 && -1+A>=1 && 0>=1+free_1 ], cost: 1+A
     20: f10 -> [6] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ B>=1 && -1+A>=1 && free_2>=1 ], cost: 1+A
     21: f10 -> [6] : [], cost: 0
      7: [6] -> f6 : [ 0>=B ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
     22: f6 -> [6] : A'=-1+A, B'=0, C'=0, D'=0, [ A>=1 && 1+B>=1 && -2+A>=1 ], cost: 2+B+(1+B)*(-1+A)
     23: f6 -> [6] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ A>=1 && 1+B>=1 && -2+A>=1 && 0>=1+free_1 ], cost: 1+A
     24: f6 -> [6] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ A>=1 && 1+B>=1 && -2+A>=1 && free_2>=1 ], cost: 1+A
     25: f6 -> [6] : A'=-1+A, B'=1+B, [ A>=1 ], cost: 1
      7: [6] -> f6 : [ 0>=B ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
     26: f6 -> f6 : A'=-1+A, B'=0, C'=0, D'=0, [ A>=1 && 1+B>=1 && -2+A>=1 && 0>=0 ], cost: 3+B+(1+B)*(-1+A)
     29: f6 -> f6 : A'=-1+A, B'=1+B, [ A>=1 && 0>=1+B ], cost: 2
     27: f6 -> [7] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ A>=1 && 1+B>=1 && -2+A>=1 && 0>=1+free_1 ], cost: 1+A
     28: f6 -> [8] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ A>=1 && 1+B>=1 && -2+A>=1 && free_2>=1 ], cost: 1+A

Eliminating 2 self-loops for location f6
  Self-Loop 26 has the metering function: -2+A, resulting in the new transition 30.
  Self-Loop 32 has unbounded runtime, resulting in the new transition 34.
  Found this metering function when nesting loops: -1-B,
  Removing the self-loops: 26 29 31 32.
Adding an epsilon transition (to model nonexecution of the loops): 35.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f6 : A'=free, B'=0, [], cost: 1
     30: f6 -> [9] : A'=2, B'=0, C'=0, D'=0, [ 1+B>=1 && -2+A>=1 ], cost: -5-1/2*(-2+A)^2+(-2+A)*A+5/2*A
     33: f6 -> [9] : A'=-1+A, B'=1+B, [ A>=1 && 0>=1+B ], cost: 2
     34: f6 -> [9] : [ A>=1 && 0>=1+B && B>A ], cost: INF
     35: f6 -> [9] : [], cost: 0
     27: [9] -> [7] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ A>=1 && 1+B>=1 && -2+A>=1 && 0>=1+free_1 ], cost: 1+A
     28: [9] -> [8] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ A>=1 && 1+B>=1 && -2+A>=1 && free_2>=1 ], cost: 1+A


Applied chaining over branches and pruning:
  Start location: f0
     36: f0 -> [9] : A'=2, B'=0, C'=0, D'=0, [ 1>=1 && -2+free>=1 ], cost: -4+free*(-2+free)+5/2*free-1/2*(-2+free)^2
     37: f0 -> [9] : A'=free, B'=0, [], cost: 1
     27: [9] -> [7] : A'=1, B'=-2+B+A, C'=0, D'=free_1, [ A>=1 && 1+B>=1 && -2+A>=1 && 0>=1+free_1 ], cost: 1+A
     28: [9] -> [8] : A'=1, B'=-2+B+A, C'=0, D'=free_2, [ A>=1 && 1+B>=1 && -2+A>=1 && free_2>=1 ], cost: 1+A


Applied chaining over branches and pruning:
  Start location: f0
     40: f0 -> [7] : A'=1, B'=-2+free, C'=0, D'=free_1, [ free>=1 && 1>=1 && -2+free>=1 && 0>=1+free_1 ], cost: 2+free
     41: f0 -> [8] : A'=1, B'=-2+free, C'=0, D'=free_2, [ free>=1 && 1>=1 && -2+free>=1 && free_2>=1 ], cost: 2+free
     38: f0 -> [10] : A'=2, B'=0, C'=0, D'=0, [ 1>=1 && -2+free>=1 ], cost: -4+free*(-2+free)+5/2*free-1/2*(-2+free)^2
     39: f0 -> [11] : A'=2, B'=0, C'=0, D'=0, [ 1>=1 && -2+free>=1 ], cost: -4+free*(-2+free)+5/2*free-1/2*(-2+free)^2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     40: f0 -> [7] : A'=1, B'=-2+free, C'=0, D'=free_1, [ free>=1 && 1>=1 && -2+free>=1 && 0>=1+free_1 ], cost: 2+free
     41: f0 -> [8] : A'=1, B'=-2+free, C'=0, D'=free_2, [ free>=1 && 1>=1 && -2+free>=1 && free_2>=1 ], cost: 2+free
     38: f0 -> [10] : A'=2, B'=0, C'=0, D'=0, [ 1>=1 && -2+free>=1 ], cost: -4+free*(-2+free)+5/2*free-1/2*(-2+free)^2
     39: f0 -> [11] : A'=2, B'=0, C'=0, D'=0, [ 1>=1 && -2+free>=1 ], cost: -4+free*(-2+free)+5/2*free-1/2*(-2+free)^2


Computing complexity for remaining 4 transitions.

  Found configuration with infinitely models for cost: 2+free
  and guard: free>=1 && 1>=1 && -2+free>=1 && 0>=1+free_1:
  free: Pos, free_1: Neg

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free>=1 && 1>=1 && -2+free>=1 && 0>=1+free_1
  Final Cost:  2+free

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

WORST_CASE(INF,?)