Trying to load file: main.koat

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


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

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

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


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


Applied chaining over branches and pruning:
  Start location: f0
     19: f45 -> [8] : D'=0, E'=free, [ 0>=free ], cost: INF
     20: f45 -> [8] : D'=0, E'=free_1, F'=0, [ free_1>=1 ], cost: INF
     15: f0 -> f45 : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A && B>=B ], cost: 2+B-A
     16: f0 -> [9] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     17: f0 -> [10] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     18: f0 -> [11] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A


Applied chaining over branches and pruning:
  Start location: f0
     21: f0 -> [8] : A'=B, C'=1, D'=0, E'=free, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A && B>=B && 0>=free ], cost: INF
     22: f0 -> [8] : A'=B, C'=1, D'=0, E'=free_1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A && B>=B && free_1>=1 ], cost: INF
     16: f0 -> [9] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     17: f0 -> [10] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     18: f0 -> [11] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     21: f0 -> [8] : A'=B, C'=1, D'=0, E'=free, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A && B>=B && 0>=free ], cost: INF
     22: f0 -> [8] : A'=B, C'=1, D'=0, E'=free_1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A && B>=B && free_1>=1 ], cost: INF
     16: f0 -> [9] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     17: f0 -> [10] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A
     18: f0 -> [11] : A'=B, C'=1, F'=0, H'=free_18, Q'=free_17, J'=free_19, K'=free_16, L'=D, M'=free_18, N'=free_18, O'=free_18, P'=free_18, Q_1'=R, S'=1, T'=1, U'=1, V'=0, W'=0, [ 0>=free_18 && B>=1+A ], cost: 1+B-A


Computing complexity for remaining 5 transitions.

Found new complexity INF, because: INF sat.


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