Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f422 : A'=3, B'=43690, C'=3, D'=free, E'=0, [], cost: 1
      1: f422 -> f422 : C'=free_2, D'=free_1, E'=1+E, [ 149>=E ], cost: 1
     22: f422 -> f437 : A'=C, F'=0, O1'=C, P1'=C, [ E>=150 ], cost: 1
      2: f437 -> f441 : G'=0, H'=0, [ 49>=F ], cost: 1
     21: f437 -> f455 : Q'=0, [ F>=50 ], cost: 1
     20: f441 -> f437 : F'=1+F, [ H>=50 ], cost: 1
      3: f441 -> f441 : G'=free_3, H'=1+H, [ 49>=H ], cost: 1
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f485 : Q_1'=98, R'=free_17, N1'=100, [ Q>=100 ], cost: 1
     18: f461 -> f455 : Q'=2+Q, [ M>=32 ], cost: 1
      5: f461 -> f461 : J'=free_9, K'=free_5, L'=free_7, M'=2+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M ], cost: 1
      6: f485 -> f485 : Q_1'=-1+Q_1, R'=free_11, [ Q_1>=0 ], cost: 1
     17: f485 -> f501 : B'=R, S'=0, T'=free_16, M1'=R, [ 0>=1+Q_1 ], cost: 1
      7: f501 -> f501 : S'=1+S, T'=free_13, U'=free_12, [ 49>=S ], cost: 1
     16: f501 -> f526 : V'=17, W'=2, E1'=B, G1'=B, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, [ S>=50 ], cost: 1
      8: f526 -> f526 : W'=1+W, [ V>=W ], cost: 1
     15: f526 -> f540 : X'=1, A1'=0, B1'=13, C1'=8, D1'=E1, F1'=E1, [ W>=1+V ], cost: 1
      9: f540 -> f543 : Y'=0, [ 8>=X ], cost: 1
     14: f540 -> f584 : [ X>=9 ], cost: 1
     13: f543 -> f540 : X'=7+X, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ Y>=8 ], cost: 1
     10: f543 -> f546 : Z'=0, [ 7>=Y ], cost: 1
     12: f546 -> f543 : Y'=1+Y, [ Z>=4 ], cost: 1
     11: f546 -> f546 : Z'=1+Z, [ 3>=Z ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f422 : A'=3, B'=43690, C'=3, D'=free, E'=0, [], cost: 1
      1: f422 -> f422 : C'=free_2, D'=free_1, E'=1+E, [ 149>=E ], cost: 1
     22: f422 -> f437 : A'=C, F'=0, O1'=C, P1'=C, [ E>=150 ], cost: 1
      2: f437 -> f441 : G'=0, H'=0, [ 49>=F ], cost: 1
     21: f437 -> f455 : Q'=0, [ F>=50 ], cost: 1
     20: f441 -> f437 : F'=1+F, [ H>=50 ], cost: 1
      3: f441 -> f441 : G'=free_3, H'=1+H, [ 49>=H ], cost: 1
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f485 : Q_1'=98, R'=free_17, N1'=100, [ Q>=100 ], cost: 1
     18: f461 -> f455 : Q'=2+Q, [ M>=32 ], cost: 1
      5: f461 -> f461 : J'=free_9, K'=free_5, L'=free_7, M'=2+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M ], cost: 1
      6: f485 -> f485 : Q_1'=-1+Q_1, R'=free_11, [ Q_1>=0 ], cost: 1
     17: f485 -> f501 : B'=R, S'=0, T'=free_16, M1'=R, [ 0>=1+Q_1 ], cost: 1
      7: f501 -> f501 : S'=1+S, T'=free_13, U'=free_12, [ 49>=S ], cost: 1
     16: f501 -> f526 : V'=17, W'=2, E1'=B, G1'=B, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, [ S>=50 ], cost: 1
      8: f526 -> f526 : W'=1+W, [ V>=W ], cost: 1
     15: f526 -> f540 : X'=1, A1'=0, B1'=13, C1'=8, D1'=E1, F1'=E1, [ W>=1+V ], cost: 1
      9: f540 -> f543 : Y'=0, [ 8>=X ], cost: 1
     13: f543 -> f540 : X'=7+X, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ Y>=8 ], cost: 1
     10: f543 -> f546 : Z'=0, [ 7>=Y ], cost: 1
     12: f546 -> f543 : Y'=1+Y, [ Z>=4 ], cost: 1
     11: f546 -> f546 : Z'=1+Z, [ 3>=Z ], cost: 1

