Trying to load file: main.koat

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


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

Eliminating 1 self-loops for location f47
  Self-Loop 0 has unbounded runtime, resulting in the new transition 11.
  Removing the self-loops: 0.
Eliminating 1 self-loops for location f11
  Self-Loop 9 has the metering function: B-A, resulting in the new transition 12.
  Removing the self-loops: 9.

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


Applied simple chaining:
  Start location: f0
     11: f47 -> [6] : [], cost: INF
      3: f35 -> f47 : C'=0, [ D>=3 ], cost: 1
      4: f35 -> f47 : C'=0, [ 1>=D ], cost: 1
      5: f35 -> f47 : C'=0, D'=2, E'=F, [ D==2 ], cost: 1
     10: f0 -> [7] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
      2: [7] -> f47 : C'=0, [ A>=B ], cost: 1
      6: [7] -> f47 : C'=0, F'=free_1, G'=free_2, H'=free_3, Q'=free, J'=C, K'=free_1, L'=free_1, [ free_1>=1 && B>=1+A ], cost: 1
      7: [7] -> f35 : D'=free_6, F'=free_5, G'=free_7, H'=free_8, Q'=free_4, J'=C, K'=free_5, L'=free_5, M'=free_5, N'=O, O'=0, P'=free_6, Q_1'=free_6, R'=0, [ B>=1+A && 0>=free_5 && free_6>=2 ], cost: 1
      8: [7] -> f35 : D'=free_11, F'=free_10, G'=free_12, H'=free_13, Q'=free_9, J'=C, K'=free_10, L'=free_10, M'=free_10, N'=O, O'=0, P'=free_11, Q_1'=free_11, R'=0, [ B>=1+A && 0>=free_10 && 0>=free_11 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     11: f47 -> [6] : [], cost: INF
     13: f0 -> f47 : A'=B, C'=0, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A && B>=B ], cost: 2+B-A
     14: f0 -> [8] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     15: f0 -> [9] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     16: f0 -> [10] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A


Applied simple chaining:
  Start location: f0
     13: f0 -> [6] : A'=B, C'=0, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A && B>=B ], cost: INF
     14: f0 -> [8] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     15: f0 -> [9] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     16: f0 -> [10] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     13: f0 -> [6] : A'=B, C'=0, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A && B>=B ], cost: INF
     14: f0 -> [8] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     15: f0 -> [9] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A
     16: f0 -> [10] : A'=B, D'=1, F'=free_15, G'=free_16, H'=free_17, Q'=free_14, J'=C, K'=free_15, L'=free_15, M'=free_15, N'=O, P'=1, Q_1'=1, R'=0, S'=0, T'=0, [ 0>=free_15 && B>=1+A ], cost: 1+B-A


Computing complexity for remaining 4 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_15 && B>=1+A && B>=B
  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,?)