Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f62 -> f63 : [ 0>=1+A ], cost: 1
      1: f62 -> f63 : [ A>=1 ], cost: 1
     27: f62 -> f71 : A'=0, L'=1, [ A==0 ], cost: 1
     24: f63 -> f71 : L'=0, [ 0>=1+D ], cost: 1
     25: f63 -> f71 : L'=0, [ D>=1 ], cost: 1
     26: f63 -> f71 : D'=0, L'=1, [ D==0 ], cost: 1
      2: f0 -> f13 : A'=1, B'=12, C'=1, D'=1, E'=free, F'=0, [], cost: 1
      3: f13 -> f13 : F'=1+F, [ B>=1+F ], cost: 1
     34: f13 -> f19 : F'=0, [ F>=B ], cost: 1
      9: f19 -> f19 : C'=0, F'=1+F, G'=0, [ B>=1+F && C==0 ], cost: 1
      4: f19 -> f22 : [ 0>=1+C && B>=1+F ], cost: 1
      5: f19 -> f22 : [ C>=1 && B>=1+F ], cost: 1
     33: f19 -> f32 : F'=0, [ F>=B ], cost: 1
      6: f22 -> f19 : C'=1, F'=1+F, G'=1, [ free_2>=0 && B>=1+free_1 ], cost: 1
      7: f22 -> f19 : C'=0, F'=1+F, G'=0, [ free_3>=0 ], cost: 1
      8: f22 -> f19 : C'=0, F'=1+F, G'=0, [ 0>=1+free_4 ], cost: 1
     10: f32 -> f35 : H'=1+F, [ B>=2+F ], cost: 1
     32: f32 -> f48 : F'=0, [ 1+F>=B ], cost: 1
     31: f35 -> f32 : F'=1+F, [ H>=B ], cost: 1
     16: f35 -> f35 : A'=0, H'=1+H, Q'=0, [ B>=1+H && A==0 ], cost: 1
     11: f35 -> f38 : [ 0>=1+A && B>=1+H ], cost: 1
     12: f35 -> f38 : [ A>=1 && B>=1+H ], cost: 1
     13: f38 -> f35 : A'=1, H'=1+H, Q'=1, [ free_6>=1+free_5 ], cost: 1
     14: f38 -> f35 : A'=1, H'=1+H, Q'=1, [], cost: 1
     15: f38 -> f35 : A'=0, H'=1+H, Q'=0, [], cost: 1
     28: f48 -> f62 : [ 0>=1+C && 1+F>=B ], cost: 1
     29: f48 -> f62 : [ C>=1 && 1+F>=B ], cost: 1
     23: f48 -> f48 : D'=0, F'=1+F, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: 1
     17: f48 -> f52 : J'=free_7, [ 0>=1+D && B>=2+F ], cost: 1
     18: f48 -> f52 : J'=free_8, [ D>=1 && B>=2+F ], cost: 1
     30: f48 -> f71 : C'=0, L'=1, [ 1+F>=B && C==0 ], cost: 1
     19: f52 -> f48 : D'=1, F'=1+F, K'=1, [ 0>=1+J ], cost: 1
     20: f52 -> f48 : D'=1, F'=1+F, K'=1, [ J>=1 ], cost: 1
     21: f52 -> f48 : D'=0, F'=1+F, J'=0, K'=0, [ J==0 ], cost: 1
     22: f52 -> f48 : D'=0, F'=1+F, K'=0, [], cost: 1

Removing duplicate transition: 7.
Removing duplicate transition: 13.

