Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     25: f19 -> f15 : C'=1+C, [ E>=1+B ], cost: 1
      2: f19 -> f19 : D'=free+D, E'=1+E, [ B>=E && E>=1+C ], cost: 1
      3: f19 -> f19 : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
      4: f19 -> f19 : D'=free_2+D, E'=1+C, [ B>=E && C==E ], cost: 1
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> f66 : G'=1, [ G>=F ], cost: 1
      9: f36 -> f36 : G'=0, H'=1+H, Q'=free_6, [ F>=H && G==0 ], cost: 1
      6: f36 -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: f36 -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1
     23: f36 -> f50 : H'=1+G, [ H>=1+F ], cost: 1
     22: f41 -> f36 : H'=1+H, [ J>=G ], cost: 1
      8: f41 -> f41 : Q'=free_5, J'=1+J, [ G>=1+J ], cost: 1
     21: f50 -> f33 : G'=1+G, [ H>=1+F ], cost: 1
     10: f50 -> f54 : Q'=free_7, J'=0, [ F>=H ], cost: 1
     20: f54 -> f50 : H'=1+H, [ J>=1+G ], cost: 1
     11: f54 -> f54 : Q'=free_8, J'=1+J, [ G>=J ], cost: 1
     12: f66 -> f70 : H'=0, Q'=free_9, [ F>=G ], cost: 1
     19: f66 -> f80 : G'=-1+F, [ G>=1+F ], cost: 1
     18: f70 -> f66 : G'=1+G, [ H>=G ], cost: 1
     13: f70 -> f70 : H'=1+H, Q'=free_10, [ G>=1+H ], cost: 1
     14: f80 -> f84 : H'=1+G, Q'=free_11, [ G>=0 ], cost: 1
     17: f80 -> f96 : K'=0, L'=0, [ 0>=1+G ], cost: 1
     16: f84 -> f80 : G'=-1+G, [ H>=1+F ], cost: 1
     15: f84 -> f84 : H'=1+H, Q'=free_12, [ F>=H ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     25: f19 -> f15 : C'=1+C, [ E>=1+B ], cost: 1
      2: f19 -> f19 : D'=free+D, E'=1+E, [ B>=E && E>=1+C ], cost: 1
      3: f19 -> f19 : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
      4: f19 -> f19 : D'=free_2+D, E'=1+C, [ B>=E && C==E ], cost: 1
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> f66 : G'=1, [ G>=F ], cost: 1
      9: f36 -> f36 : G'=0, H'=1+H, Q'=free_6, [ F>=H && G==0 ], cost: 1
      6: f36 -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: f36 -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1
     23: f36 -> f50 : H'=1+G, [ H>=1+F ], cost: 1
     22: f41 -> f36 : H'=1+H, [ J>=G ], cost: 1
      8: f41 -> f41 : Q'=free_5, J'=1+J, [ G>=1+J ], cost: 1
     21: f50 -> f33 : G'=1+G, [ H>=1+F ], cost: 1
     10: f50 -> f54 : Q'=free_7, J'=0, [ F>=H ], cost: 1
     20: f54 -> f50 : H'=1+H, [ J>=1+G ], cost: 1
     11: f54 -> f54 : Q'=free_8, J'=1+J, [ G>=J ], cost: 1
     12: f66 -> f70 : H'=0, Q'=free_9, [ F>=G ], cost: 1
     19: f66 -> f80 : G'=-1+F, [ G>=1+F ], cost: 1
     18: f70 -> f66 : G'=1+G, [ H>=G ], cost: 1
     13: f70 -> f70 : H'=1+H, Q'=free_10, [ G>=1+H ], cost: 1
     14: f80 -> f84 : H'=1+G, Q'=free_11, [ G>=0 ], cost: 1
     16: f84 -> f80 : G'=-1+G, [ H>=1+F ], cost: 1
     15: f84 -> f84 : H'=1+H, Q'=free_12, [ F>=H ], cost: 1

Eliminating 3 self-loops for location f19
  Self-Loop 2 has the metering function: 1-E+B, resulting in the new transition 27.
  Self-Loop 4 has the metering function: -E+C, resulting in the new transition 29.
  Found this metering function when nesting loops: meter,
  Found this metering function when nesting loops: meter_1,
  Removing the self-loops: 2 3 4.
Adding an epsilon transition (to model nonexecution of the loops): 30.
Eliminating 1 self-loops for location f36
  Self-Loop 9 has the metering function: 1-H+F, resulting in the new transition 31.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f41
  Self-Loop 8 has the metering function: -J+G, resulting in the new transition 32.
  Removing the self-loops: 8.
Eliminating 1 self-loops for location f54
  Self-Loop 11 has the metering function: 1-J+G, resulting in the new transition 33.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location f70
  Self-Loop 13 has the metering function: -H+G, resulting in the new transition 34.
  Removing the self-loops: 13.
Eliminating 1 self-loops for location f84
  Self-Loop 15 has the metering function: 1-H+F, resulting in the new transition 35.
  Removing the self-loops: 15.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     27: f19 -> [13] : D'=-(-1+E-B)*free+D, E'=1+B, [ B>=E && E>=1+C ], cost: 1-E+B
     28: f19 -> [13] : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
     29: f19 -> [13] : D'=D-free_2*(E-C), E'=1+C, [ B>=E && C==E ], cost: -E+C
     30: f19 -> [13] : [], cost: 0
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> f66 : G'=1, [ G>=F ], cost: 1
     31: f36 -> [14] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     32: f41 -> [15] : Q'=free_5, J'=G, [ G>=1+J ], cost: -J+G
     21: f50 -> f33 : G'=1+G, [ H>=1+F ], cost: 1
     10: f50 -> f54 : Q'=free_7, J'=0, [ F>=H ], cost: 1
     33: f54 -> [16] : Q'=free_8, J'=1+G, [ G>=J ], cost: 1-J+G
     12: f66 -> f70 : H'=0, Q'=free_9, [ F>=G ], cost: 1
     19: f66 -> f80 : G'=-1+F, [ G>=1+F ], cost: 1
     34: f70 -> [17] : H'=G, Q'=free_10, [ G>=1+H ], cost: -H+G
     14: f80 -> f84 : H'=1+G, Q'=free_11, [ G>=0 ], cost: 1
     35: f84 -> [18] : H'=1+F, Q'=free_12, [ F>=H ], cost: 1-H+F
     25: [13] -> f15 : C'=1+C, [ E>=1+B ], cost: 1
      6: [14] -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: [14] -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1
     23: [14] -> f50 : H'=1+G, [ H>=1+F ], cost: 1
     22: [15] -> f36 : H'=1+H, [ J>=G ], cost: 1
     20: [16] -> f50 : H'=1+H, [ J>=1+G ], cost: 1
     18: [17] -> f66 : G'=1+G, [ H>=G ], cost: 1
     16: [18] -> f80 : G'=-1+G, [ H>=1+F ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     27: f19 -> [13] : D'=-(-1+E-B)*free+D, E'=1+B, [ B>=E && E>=1+C ], cost: 1-E+B
     28: f19 -> [13] : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
     29: f19 -> [13] : D'=D-free_2*(E-C), E'=1+C, [ B>=E && C==E ], cost: -E+C
     30: f19 -> [13] : [], cost: 0
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> f66 : G'=1, [ G>=F ], cost: 1
     31: f36 -> [14] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     32: f41 -> f36 : H'=1+H, Q'=free_5, J'=G, [ G>=1+J && G>=G ], cost: 1-J+G
     21: f50 -> f33 : G'=1+G, [ H>=1+F ], cost: 1
     10: f50 -> f50 : H'=1+H, Q'=free_8, J'=1+G, [ F>=H && G>=0 && 1+G>=1+G ], cost: 3+G
     12: f66 -> f66 : G'=1+G, H'=G, Q'=free_10, [ F>=G && G>=1 && G>=G ], cost: 2+G
     19: f66 -> f80 : G'=-1+F, [ G>=1+F ], cost: 1
     14: f80 -> f80 : G'=-1+G, H'=1+F, Q'=free_12, [ G>=0 && F>=1+G && 1+F>=1+F ], cost: 2+F-G
     25: [13] -> f15 : C'=1+C, [ E>=1+B ], cost: 1
      6: [14] -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: [14] -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1
     23: [14] -> f50 : H'=1+G, [ H>=1+F ], cost: 1

Eliminating 1 self-loops for location f50
  Self-Loop 10 has the metering function: 1-H+F, resulting in the new transition 36.
  Removing the self-loops: 10.
Eliminating 1 self-loops for location f66
  Self-Loop 12 has the metering function: 1+F-G, resulting in the new transition 37.
  Removing the self-loops: 12.
Eliminating 1 self-loops for location f80
  Self-Loop 14 has the metering function: 1+G, resulting in the new transition 38.
  Removing the self-loops: 14.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     27: f19 -> [13] : D'=-(-1+E-B)*free+D, E'=1+B, [ B>=E && E>=1+C ], cost: 1-E+B
     28: f19 -> [13] : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
     29: f19 -> [13] : D'=D-free_2*(E-C), E'=1+C, [ B>=E && C==E ], cost: -E+C
     30: f19 -> [13] : [], cost: 0
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> f66 : G'=1, [ G>=F ], cost: 1
     31: f36 -> [14] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     32: f41 -> f36 : H'=1+H, Q'=free_5, J'=G, [ G>=1+J && G>=G ], cost: 1-J+G
     36: f50 -> [19] : H'=1+F, Q'=free_8, J'=1+G, [ F>=H && G>=0 ], cost: 3-3*H+3*F-(-1+H-F)*G
     37: f66 -> [20] : G'=1+F, H'=F, Q'=free_10, [ F>=G && G>=1 ], cost: 3/2+(1+F-G)*G+3/2*F+1/2*(1+F-G)^2-3/2*G
     38: f80 -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=0 && F>=1+G ], cost: 3/2-(1+G)*G+1/2*(1+G)^2+(1+G)*F+3/2*G
     25: [13] -> f15 : C'=1+C, [ E>=1+B ], cost: 1
      6: [14] -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: [14] -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1
     23: [14] -> f50 : H'=1+G, [ H>=1+F ], cost: 1
     21: [19] -> f33 : G'=1+G, [ H>=1+F ], cost: 1
     19: [20] -> f80 : G'=-1+F, [ G>=1+F ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
      1: f15 -> f19 : D'=0, E'=0, [ B>=C ], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     27: f19 -> [13] : D'=-(-1+E-B)*free+D, E'=1+B, [ B>=E && E>=1+C ], cost: 1-E+B
     28: f19 -> [13] : D'=free_1+D, E'=1+E, [ C>=1+E && B>=E ], cost: 1
     29: f19 -> [13] : D'=D-free_2*(E-C), E'=1+C, [ B>=E && C==E ], cost: -E+C
     30: f19 -> [13] : [], cost: 0
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=F && F>=1 && 1>=1 && 1+F>=1+F && -1+F>=0 && F>=F ], cost: 2+4*F-(-1+F)*F+2*F^2
     31: f36 -> [14] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     32: f41 -> f36 : H'=1+H, Q'=free_5, J'=G, [ G>=1+J && G>=G ], cost: 1-J+G
     25: [13] -> f15 : C'=1+C, [ E>=1+B ], cost: 1
     23: [14] -> f33 : G'=1+G, H'=1+F, Q'=free_8, J'=1+G, [ H>=1+F && F>=1+G && G>=0 && 1+F>=1+F ], cost: 2+(F-G)*G+3*F-3*G
      6: [14] -> f41 : Q'=free_3, J'=0, [ 0>=1+G && F>=H ], cost: 1
      7: [14] -> f41 : Q'=free_4, J'=0, [ G>=1 && F>=H ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     39: f15 -> [13] : D'=(1+B)*free, E'=1+B, [ B>=C && B>=0 && 0>=1+C ], cost: 2+B
     40: f15 -> [13] : D'=free_1, E'=1, [ B>=C && C>=1 && B>=0 ], cost: 2
     41: f15 -> [13] : D'=free_2*C, E'=1+C, [ B>=C && B>=0 && C==0 ], cost: 1+C
     42: f15 -> [13] : D'=0, E'=0, [ B>=C ], cost: 1
      5: f33 -> f36 : H'=1+G, [ F>=1+G ], cost: 1
     24: f33 -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=F && F>=1 && 1>=1 && 1+F>=1+F && -1+F>=0 && F>=F ], cost: 2+4*F-(-1+F)*F+2*F^2
     43: f36 -> f33 : G'=1, H'=1+F, Q'=free_8, J'=1, [ F>=H && G==0 && 1+F>=1+F && F>=1 && 0>=0 && 1+F>=1+F ], cost: 3-H+4*F
     44: f36 -> [22] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     45: f36 -> [23] : G'=0, H'=1+F, Q'=free_6, [ F>=H && G==0 ], cost: 1-H+F
     25: [13] -> f15 : C'=1+C, [ E>=1+B ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
     46: f15 -> f15 : C'=1+C, D'=(1+B)*free, E'=1+B, [ B>=C && B>=0 && 0>=1+C && 1+B>=1+B ], cost: 3+B
     47: f15 -> f15 : C'=1+C, D'=free_2*C, E'=1+C, [ B>=C && B>=0 && C==0 && 1+C>=1+B ], cost: 2+C
     48: f15 -> f15 : C'=1+C, D'=0, E'=0, [ B>=C && 0>=1+B ], cost: 2
     26: f15 -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     49: f33 -> f33 : G'=1, H'=1+F, Q'=free_8, J'=1, [ F>=1+G && F>=1+G && G==0 && 1+F>=1+F && F>=1 && 0>=0 && 1+F>=1+F ], cost: 3+4*F-G
     24: f33 -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=F && F>=1 && 1>=1 && 1+F>=1+F && -1+F>=0 && F>=F ], cost: 2+4*F-(-1+F)*F+2*F^2
     50: f33 -> [22] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G
     51: f33 -> [23] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G

