Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f9
      0: f12 -> f116 : C'=1, D'=-1, E'=F, G'=free_1, H'=1+F, Q'=free, J'=free_1, [ A>=2 && free_2>=A && B>=0 && C==1 ], cost: 1
     10: f116 -> f116 : C'=1+C, F'=-1+F, O'=F, P'=1, M1'=U, N1'=1+C, O1'=-1+F, [ A>=2 && C>=0 && F>=0 && P==0 && U==M1 ], cost: 1
      2: f116 -> f300 : P'=1, [ F>=O && P==1 ], cost: 1
     11: f116 -> f8 : C'=1+E1, O'=F, P'=1, U'=0, B1'=E1, C1'=V, D1'=V, G1'=0, H1'=V, Q1'=0, J1'=V, L1'=-1, P1'=free_33, [ free_33>=0 && A>=2 && C>=0 && F>=0 && U==0 && P==0 ], cost: 1
      1: f13 -> f116 : C'=2, E'=free_6, F'=-1+free_6, J'=free_3, K'=2, L'=-1, M'=free_5, N'=free_4, [ E>=0 && A>=2 ], cost: 1
      9: f13 -> f8 : C'=1+E1, E'=0, U'=0, B1'=E1, C1'=V, D1'=V, G1'=0, H1'=V, Q1'=0, J1'=V, L1'=-1, [ A>=2 && U==0 && E==0 && C==1 ], cost: 1
      4: f1 -> f116 : B'=free_15, C'=0, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=R, V'=R, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, [ A>=2 && free_14>=A && F>=A && B>=Q_1 && B>=0 && C==0 ], cost: 1
      3: f1 -> f1 : B'=1+B, R'=S, S'=free_7, T'=S, [ B>=0 && Q_1>=1+B ], cost: 1
      5: f7 -> f8 : B1'=free_17, C1'=D1, E1'=-1+free_17, F1'=-1, [ B1>=0 ], cost: 1
      6: f7 -> f10 : Y'=free_20, C1'=free_23, D1'=free_18, G1'=free_21, H1'=free_24, Q1'=free_19, J1'=free_22, [ B1>=0 && G1==D1 ], cost: 1
      7: f8 -> f8 : U'=0, V'=H1, C1'=D1, E1'=-1+E1, G1'=0, Q1'=0, J1'=H1, K1'=-1+E1, [ E1>=0 && A>=2 && Q1==0 && H1==V && G1==0 && U==0 && J1==V ], cost: 1
      8: f8 -> f10 : A'=free_27, Y'=free_30, C1'=free_32, D1'=free_25, G1'=free_28, H1'=free_31, Q1'=free_26, J1'=free_29, [ E1>=0 && G1==D1 ], cost: 1
     12: f9 -> f1 : A'=free_39, B'=2, P'=0, Q_1'=free_39, R'=S, S'=free_37, T'=S, W'=S, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W ], cost: 1
     13: f9 -> f10 : A'=free_51, B'=free_45, P'=0, Q_1'=free_52, R'=free_44, S'=free_43, T'=free_50, U'=0, V'=0, W'=free_49, X'=free_54, Y'=free_42, C1'=free_47, D1'=free_40, G1'=free_46, H1'=free_53, Q1'=free_41, J1'=free_48, R1'=free_55, [ 0>=free_51 ], cost: 1
     14: f9 -> f10 : A'=1, B'=free_62, P'=0, Q_1'=free_61, R'=free_68, S'=free_67, T'=free_60, U'=0, V'=0, W'=free_59, X'=free_65, Y'=free_71, C1'=free_63, D1'=free_56, G1'=free_64, H1'=free_72, Q1'=free_58, J1'=free_66, Q1_1'=free_74, R1'=free_70, S1'=free_73, V1'=free_69, W1'=free_74, X1'=free_57, [ S==0 && W==0 ], cost: 1


Simplified the transitions:
  Start location: f9
     10: f116 -> f116 : C'=1+C, F'=-1+F, O'=F, P'=1, M1'=U, N1'=1+C, O1'=-1+F, [ A>=2 && C>=0 && F>=0 && P==0 && U==M1 ], cost: 1
     11: f116 -> f8 : C'=1+E1, O'=F, P'=1, U'=0, B1'=E1, C1'=V, D1'=V, G1'=0, H1'=V, Q1'=0, J1'=V, L1'=-1, P1'=free_33, [ free_33>=0 && A>=2 && C>=0 && F>=0 && U==0 && P==0 ], cost: 1
      4: f1 -> f116 : B'=free_15, C'=0, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=R, V'=R, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, [ A>=2 && free_14>=A && F>=A && B>=Q_1 && B>=0 && C==0 ], cost: 1
      3: f1 -> f1 : B'=1+B, R'=S, S'=free_7, T'=S, [ B>=0 && Q_1>=1+B ], cost: 1
      7: f8 -> f8 : U'=0, V'=H1, C1'=D1, E1'=-1+E1, G1'=0, Q1'=0, J1'=H1, K1'=-1+E1, [ E1>=0 && A>=2 && Q1==0 && H1==V && G1==0 && U==0 && J1==V ], cost: 1
     12: f9 -> f1 : A'=free_39, B'=2, P'=0, Q_1'=free_39, R'=S, S'=free_37, T'=S, W'=S, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W ], cost: 1