Simplified the transitions:
  Start location: f0
      2: f0 -> f13 : A'=1, B'=12, C'=1, D'=1, E'=free, F'=0, [], cost: 1
      3: f13 -> f13 : F'=1+F, [ B>=1+F ], cost: 1
     34: f13 -> f19 : F'=0, [ F>=B ], cost: 1
      9: f19 -> f19 : C'=0, F'=1+F, G'=0, [ B>=1+F && C==0 ], cost: 1
      4: f19 -> f22 : [ 0>=1+C && B>=1+F ], cost: 1
      5: f19 -> f22 : [ C>=1 && B>=1+F ], cost: 1
     33: f19 -> f32 : F'=0, [ F>=B ], cost: 1
      6: f22 -> f19 : C'=1, F'=1+F, G'=1, [], cost: 1
      8: f22 -> f19 : C'=0, F'=1+F, G'=0, [], cost: 1
     10: f32 -> f35 : H'=1+F, [ B>=2+F ], cost: 1
     32: f32 -> f48 : F'=0, [ 1+F>=B ], cost: 1
     31: f35 -> f32 : F'=1+F, [ H>=B ], cost: 1
     16: f35 -> f35 : A'=0, H'=1+H, Q'=0, [ B>=1+H && A==0 ], cost: 1
     11: f35 -> f38 : [ 0>=1+A && B>=1+H ], cost: 1
     12: f35 -> f38 : [ A>=1 && B>=1+H ], cost: 1
     14: f38 -> f35 : A'=1, H'=1+H, Q'=1, [], cost: 1
     15: f38 -> f35 : A'=0, H'=1+H, Q'=0, [], cost: 1
     23: f48 -> f48 : D'=0, F'=1+F, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: 1
     17: f48 -> f52 : J'=free_7, [ 0>=1+D && B>=2+F ], cost: 1
     18: f48 -> f52 : J'=free_8, [ D>=1 && B>=2+F ], cost: 1
     19: f52 -> f48 : D'=1, F'=1+F, K'=1, [ 0>=1+J ], cost: 1
     20: f52 -> f48 : D'=1, F'=1+F, K'=1, [ J>=1 ], cost: 1
     21: f52 -> f48 : D'=0, F'=1+F, J'=0, K'=0, [ J==0 ], cost: 1
     22: f52 -> f48 : D'=0, F'=1+F, K'=0, [], cost: 1

Eliminating 1 self-loops for location f13
  Self-Loop 3 has the metering function: B-F, resulting in the new transition 35.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f19
  Self-Loop 9 has the metering function: B-F, resulting in the new transition 36.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f35
  Self-Loop 16 has the metering function: -H+B, resulting in the new transition 37.
  Removing the self-loops: 16.
Eliminating 1 self-loops for location f48
  Self-Loop 23 has the metering function: -1+B-F, resulting in the new transition 38.
  Removing the self-loops: 23.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      2: f0 -> f13 : A'=1, B'=12, C'=1, D'=1, E'=free, F'=0, [], cost: 1
     35: f13 -> [12] : F'=B, [ B>=1+F ], cost: B-F
     36: f19 -> [13] : C'=0, F'=B, G'=0, [ B>=1+F && C==0 ], cost: B-F
      6: f22 -> f19 : C'=1, F'=1+F, G'=1, [], cost: 1
      8: f22 -> f19 : C'=0, F'=1+F, G'=0, [], cost: 1
     10: f32 -> f35 : H'=1+F, [ B>=2+F ], cost: 1
     32: f32 -> f48 : F'=0, [ 1+F>=B ], cost: 1
     37: f35 -> [14] : A'=0, H'=B, Q'=0, [ B>=1+H && A==0 ], cost: -H+B
     14: f38 -> f35 : A'=1, H'=1+H, Q'=1, [], cost: 1
     15: f38 -> f35 : A'=0, H'=1+H, Q'=0, [], cost: 1
     38: f48 -> [15] : D'=0, F'=-1+B, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: -1+B-F
     19: f52 -> f48 : D'=1, F'=1+F, K'=1, [ 0>=1+J ], cost: 1
     20: f52 -> f48 : D'=1, F'=1+F, K'=1, [ J>=1 ], cost: 1
     21: f52 -> f48 : D'=0, F'=1+F, J'=0, K'=0, [ J==0 ], cost: 1
     22: f52 -> f48 : D'=0, F'=1+F, K'=0, [], cost: 1
     34: [12] -> f19 : F'=0, [ F>=B ], cost: 1
      4: [13] -> f22 : [ 0>=1+C && B>=1+F ], cost: 1
      5: [13] -> f22 : [ C>=1 && B>=1+F ], cost: 1
     33: [13] -> f32 : F'=0, [ F>=B ], cost: 1
     31: [14] -> f32 : F'=1+F, [ H>=B ], cost: 1
     11: [14] -> f38 : [ 0>=1+A && B>=1+H ], cost: 1
     12: [14] -> f38 : [ A>=1 && B>=1+H ], cost: 1
     17: [15] -> f52 : J'=free_7, [ 0>=1+D && B>=2+F ], cost: 1
     18: [15] -> f52 : J'=free_8, [ D>=1 && B>=2+F ], cost: 1


