Trying to load file: main.koat

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


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


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


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