Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
     11: f13 -> f13 : A'=1+A, C'=1, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, [ 0>=free_16 && B>=1+A ], cost: 1
      0: f13 -> f45 : [ A>=B ], cost: 1
      8: f13 -> f45 : H'=free_2, Q'=free_3, J'=free, K'=free_1, L'=E, M'=free_2, N'=free_2, [ free_2>=1 && B>=1+A ], cost: 1
      9: f13 -> f37 : C'=free_7, H'=free_6, Q'=free_8, J'=free_4, K'=free_5, L'=E, M'=free_6, N'=free_6, O'=free_6, P'=Q_1, Q_1'=0, R'=free_7, S'=free_7, T'=0, [ B>=1+A && 0>=free_6 && free_7>=2 ], cost: 1
     10: f13 -> f37 : C'=free_12, H'=free_11, Q'=free_13, J'=free_9, K'=free_10, L'=E, M'=free_11, N'=free_11, O'=free_11, P'=Q_1, Q_1'=0, R'=free_12, S'=free_12, T'=0, [ B>=1+A && 0>=free_11 && 0>=free_12 ], cost: 1
      5: f45 -> f52 : E'=0, [ D>=1 ], cost: 1
      6: f45 -> f52 : E'=0, F'=0, [ 0>=D ], cost: 1
      1: f37 -> f45 : [ C>=3 ], cost: 1
      2: f37 -> f45 : [ 1>=C ], cost: 1
      7: f37 -> f45 : C'=2, E'=1+E, G'=H, [ C==2 ], cost: 1
      3: f52 -> f52 : [], cost: 1
      4: f54 -> f57 : [], cost: 1
     12: f0 -> f13 : D'=free_18, F'=0, U'=0, [ 0>=free_18 ], cost: 1
     13: f0 -> f13 : D'=free_19, F'=0, U'=0, [ free_19>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
     11: f13 -> f13 : A'=1+A, C'=1, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, [ 0>=free_16 && B>=1+A ], cost: 1
      0: f13 -> f45 : [ A>=B ], cost: 1
      8: f13 -> f45 : H'=free_2, Q'=free_3, J'=free, K'=free_1, L'=E, M'=free_2, N'=free_2, [ free_2>=1 && B>=1+A ], cost: 1
      9: f13 -> f37 : C'=free_7, H'=free_6, Q'=free_8, J'=free_4, K'=free_5, L'=E, M'=free_6, N'=free_6, O'=free_6, P'=Q_1, Q_1'=0, R'=free_7, S'=free_7, T'=0, [ B>=1+A && 0>=free_6 && free_7>=2 ], cost: 1
     10: f13 -> f37 : C'=free_12, H'=free_11, Q'=free_13, J'=free_9, K'=free_10, L'=E, M'=free_11, N'=free_11, O'=free_11, P'=Q_1, Q_1'=0, R'=free_12, S'=free_12, T'=0, [ B>=1+A && 0>=free_11 && 0>=free_12 ], cost: 1
      5: f45 -> f52 : E'=0, [ D>=1 ], cost: 1
      6: f45 -> f52 : E'=0, F'=0, [ 0>=D ], cost: 1
      1: f37 -> f45 : [ C>=3 ], cost: 1
      2: f37 -> f45 : [ 1>=C ], cost: 1
      7: f37 -> f45 : C'=2, E'=1+E, G'=H, [ C==2 ], cost: 1
      3: f52 -> f52 : [], cost: 1
     12: f0 -> f13 : D'=free_18, F'=0, U'=0, [ 0>=free_18 ], cost: 1
     13: f0 -> f13 : D'=free_19, F'=0, U'=0, [ free_19>=1 ], cost: 1