Applied simple chaining:
  Start location: f0
      2: f0 -> f19 : A'=1, B'=12, C'=1, D'=1, E'=free, F'=0, [ 12>=1 && 12>=12 ], cost: 14
     36: f19 -> [13] : C'=0, F'=B, G'=0, [ B>=1+F && C==0 ], cost: B-F
      6: f22 -> f19 : C'=1, F'=1+F, G'=1, [], cost: 1
      8: f22 -> f19 : C'=0, F'=1+F, G'=0, [], cost: 1
     10: f32 -> f35 : H'=1+F, [ B>=2+F ], cost: 1
     32: f32 -> f48 : F'=0, [ 1+F>=B ], cost: 1
     37: f35 -> [14] : A'=0, H'=B, Q'=0, [ B>=1+H && A==0 ], cost: -H+B
     14: f38 -> f35 : A'=1, H'=1+H, Q'=1, [], cost: 1
     15: f38 -> f35 : A'=0, H'=1+H, Q'=0, [], cost: 1
     38: f48 -> [15] : D'=0, F'=-1+B, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: -1+B-F
     19: f52 -> f48 : D'=1, F'=1+F, K'=1, [ 0>=1+J ], cost: 1
     20: f52 -> f48 : D'=1, F'=1+F, K'=1, [ J>=1 ], cost: 1
     21: f52 -> f48 : D'=0, F'=1+F, J'=0, K'=0, [ J==0 ], cost: 1
     22: f52 -> f48 : D'=0, F'=1+F, K'=0, [], cost: 1
      4: [13] -> f22 : [ 0>=1+C && B>=1+F ], cost: 1
      5: [13] -> f22 : [ C>=1 && B>=1+F ], cost: 1
     33: [13] -> f32 : F'=0, [ F>=B ], cost: 1
     31: [14] -> f32 : F'=1+F, [ H>=B ], cost: 1
     11: [14] -> f38 : [ 0>=1+A && B>=1+H ], cost: 1
     12: [14] -> f38 : [ A>=1 && B>=1+H ], cost: 1
     17: [15] -> f52 : J'=free_7, [ 0>=1+D && B>=2+F ], cost: 1
     18: [15] -> f52 : J'=free_8, [ D>=1 && B>=2+F ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      2: f0 -> f19 : A'=1, B'=12, C'=1, D'=1, E'=free, F'=0, [ 12>=1 && 12>=12 ], cost: 14
     41: f19 -> f32 : C'=0, F'=0, G'=0, [ B>=1+F && C==0 && B>=B ], cost: 1+B-F
     39: f19 -> [16] : C'=0, F'=B, G'=0, [ B>=1+F && C==0 ], cost: B-F
     40: f19 -> [17] : C'=0, F'=B, G'=0, [ B>=1+F && C==0 ], cost: B-F
     10: f32 -> f35 : H'=1+F, [ B>=2+F ], cost: 1
     32: f32 -> f48 : F'=0, [ 1+F>=B ], cost: 1
     42: f35 -> f32 : A'=0, F'=1+F, H'=B, Q'=0, [ B>=1+H && A==0 && B>=B ], cost: 1-H+B
     43: f35 -> [18] : A'=0, H'=B, Q'=0, [ B>=1+H && A==0 ], cost: -H+B
     44: f35 -> [19] : A'=0, H'=B, Q'=0, [ B>=1+H && A==0 ], cost: -H+B
     45: f48 -> [20] : D'=0, F'=-1+B, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: -1+B-F
     46: f48 -> [21] : D'=0, F'=-1+B, J'=free_9, K'=0, [ B>=2+F && D==0 ], cost: -1+B-F


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


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    <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),?)