Eliminating 1 self-loops for location f116
  Self-Loop 10 has the metering function: -P, resulting in the new transition 15.
  Removing the self-loops: 10.
Eliminating 1 self-loops for location f1
  Self-Loop 3 has the metering function: Q_1-B, resulting in the new transition 16.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f8
  Self-Loop 7 has the metering function: 1+E1, resulting in the new transition 17.
  Removing the self-loops: 7.

Removed all Self-loops using metering functions (where possible):
  Start location: f9
     15: f116 -> [9] : C'=C-P, F'=F+P, O'=1+F+P, P'=1, M1'=U, N1'=C-P, O1'=F+P, [ A>=2 && C>=0 && F>=0 && P==0 && U==M1 ], cost: -P
     16: f1 -> [10] : B'=Q_1, R'=free_7, S'=free_7, T'=free_7, [ B>=0 && Q_1>=1+B ], cost: Q_1-B
     17: f8 -> [11] : U'=0, V'=H1, C1'=D1, E1'=-1, G1'=0, Q1'=0, J1'=H1, K1'=-1, [ E1>=0 && A>=2 && Q1==0 && H1==V && G1==0 && U==0 && J1==V ], cost: 1+E1
     12: f9 -> f1 : A'=free_39, B'=2, P'=0, Q_1'=free_39, R'=S, S'=free_37, T'=S, W'=S, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W ], cost: 1
     11: [9] -> f8 : C'=1+E1, O'=F, P'=1, U'=0, B1'=E1, C1'=V, D1'=V, G1'=0, H1'=V, Q1'=0, J1'=V, L1'=-1, P1'=free_33, [ free_33>=0 && A>=2 && C>=0 && F>=0 && U==0 && P==0 ], cost: 1
      4: [10] -> f116 : B'=free_15, C'=0, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=R, V'=R, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, [ A>=2 && free_14>=A && F>=A && B>=Q_1 && B>=0 && C==0 ], cost: 1


Applied simple chaining:
  Start location: f9
     12: f9 -> [9] : A'=free_39, B'=free_15, C'=0, F'=F, O'=1+F, P'=1, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=free_7, V'=free_7, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, M1'=free_7, N1'=0, O1'=F, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W && 2>=0 && free_39>=3 && free_39>=2 && free_14>=free_39 && F>=free_39 && free_39>=free_39 && free_39>=0 && C==0 && free_39>=2 && 0>=0 && F>=0 && 0==0 && free_7==M1 ], cost: free_39
     11: [9] -> [11] : C'=1+E1, O'=F, P'=1, U'=0, V'=V, B1'=E1, C1'=V, D1'=V, E1'=-1, G1'=0, H1'=V, Q1'=0, J1'=V, K1'=-1, L1'=-1, P1'=free_33, [ free_33>=0 && A>=2 && C>=0 && F>=0 && U==0 && P==0 && E1>=0 && A>=2 && 0==0 && V==V && 0==0 && 0==0 && V==V ], cost: 2+E1


Applied chaining over branches and pruning:
  Start location: f9
     18: f9 -> [12] : A'=free_39, B'=free_15, C'=0, F'=F, O'=1+F, P'=1, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=free_7, V'=free_7, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, M1'=free_7, N1'=0, O1'=F, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W && 2>=0 && free_39>=3 && free_39>=2 && free_14>=free_39 && F>=free_39 && free_39>=free_39 && free_39>=0 && C==0 && free_39>=2 && 0>=0 && F>=0 && 0==0 && free_7==M1 ], cost: free_39


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f9
     18: f9 -> [12] : A'=free_39, B'=free_15, C'=0, F'=F, O'=1+F, P'=1, Q_1'=free_9, R'=free_12, S'=free_8, T'=free_11, U'=free_7, V'=free_7, W'=free_10, X'=free_13, Y'=free_16, Z'=free_15, A1'=free_14, M1'=free_7, N1'=0, O1'=F, Q1_1'=free_35, R1'=free_38, S1'=free_34, T1'=2, U1'=free_36, [ free_39>=2 && S==W && 2>=0 && free_39>=3 && free_39>=2 && free_14>=free_39 && F>=free_39 && free_39>=free_39 && free_39>=0 && C==0 && free_39>=2 && 0>=0 && F>=0 && 0==0 && free_7==M1 ], cost: free_39


Computing complexity for remaining 1 transitions.

  Found configuration with infinitely models for cost: free_39
  and guard: free_39>=2 && S==W && 2>=0 && free_39>=3 && free_39>=2 && free_14>=free_39 && F>=free_39 && free_39>=free_39 && free_39>=0 && C==0 && free_39>=2 && 0>=0 && F>=0 && 0==0 && free_7==M1:
  free_14: Pos, F: Pos, C: Both, S: Both, M1: Both, free_39: Const, W: Both, free_7: Both

Found new complexity const, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free_39>=2 && S==W && 2>=0 && free_39>=3 && free_39>=2 && free_14>=free_39 && F>=free_39 && free_39>=free_39 && free_39>=0 && C==0 && free_39>=2 && 0>=0 && F>=0 && 0==0 && free_7==M1
  Final Cost:  3

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: const
  Complexity value: 0

WORST_CASE(Omega(1),?)