Eliminating 3 self-loops for location f15
  Self-Loop 46 has the metering function: -C, resulting in the new transition 52.
  Self-Loop 47 has the metering function: 1-B-C, resulting in the new transition 53.
  Self-Loop 48 has the metering function: 1+B-C, resulting in the new transition 54.
  Found this metering function when nesting loops: -B,
  Found this metering function when nesting loops: meter_2,
  Removing the self-loops: 46 47 48.
Eliminating 1 self-loops for location f33
  Self-Loop 49 has the metering function: 1-G, resulting in the new transition 55.
  Removing the self-loops: 49.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
     52: f15 -> [24] : C'=0, D'=free+B*free, E'=1+B, [ B>=C && B>=0 && 0>=1+C ], cost: -B*C-3*C
     53: f15 -> [24] : C'=1-B, D'=-free_2+free_2*C-free_2*(-1+B+C), E'=1-B, [ -B+C==0 && B>=0 && C==0 ], cost: 3/2-C*(-1+B+C)-3/2*B-3/2*C+1/2*(-1+B+C)^2
     54: f15 -> [24] : C'=1+B, D'=0, E'=0, [ B>=C && 0>=1+B ], cost: 2+2*B-2*C
     55: f33 -> [25] : G'=1, H'=1+F, Q'=free_8, J'=1, [ F>=1+G && G==0 && F>=1 ], cost: 2-4*F*(-1+G)-2*G
     26: [24] -> f33 : F'=B, G'=0, M'=A, [ C>=1+B ], cost: 1
     24: [25] -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=F && F>=1 && 1>=1 && 1+F>=1+F && -1+F>=0 && F>=F ], cost: 2+4*F-(-1+F)*F+2*F^2
     50: [25] -> [22] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G
     51: [25] -> [23] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G