Eliminating 1 self-loops for location f422
  Self-Loop 1 has the metering function: 150-E, resulting in the new transition 23.
  Removing the self-loops: 1.
Eliminating 1 self-loops for location f441
  Self-Loop 3 has the metering function: 50-H, resulting in the new transition 24.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f461
  Self-Loop 5 has the metering function: meter, resulting in the new transition 25.
  Removing the self-loops: 5.
Eliminating 1 self-loops for location f485
  Self-Loop 6 has the metering function: 1+Q_1, resulting in the new transition 26.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location f501
  Self-Loop 7 has the metering function: 50-S, resulting in the new transition 27.
  Removing the self-loops: 7.
Eliminating 1 self-loops for location f526
  Self-Loop 8 has the metering function: 1+V-W, resulting in the new transition 28.
  Removing the self-loops: 8.
Eliminating 1 self-loops for location f546
  Self-Loop 11 has the metering function: 4-Z, resulting in the new transition 29.
  Removing the self-loops: 11.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f422 : A'=3, B'=43690, C'=3, D'=free, E'=0, [], cost: 1
     23: f422 -> [13] : C'=free_2, D'=free_1, E'=150, [ 149>=E ], cost: 150-E
      2: f437 -> f441 : G'=0, H'=0, [ 49>=F ], cost: 1
     21: f437 -> f455 : Q'=0, [ F>=50 ], cost: 1
     24: f441 -> [14] : G'=free_3, H'=50, [ 49>=H ], cost: 50-H
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f485 : Q_1'=98, R'=free_17, N1'=100, [ Q>=100 ], cost: 1
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
     26: f485 -> [16] : Q_1'=-1, R'=free_11, [ Q_1>=0 ], cost: 1+Q_1
     27: f501 -> [17] : S'=50, T'=free_13, U'=free_12, [ 49>=S ], cost: 50-S
     28: f526 -> [18] : W'=1+V, [ V>=W ], cost: 1+V-W
      9: f540 -> f543 : Y'=0, [ 8>=X ], cost: 1
     13: f543 -> f540 : X'=7+X, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ Y>=8 ], cost: 1
     10: f543 -> f546 : Z'=0, [ 7>=Y ], cost: 1
     29: f546 -> [19] : Z'=4, [ 3>=Z ], cost: 4-Z
     22: [13] -> f437 : A'=C, F'=0, O1'=C, P1'=C, [ E>=150 ], cost: 1
     20: [14] -> f437 : F'=1+F, [ H>=50 ], cost: 1
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1
     17: [16] -> f501 : B'=R, S'=0, T'=free_16, M1'=R, [ 0>=1+Q_1 ], cost: 1
     16: [17] -> f526 : V'=17, W'=2, E1'=B, G1'=B, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, [ S>=50 ], cost: 1
     15: [18] -> f540 : X'=1, A1'=0, B1'=13, C1'=8, D1'=E1, F1'=E1, [ W>=1+V ], cost: 1
     12: [19] -> f543 : Y'=1+Y, [ Z>=4 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f437 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 ], cost: 152
      2: f437 -> f437 : F'=1+F, G'=free_3, H'=50, [ 49>=F && 49>=0 && 50>=50 ], cost: 52
     21: f437 -> f455 : Q'=0, [ F>=50 ], cost: 1
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f540 : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1, A1'=0, B1'=13, C1'=8, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 ], cost: 169
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
      9: f540 -> f543 : Y'=0, [ 8>=X ], cost: 1
     13: f543 -> f540 : X'=7+X, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ Y>=8 ], cost: 1
     10: f543 -> f543 : Y'=1+Y, Z'=4, [ 7>=Y && 3>=0 && 4>=4 ], cost: 6
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1

