Trying to load file: main.koat

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


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

Eliminating 1 self-loops for location f49
  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: f49 -> [6] : [], cost: INF
     12: f11 -> [7] : A'=B, E'=1, G'=free_15, H'=free_16, Q'=free_17, J'=free_14, K'=D, L'=free_15, M'=free_15, N'=free_15, O'=P, Q_1'=1, R'=1, S'=0, [ 0>=free_15 && B>=1+A ], cost: B-A
      3: f35 -> f49 : C'=0, D'=0, [ E>=3 ], cost: 1
      4: f35 -> f49 : C'=0, D'=0, [ 1>=E ], cost: 1
      5: f35 -> f49 : C'=0, D'=0, E'=2, F'=G, [ E==2 ], cost: 1
     10: f0 -> f11 : C'=0, T'=0, [], cost: 1
      2: [7] -> f49 : C'=0, D'=0, [ A>=B ], cost: 1
      6: [7] -> f49 : C'=0, D'=0, G'=free_1, H'=free_2, Q'=free_3, J'=free, K'=D, L'=free_1, M'=free_1, [ free_1>=1 && B>=1+A ], cost: 1
      7: [7] -> f35 : E'=free_6, G'=free_5, H'=free_7, Q'=free_8, J'=free_4, K'=D, L'=free_5, M'=free_5, N'=free_5, O'=P, P'=0, Q_1'=free_6, R'=free_6, S'=0, [ B>=1+A && 0>=free_5 && free_6>=2 ], cost: 1
      8: [7] -> f35 : E'=free_11, G'=free_10, H'=free_12, Q'=free_13, J'=free_9, K'=D, L'=free_10, M'=free_10, N'=free_10, O'=P, P'=0, Q_1'=free_11, R'=free_11, S'=0, [ B>=1+A && 0>=free_10 && 0>=free_11 ], cost: 1


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


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