Trying to load file: main.koat

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


Simplified the transitions:
  Start location: f300
      0: f300 -> f1 : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [], cost: 1
      1: f1 -> f1 : H'=256, Q'=free_8, J'=free_11, K'=free_5, L'=free_7, M'=free_10, N'=free_6, O'=free_9, P'=free_12, [ 1+F==G && H==256 ], cost: 1
      2: f1 -> f1 : Q'=free_17, J'=free_20, K'=free_14, L'=free_16, M'=free_19, N'=free_15, O'=free_18, [ 0>=H && 1+F==G ], cost: 1
      3: f1 -> f1 : Q'=free_24, J'=free_27, K'=free_21, L'=free_23, M'=free_26, N'=free_22, O'=free_25, P'=free_28, Q_1'=256, [ G>=2+F && Q_1==256 ], cost: 1
      4: f1 -> f1 : Q'=free_33, J'=free_36, K'=free_30, L'=free_32, M'=free_35, N'=free_31, O'=free_34, [ 0>=Q_1 && G>=2+F ], cost: 1

Eliminating 4 self-loops for location f1
  Self-Loop 1 has unbounded runtime, resulting in the new transition 10.
  Self-Loop 2 has unbounded runtime, resulting in the new transition 11.
  Self-Loop 3 has unbounded runtime, resulting in the new transition 12.
  Self-Loop 4 has unbounded runtime, resulting in the new transition 13.
  Removing the self-loops: 1 2 3 4.

Removed all Self-loops using metering functions (where possible):
  Start location: f300
      0: f300 -> f1 : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [], cost: 1
     10: f1 -> [4] : [ 1+F==G && H==256 ], cost: INF
     11: f1 -> [4] : [ 0>=H && 1+F==G ], cost: INF
     12: f1 -> [4] : [ G>=2+F && Q_1==256 ], cost: INF
     13: f1 -> [4] : [ 0>=Q_1 && G>=2+F ], cost: INF


Applied chaining over branches and pruning:
  Start location: f300
     14: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 1+F==G && H==256 ], cost: INF
     15: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 0>=H && 1+F==G ], cost: INF
     16: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ G>=2+F && Q_1==256 ], cost: INF
     17: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 0>=Q_1 && G>=2+F ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f300
     14: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 1+F==G && H==256 ], cost: INF
     15: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 0>=H && 1+F==G ], cost: INF
     16: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ G>=2+F && Q_1==256 ], cost: INF
     17: f300 -> [4] : A'=free_2, B'=free_4, C'=free, D'=free_1, E'=free_3, [ 0>=Q_1 && G>=2+F ], cost: INF


Computing complexity for remaining 4 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 1+F==G && H==256
  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,?)