Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f8
      0: f12 -> f12 : B'=free, C'=free_1, D'=E, F'=G, H'=A, [ A>=0 && free>=2 ], cost: 1
      5: f12 -> f9 : B'=free_45, C'=0, E'=0, T'=free_47, U'=free_41, V'=free_43, W'=free_46, X'=free_40, Z'=free_42, A1'=free_44, [ free_48>=2 && free_49>=2 && A>=0 && free_45>=2 && E==0 && C==0 ], cost: 1
      4: f1 -> f12 : B'=free_36, C'=free_38, E'=K, Q'=free_37, J'=free_33, K'=free_29, L'=free_28, M'=free_35, Q_1'=free_32, Y'=free_31, Z'=free_34, B1'=free_30, [ J>=Q && J>=0 && free_39>=2 && free_33>=free_39 && free_33>=0 && free_36>=2 && free_30>=free_36 ], cost: 1
      1: f1 -> f1 : J'=1+J, K'=L, L'=free_2, M'=L, N'=free_3, O'=J, [ Q>=1+J && J>=0 ], cost: 1
      2: f8 -> f1 : B'=free_6, Q'=free_6, J'=2, K'=free_4, L'=free_5, M'=free_4, P'=free_8, Q_1'=free_4, R'=free_7, S'=2, [ free_6>=2 ], cost: 1
      3: f8 -> f9 : B'=free_20, C'=0, E'=0, Q'=free_9, J'=free_15, K'=free_14, L'=free_12, M'=free_23, P'=free_19, Q_1'=free_18, T'=free_22, U'=free_11, V'=free_16, W'=free_21, X'=free_10, Y'=free_17, Z'=free_24, A1'=free_13, [ 0>=free_25 && 0>=free_26 && 0>=free_20 && 0>=free_27 ], cost: 1
      6: f8 -> f9 : B'=1, C'=free_51, E'=0, Q'=free_50, J'=free_56, K'=free_55, L'=free_53, M'=free_64, P'=free_60, Q_1'=free_59, T'=free_61, U'=free_63, V'=free_52, W'=free_57, X'=free_62, Y'=free_58, Z'=free_65, A1'=free_54, [ L==0 ], cost: 1


Simplified the transitions:
  Start location: f8
      0: f12 -> f12 : B'=free, C'=free_1, D'=E, F'=G, H'=A, [ A>=0 && free>=2 ], cost: 1
      4: f1 -> f12 : B'=free_36, C'=free_38, E'=K, Q'=free_37, J'=free_33, K'=free_29, L'=free_28, M'=free_35, Q_1'=free_32, Y'=free_31, Z'=free_34, B1'=free_30, [ J>=Q && J>=0 && free_33>=0 && free_36>=2 && free_30>=free_36 && 2<=free_33 ], cost: 1
      1: f1 -> f1 : J'=1+J, K'=L, L'=free_2, M'=L, N'=free_3, O'=J, [ Q>=1+J && J>=0 ], cost: 1
      2: f8 -> f1 : B'=free_6, Q'=free_6, J'=2, K'=free_4, L'=free_5, M'=free_4, P'=free_8, Q_1'=free_4, R'=free_7, S'=2, [ free_6>=2 ], cost: 1

Eliminating 1 self-loops for location f12
  Self-Loop 0 has unbounded runtime, resulting in the new transition 7.
  Removing the self-loops: 0.
Eliminating 1 self-loops for location f1
  Self-Loop 1 has the metering function: Q-J, resulting in the new transition 8.
  Removing the self-loops: 1.

Removed all Self-loops using metering functions (where possible):
  Start location: f8
      7: f12 -> [4] : [ A>=0 && free>=2 ], cost: INF
      8: f1 -> [5] : J'=Q, K'=free_2, L'=free_2, M'=free_2, N'=free_3, O'=-1+Q, [ Q>=1+J && J>=0 ], cost: Q-J
      2: f8 -> f1 : B'=free_6, Q'=free_6, J'=2, K'=free_4, L'=free_5, M'=free_4, P'=free_8, Q_1'=free_4, R'=free_7, S'=2, [ free_6>=2 ], cost: 1
      4: [5] -> f12 : B'=free_36, C'=free_38, E'=K, Q'=free_37, J'=free_33, K'=free_29, L'=free_28, M'=free_35, Q_1'=free_32, Y'=free_31, Z'=free_34, B1'=free_30, [ J>=Q && J>=0 && free_33>=0 && free_36>=2 && free_30>=free_36 && 2<=free_33 ], cost: 1


Applied simple chaining:
  Start location: f8
      2: f8 -> [4] : B'=free_36, C'=free_38, E'=free_2, Q'=free_37, J'=free_33, K'=free_29, L'=free_28, M'=free_35, N'=free_3, O'=-1+free_6, P'=free_8, Q_1'=free_32, R'=free_7, S'=2, Y'=free_31, Z'=free_34, B1'=free_30, [ free_6>=2 && free_6>=3 && 2>=0 && free_6>=free_6 && free_6>=0 && free_33>=0 && free_36>=2 && free_30>=free_36 && 2<=free_33 && A>=0 && free>=2 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f8
      2: f8 -> [4] : B'=free_36, C'=free_38, E'=free_2, Q'=free_37, J'=free_33, K'=free_29, L'=free_28, M'=free_35, N'=free_3, O'=-1+free_6, P'=free_8, Q_1'=free_32, R'=free_7, S'=2, Y'=free_31, Z'=free_34, B1'=free_30, [ free_6>=2 && free_6>=3 && 2>=0 && free_6>=free_6 && free_6>=0 && free_33>=0 && free_36>=2 && free_30>=free_36 && 2<=free_33 && A>=0 && free>=2 ], cost: INF


Computing complexity for remaining 1 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_6>=2 && free_6>=3 && 2>=0 && free_6>=free_6 && free_6>=0 && free_33>=0 && free_36>=2 && free_30>=free_36 && 2<=free_33 && A>=0 && free>=2
  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,?)