Eliminating 1 self-loops for location f13
  Self-Loop 11 has the metering function: B-A, resulting in the new transition 14.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location f52
  Self-Loop 3 has unbounded runtime, resulting in the new transition 15.
  Removing the self-loops: 3.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     14: f13 -> [7] : A'=B, C'=1, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, [ 0>=free_16 && B>=1+A ], cost: B-A
      5: f45 -> f52 : E'=0, [ D>=1 ], cost: 1
      6: f45 -> f52 : E'=0, F'=0, [ 0>=D ], cost: 1
      1: f37 -> f45 : [ C>=3 ], cost: 1
      2: f37 -> f45 : [ 1>=C ], cost: 1
      7: f37 -> f45 : C'=2, E'=1+E, G'=H, [ C==2 ], cost: 1
     15: f52 -> [8] : [], cost: INF
     12: f0 -> f13 : D'=free_18, F'=0, U'=0, [ 0>=free_18 ], cost: 1
     13: f0 -> f13 : D'=free_19, F'=0, U'=0, [ free_19>=1 ], cost: 1
      0: [7] -> f45 : [ A>=B ], cost: 1
      8: [7] -> f45 : H'=free_2, Q'=free_3, J'=free, K'=free_1, L'=E, M'=free_2, N'=free_2, [ free_2>=1 && B>=1+A ], cost: 1
      9: [7] -> f37 : C'=free_7, H'=free_6, Q'=free_8, J'=free_4, K'=free_5, L'=E, M'=free_6, N'=free_6, O'=free_6, P'=Q_1, Q_1'=0, R'=free_7, S'=free_7, T'=0, [ B>=1+A && 0>=free_6 && free_7>=2 ], cost: 1
     10: [7] -> f37 : C'=free_12, H'=free_11, Q'=free_13, J'=free_9, K'=free_10, L'=E, M'=free_11, N'=free_11, O'=free_11, P'=Q_1, Q_1'=0, R'=free_12, S'=free_12, T'=0, [ B>=1+A && 0>=free_11 && 0>=free_12 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     21: f45 -> [8] : E'=0, [ D>=1 ], cost: INF
     22: f45 -> [8] : E'=0, F'=0, [ 0>=D ], cost: INF
     16: f0 -> [7] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     17: f0 -> [7] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
      0: [7] -> f45 : [ A>=B ], cost: 1
      8: [7] -> f45 : H'=free_2, Q'=free_3, J'=free, K'=free_1, L'=E, M'=free_2, N'=free_2, [ free_2>=1 && B>=1+A ], cost: 1
     18: [7] -> f45 : C'=free_7, H'=free_6, Q'=free_8, J'=free_4, K'=free_5, L'=E, M'=free_6, N'=free_6, O'=free_6, P'=Q_1, Q_1'=0, R'=free_7, S'=free_7, T'=0, [ B>=1+A && 0>=free_6 && free_7>=2 && free_7>=3 ], cost: 2
     19: [7] -> f45 : C'=2, E'=1+E, G'=free_6, H'=free_6, Q'=free_8, J'=free_4, K'=free_5, L'=E, M'=free_6, N'=free_6, O'=free_6, P'=Q_1, Q_1'=0, R'=free_7, S'=free_7, T'=0, [ B>=1+A && 0>=free_6 && free_7>=2 && free_7==2 ], cost: 2
     20: [7] -> f45 : C'=free_12, H'=free_11, Q'=free_13, J'=free_9, K'=free_10, L'=E, M'=free_11, N'=free_11, O'=free_11, P'=Q_1, Q_1'=0, R'=free_12, S'=free_12, T'=0, [ B>=1+A && 0>=free_11 && 0>=free_12 && 1>=free_12 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     21: f45 -> [8] : E'=0, [ D>=1 ], cost: INF
     22: f45 -> [8] : E'=0, F'=0, [ 0>=D ], cost: INF
     23: f0 -> f45 : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A
     28: f0 -> f45 : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A
     24: f0 -> [9] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     25: f0 -> [10] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     26: f0 -> [11] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     27: f0 -> [12] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     29: f0 -> [13] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     30: f0 -> [14] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     31: f0 -> [15] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     32: f0 -> [16] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A


Applied chaining over branches and pruning:
  Start location: f0
     34: f0 -> [8] : A'=B, C'=1, D'=free_18, E'=0, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A && B>=B && 0>=free_18 ], cost: INF
     35: f0 -> [8] : A'=B, C'=1, D'=free_19, E'=0, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A && B>=B && free_19>=1 ], cost: INF
     24: f0 -> [9] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     25: f0 -> [10] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     26: f0 -> [11] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     27: f0 -> [12] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     29: f0 -> [13] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     30: f0 -> [14] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     31: f0 -> [15] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     32: f0 -> [16] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     33: f0 -> [17] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A
     36: f0 -> [18] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     34: f0 -> [8] : A'=B, C'=1, D'=free_18, E'=0, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A && B>=B && 0>=free_18 ], cost: INF
     35: f0 -> [8] : A'=B, C'=1, D'=free_19, E'=0, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A && B>=B && free_19>=1 ], cost: INF
     24: f0 -> [9] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     25: f0 -> [10] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     26: f0 -> [11] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     27: f0 -> [12] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     29: f0 -> [13] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     30: f0 -> [14] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     31: f0 -> [15] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     32: f0 -> [16] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A ], cost: 1+B-A
     33: f0 -> [17] : A'=B, C'=1, D'=free_18, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ 0>=free_18 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A
     36: f0 -> [18] : A'=B, C'=1, D'=free_19, F'=0, H'=free_16, Q'=free_17, J'=free_14, K'=free_15, L'=E, M'=free_16, N'=free_16, O'=free_16, P'=Q_1, R'=1, S'=1, T'=0, U'=0, [ free_19>=1 && 0>=free_16 && B>=1+A && B>=B ], cost: 2+B-A


Computing complexity for remaining 12 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_18 && 0>=free_16 && B>=1+A && B>=B && 0>=free_18
  Final Cost:  INF

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

WORST_CASE(INF,?)