Eliminating 1 self-loops for location f437
  Self-Loop 2 has the metering function: 50-F, resulting in the new transition 30.
  Removing the self-loops: 2.
Eliminating 1 self-loops for location f543
  Self-Loop 10 has the metering function: 8-Y, resulting in the new transition 31.
  Removing the self-loops: 10.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f437 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 ], cost: 152
     30: f437 -> [20] : F'=50, G'=free_3, H'=50, [ 49>=F ], cost: 2600-52*F
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f540 : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1, A1'=0, B1'=13, C1'=8, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 ], cost: 169
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
      9: f540 -> f543 : Y'=0, [ 8>=X ], cost: 1
     31: f543 -> [21] : Y'=8, Z'=4, [ 7>=Y ], cost: 48-6*Y
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1
     21: [20] -> f455 : Q'=0, [ F>=50 ], cost: 1
     13: [21] -> f540 : X'=7+X, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ Y>=8 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f455 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=50, G'=free_3, H'=50, Q'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 && 49>=0 && 50>=50 ], cost: 2753
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f540 : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1, A1'=0, B1'=13, C1'=8, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 ], cost: 169
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
      9: f540 -> f540 : X'=7+X, Y'=8, Z'=4, A1'=3+A1, B1'=3+B1, C1'=-7+C1, [ 8>=X && 7>=0 && 8>=8 ], cost: 50
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1

Eliminating 1 self-loops for location f540
  Self-Loop 9 has the metering function: meter_1, resulting in the new transition 32.
  Removing the self-loops: 9.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f455 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=50, G'=free_3, H'=50, Q'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 && 49>=0 && 50>=50 ], cost: 2753
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> f540 : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1, A1'=0, B1'=13, C1'=8, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 ], cost: 169
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
     32: f540 -> [22] : X'=X+7*meter_1, Y'=8, Z'=4, A1'=A1+3*meter_1, B1'=3*meter_1+B1, C1'=-7*meter_1+C1, [ 8>=X && 7*meter_1==8-X ], cost: 50*meter_1
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f455 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=50, G'=free_3, H'=50, Q'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 && 49>=0 && 50>=50 ], cost: 2753
      4: f455 -> f461 : J'=0, K'=0, L'=free_4, M'=0, [ 99>=Q ], cost: 1
     19: f455 -> [22] : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1+7*meter_1, Y'=8, Z'=4, A1'=3*meter_1, B1'=13+3*meter_1, C1'=8-7*meter_1, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 && 8>=1 && 7*meter_1==7 ], cost: 169+50*meter_1
     25: f461 -> [15] : J'=free_9, K'=free_5, L'=free_7, M'=2*meter+M, N'=free_10, O'=free_6, P'=free_8, [ 31>=M && 2*meter==31-M ], cost: meter
     18: [15] -> f455 : Q'=2+Q, [ M>=32 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f455 : A'=free_2, B'=43690, C'=free_2, D'=free_1, E'=150, F'=50, G'=free_3, H'=50, Q'=0, O1'=free_2, P1'=free_2, [ 149>=0 && 150>=150 && 49>=0 && 50>=50 ], cost: 2753
     19: f455 -> [22] : B'=free_11, Q_1'=-1, R'=free_11, S'=50, T'=free_13, U'=free_12, V'=17, W'=18, X'=1+7*meter_1, Y'=8, Z'=4, A1'=3*meter_1, B1'=13+3*meter_1, C1'=8-7*meter_1, D1'=free_11, E1'=free_11, F1'=free_11, G1'=free_11, H1'=1, Q1'=free_15, J1'=A, K1'=1, L1'=free_14, M1'=free_11, N1'=100, [ Q>=100 && 98>=0 && 0>=0 && 49>=0 && 50>=50 && 17>=2 && 18>=18 && 8>=1 && 7*meter_1==7 ], cost: 169+50*meter_1


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