Applied simple chaining:
  Start location: f0
      0: f0 -> f15 : A'=50, B'=5, C'=0, [], cost: 1
     52: f15 -> [24] : C'=0, D'=free+B*free, E'=1+B, [ B>=C && B>=0 && 0>=1+C ], cost: -B*C-3*C
     53: f15 -> [24] : C'=1-B, D'=-free_2+free_2*C-free_2*(-1+B+C), E'=1-B, [ -B+C==0 && B>=0 && C==0 ], cost: 3/2-C*(-1+B+C)-3/2*B-3/2*C+1/2*(-1+B+C)^2
     54: f15 -> [24] : C'=1+B, D'=0, E'=0, [ B>=C && 0>=1+B ], cost: 2+2*B-2*C
     26: [24] -> [25] : F'=B, G'=1, H'=1+B, Q'=free_8, J'=1, M'=A, [ C>=1+B && B>=1 && 0==0 && B>=1 ], cost: 3+4*B
     24: [25] -> [21] : G'=-1, H'=1+F, Q'=free_12, [ G>=F && F>=1 && 1>=1 && 1+F>=1+F && -1+F>=0 && F>=F ], cost: 2+4*F-(-1+F)*F+2*F^2
     50: [25] -> [22] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G
     51: [25] -> [23] : G'=0, H'=1+F, Q'=free_6, [ F>=1+G && F>=1+G && G==0 ], cost: 1+F-G


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