Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f6
      0: f9 -> f9 : B'=1+B, C'=1+C, D'=free, E'=free, F'=free, [ A>=1+B && C>=0 ], cost: 1
      9: f9 -> f5 : G'=-3+C, H'=free_43, Q'=1, J'=0, K'=free_41, L'=free_44, P'=free_46, Q_1'=free_43, R'=free_42, S'=free_45, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_48, A1'=free_47, [ free_48>=free_47 && C>=2 && free_42>=1 && free_43>=1 && B>=A && D>=1 ], cost: 1
     10: f9 -> f5 : G'=-3+C, H'=free_51, Q'=1, J'=0, K'=free_49, L'=free_52, P'=free_54, Q_1'=free_51, R'=free_50, S'=free_53, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_56, A1'=free_55, [ free_56>=free_55 && C>=2 && free_50>=1 && free_51>=1 && B>=A && 0>=1+D ], cost: 1
     11: f9 -> f5 : G'=-3+C, H'=free_59, Q'=1, J'=0, K'=free_57, L'=free_60, P'=free_62, Q_1'=free_59, R'=free_58, S'=free_61, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_64, A1'=free_63, [ free_64>=free_63 && C>=2 && free_58>=1 && 0>=1+free_59 && B>=A && D>=1 ], cost: 1
     12: f9 -> f5 : G'=-3+C, H'=free_67, Q'=1, J'=0, K'=free_65, L'=free_68, P'=free_70, Q_1'=free_67, R'=free_66, S'=free_69, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_72, A1'=free_71, [ free_72>=free_71 && C>=2 && free_66>=1 && 0>=1+free_67 && B>=A && 0>=1+D ], cost: 1
     13: f9 -> f5 : G'=-3+C, H'=free_75, Q'=1, J'=0, K'=free_73, L'=free_76, P'=free_78, Q_1'=free_75, R'=free_74, S'=free_77, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_80, A1'=free_79, [ free_80>=free_79 && C>=2 && 0>=1+free_74 && free_75>=1 && B>=A && D>=1 ], cost: 1
     14: f9 -> f5 : G'=-3+C, H'=free_83, Q'=1, J'=0, K'=free_81, L'=free_84, P'=free_86, Q_1'=free_83, R'=free_82, S'=free_85, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_88, A1'=free_87, [ free_88>=free_87 && C>=2 && 0>=1+free_82 && free_83>=1 && B>=A && 0>=1+D ], cost: 1
     15: f9 -> f5 : G'=-3+C, H'=free_91, Q'=1, J'=0, K'=free_89, L'=free_92, P'=free_94, Q_1'=free_91, R'=free_90, S'=free_93, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_96, A1'=free_95, [ free_96>=free_95 && C>=2 && 0>=1+free_90 && 0>=1+free_91 && B>=A && D>=1 ], cost: 1
     16: f9 -> f5 : G'=-3+C, H'=free_99, Q'=1, J'=0, K'=free_97, L'=free_100, P'=free_102, Q_1'=free_99, R'=free_98, S'=free_101, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_104, A1'=free_103, [ free_104>=free_103 && C>=2 && 0>=1+free_98 && 0>=1+free_99 && B>=A && 0>=1+D ], cost: 1
      3: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_15, L'=free_16, N'=free_17, P'=free_13, Q_1'=R, R'=P, S'=free_14, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_17 && G>=0 && Q>=0 && P>=1 && H>=1 && J==0 ], cost: 1
      4: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_20, L'=free_21, N'=free_22, P'=free_18, Q_1'=R, R'=P, S'=free_19, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_22 && G>=0 && Q>=0 && P>=1 && 0>=1+H && J==0 ], cost: 1
      5: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_25, L'=free_26, N'=free_27, P'=free_23, Q_1'=R, R'=P, S'=free_24, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_27 && G>=0 && Q>=0 && 0>=1+P && H>=1 && J==0 ], cost: 1
      6: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_30, L'=free_31, N'=free_32, P'=free_28, Q_1'=R, R'=P, S'=free_29, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_32 && G>=0 && Q>=0 && 0>=1+P && 0>=1+H && J==0 ], cost: 1
      1: f5 -> f0 : H'=free_2, J'=H, K'=free_1, L'=free_3, M'=free_4, N'=free_6, O'=free_5, [ free_6>=1+free_4 && G>=0 && H>=1 && Q>=1 ], cost: 1
      2: f5 -> f0 : H'=free_8, J'=H, K'=free_7, L'=free_9, M'=free_10, N'=free_12, O'=free_11, [ free_12>=1+free_10 && G>=0 && 0>=1+H && Q>=1 ], cost: 1
      7: f5 -> f12 : J'=0, K'=free_33, L'=free_35, N'=free_36, P'=0, Q_1'=R, V'=Q, W'=free_34, [ M>=free_36 && G>=0 && H>=1 && Q>=0 && P==0 && J==0 ], cost: 1
      8: f5 -> f12 : J'=0, K'=free_37, L'=free_39, N'=free_40, P'=0, Q_1'=R, V'=Q, W'=free_38, [ M>=free_40 && G>=0 && 0>=1+H && Q>=0 && P==0 && J==0 ], cost: 1
     17: f6 -> f9 : A'=17, B'=1, C'=0, D'=free_106, E'=free_106, F'=free_106, Q_1'=free_105, [], cost: 1


Simplified the transitions:
  Start location: f6
      0: f9 -> f9 : B'=1+B, C'=1+C, D'=free, E'=free, F'=free, [ A>=1+B && C>=0 ], cost: 1
      9: f9 -> f5 : G'=-3+C, H'=free_43, Q'=1, J'=0, K'=free_41, L'=free_44, P'=free_46, Q_1'=free_43, R'=free_42, S'=free_45, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_48, A1'=free_47, [ free_48>=free_47 && C>=2 && free_42>=1 && free_43>=1 && B>=A && D>=1 ], cost: 1
     10: f9 -> f5 : G'=-3+C, H'=free_51, Q'=1, J'=0, K'=free_49, L'=free_52, P'=free_54, Q_1'=free_51, R'=free_50, S'=free_53, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_56, A1'=free_55, [ free_56>=free_55 && C>=2 && free_50>=1 && free_51>=1 && B>=A && 0>=1+D ], cost: 1
     11: f9 -> f5 : G'=-3+C, H'=free_59, Q'=1, J'=0, K'=free_57, L'=free_60, P'=free_62, Q_1'=free_59, R'=free_58, S'=free_61, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_64, A1'=free_63, [ free_64>=free_63 && C>=2 && free_58>=1 && 0>=1+free_59 && B>=A && D>=1 ], cost: 1
     12: f9 -> f5 : G'=-3+C, H'=free_67, Q'=1, J'=0, K'=free_65, L'=free_68, P'=free_70, Q_1'=free_67, R'=free_66, S'=free_69, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_72, A1'=free_71, [ free_72>=free_71 && C>=2 && free_66>=1 && 0>=1+free_67 && B>=A && 0>=1+D ], cost: 1
     13: f9 -> f5 : G'=-3+C, H'=free_75, Q'=1, J'=0, K'=free_73, L'=free_76, P'=free_78, Q_1'=free_75, R'=free_74, S'=free_77, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_80, A1'=free_79, [ free_80>=free_79 && C>=2 && 0>=1+free_74 && free_75>=1 && B>=A && D>=1 ], cost: 1
     14: f9 -> f5 : G'=-3+C, H'=free_83, Q'=1, J'=0, K'=free_81, L'=free_84, P'=free_86, Q_1'=free_83, R'=free_82, S'=free_85, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_88, A1'=free_87, [ free_88>=free_87 && C>=2 && 0>=1+free_82 && free_83>=1 && B>=A && 0>=1+D ], cost: 1
     15: f9 -> f5 : G'=-3+C, H'=free_91, Q'=1, J'=0, K'=free_89, L'=free_92, P'=free_94, Q_1'=free_91, R'=free_90, S'=free_93, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_96, A1'=free_95, [ free_96>=free_95 && C>=2 && 0>=1+free_90 && 0>=1+free_91 && B>=A && D>=1 ], cost: 1
     16: f9 -> f5 : G'=-3+C, H'=free_99, Q'=1, J'=0, K'=free_97, L'=free_100, P'=free_102, Q_1'=free_99, R'=free_98, S'=free_101, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_104, A1'=free_103, [ free_104>=free_103 && C>=2 && 0>=1+free_98 && 0>=1+free_99 && B>=A && 0>=1+D ], cost: 1
      3: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_15, L'=free_16, N'=free_17, P'=free_13, Q_1'=R, R'=P, S'=free_14, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_17 && G>=0 && Q>=0 && P>=1 && H>=1 && J==0 ], cost: 1
      4: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_20, L'=free_21, N'=free_22, P'=free_18, Q_1'=R, R'=P, S'=free_19, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_22 && G>=0 && Q>=0 && P>=1 && 0>=1+H && J==0 ], cost: 1
      5: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_25, L'=free_26, N'=free_27, P'=free_23, Q_1'=R, R'=P, S'=free_24, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_27 && G>=0 && Q>=0 && 0>=1+P && H>=1 && J==0 ], cost: 1
      6: f5 -> f5 : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_30, L'=free_31, N'=free_32, P'=free_28, Q_1'=R, R'=P, S'=free_29, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_32 && G>=0 && Q>=0 && 0>=1+P && 0>=1+H && J==0 ], cost: 1
     17: f6 -> f9 : A'=17, B'=1, C'=0, D'=free_106, E'=free_106, F'=free_106, Q_1'=free_105, [], cost: 1

Eliminating 1 self-loops for location f9
  Self-Loop 0 has the metering function: -B+A, resulting in the new transition 18.
  Removing the self-loops: 0.
Eliminating 4 self-loops for location f5
  Removing the self-loops: 3 4 5 6.
Adding an epsilon transition (to model nonexecution of the loops): 23.

Removed all Self-loops using metering functions (where possible):
  Start location: f6
     18: f9 -> [5] : B'=A, C'=-B+C+A, D'=free, E'=free, F'=free, [ A>=1+B && C>=0 ], cost: -B+A
     19: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_15, L'=free_16, N'=free_17, P'=free_13, Q_1'=R, R'=P, S'=free_14, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_17 && G>=0 && Q>=0 && P>=1 && H>=1 && J==0 ], cost: 1
     20: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_20, L'=free_21, N'=free_22, P'=free_18, Q_1'=R, R'=P, S'=free_19, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_22 && G>=0 && Q>=0 && P>=1 && 0>=1+H && J==0 ], cost: 1
     21: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_25, L'=free_26, N'=free_27, P'=free_23, Q_1'=R, R'=P, S'=free_24, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_27 && G>=0 && Q>=0 && 0>=1+P && H>=1 && J==0 ], cost: 1
     22: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_30, L'=free_31, N'=free_32, P'=free_28, Q_1'=R, R'=P, S'=free_29, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_32 && G>=0 && Q>=0 && 0>=1+P && 0>=1+H && J==0 ], cost: 1
     23: f5 -> [6] : [], cost: 0
     17: f6 -> f9 : A'=17, B'=1, C'=0, D'=free_106, E'=free_106, F'=free_106, Q_1'=free_105, [], cost: 1
      9: [5] -> f5 : G'=-3+C, H'=free_43, Q'=1, J'=0, K'=free_41, L'=free_44, P'=free_46, Q_1'=free_43, R'=free_42, S'=free_45, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_48, A1'=free_47, [ free_48>=free_47 && C>=2 && free_42>=1 && free_43>=1 && B>=A && D>=1 ], cost: 1
     10: [5] -> f5 : G'=-3+C, H'=free_51, Q'=1, J'=0, K'=free_49, L'=free_52, P'=free_54, Q_1'=free_51, R'=free_50, S'=free_53, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_56, A1'=free_55, [ free_56>=free_55 && C>=2 && free_50>=1 && free_51>=1 && B>=A && 0>=1+D ], cost: 1
     11: [5] -> f5 : G'=-3+C, H'=free_59, Q'=1, J'=0, K'=free_57, L'=free_60, P'=free_62, Q_1'=free_59, R'=free_58, S'=free_61, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_64, A1'=free_63, [ free_64>=free_63 && C>=2 && free_58>=1 && 0>=1+free_59 && B>=A && D>=1 ], cost: 1
     12: [5] -> f5 : G'=-3+C, H'=free_67, Q'=1, J'=0, K'=free_65, L'=free_68, P'=free_70, Q_1'=free_67, R'=free_66, S'=free_69, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_72, A1'=free_71, [ free_72>=free_71 && C>=2 && free_66>=1 && 0>=1+free_67 && B>=A && 0>=1+D ], cost: 1
     13: [5] -> f5 : G'=-3+C, H'=free_75, Q'=1, J'=0, K'=free_73, L'=free_76, P'=free_78, Q_1'=free_75, R'=free_74, S'=free_77, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_80, A1'=free_79, [ free_80>=free_79 && C>=2 && 0>=1+free_74 && free_75>=1 && B>=A && D>=1 ], cost: 1
     14: [5] -> f5 : G'=-3+C, H'=free_83, Q'=1, J'=0, K'=free_81, L'=free_84, P'=free_86, Q_1'=free_83, R'=free_82, S'=free_85, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_88, A1'=free_87, [ free_88>=free_87 && C>=2 && 0>=1+free_82 && free_83>=1 && B>=A && 0>=1+D ], cost: 1
     15: [5] -> f5 : G'=-3+C, H'=free_91, Q'=1, J'=0, K'=free_89, L'=free_92, P'=free_94, Q_1'=free_91, R'=free_90, S'=free_93, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_96, A1'=free_95, [ free_96>=free_95 && C>=2 && 0>=1+free_90 && 0>=1+free_91 && B>=A && D>=1 ], cost: 1
     16: [5] -> f5 : G'=-3+C, H'=free_99, Q'=1, J'=0, K'=free_97, L'=free_100, P'=free_102, Q_1'=free_99, R'=free_98, S'=free_101, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_104, A1'=free_103, [ free_104>=free_103 && C>=2 && 0>=1+free_98 && 0>=1+free_99 && B>=A && 0>=1+D ], cost: 1


Applied simple chaining:
  Start location: f6
     19: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_15, L'=free_16, N'=free_17, P'=free_13, Q_1'=R, R'=P, S'=free_14, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_17 && G>=0 && Q>=0 && P>=1 && H>=1 && J==0 ], cost: 1
     20: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_20, L'=free_21, N'=free_22, P'=free_18, Q_1'=R, R'=P, S'=free_19, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_22 && G>=0 && Q>=0 && P>=1 && 0>=1+H && J==0 ], cost: 1
     21: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_25, L'=free_26, N'=free_27, P'=free_23, Q_1'=R, R'=P, S'=free_24, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_27 && G>=0 && Q>=0 && 0>=1+P && H>=1 && J==0 ], cost: 1
     22: f5 -> [6] : G'=-1+G, H'=R, Q'=1+Q, J'=0, K'=free_30, L'=free_31, N'=free_32, P'=free_28, Q_1'=R, R'=P, S'=free_29, T'=1+Q, U'=-1+G, V'=Q, [ M>=free_32 && G>=0 && Q>=0 && 0>=1+P && 0>=1+H && J==0 ], cost: 1
     23: f5 -> [6] : [], cost: 0
     17: f6 -> [5] : A'=17, B'=17, C'=16, D'=free, E'=free, F'=free, Q_1'=free_105, [ 17>=2 && 0>=0 ], cost: 17
      9: [5] -> f5 : G'=-3+C, H'=free_43, Q'=1, J'=0, K'=free_41, L'=free_44, P'=free_46, Q_1'=free_43, R'=free_42, S'=free_45, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_48, A1'=free_47, [ free_48>=free_47 && C>=2 && free_42>=1 && free_43>=1 && B>=A && D>=1 ], cost: 1
     10: [5] -> f5 : G'=-3+C, H'=free_51, Q'=1, J'=0, K'=free_49, L'=free_52, P'=free_54, Q_1'=free_51, R'=free_50, S'=free_53, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_56, A1'=free_55, [ free_56>=free_55 && C>=2 && free_50>=1 && free_51>=1 && B>=A && 0>=1+D ], cost: 1
     11: [5] -> f5 : G'=-3+C, H'=free_59, Q'=1, J'=0, K'=free_57, L'=free_60, P'=free_62, Q_1'=free_59, R'=free_58, S'=free_61, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_64, A1'=free_63, [ free_64>=free_63 && C>=2 && free_58>=1 && 0>=1+free_59 && B>=A && D>=1 ], cost: 1
     12: [5] -> f5 : G'=-3+C, H'=free_67, Q'=1, J'=0, K'=free_65, L'=free_68, P'=free_70, Q_1'=free_67, R'=free_66, S'=free_69, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_72, A1'=free_71, [ free_72>=free_71 && C>=2 && free_66>=1 && 0>=1+free_67 && B>=A && 0>=1+D ], cost: 1
     13: [5] -> f5 : G'=-3+C, H'=free_75, Q'=1, J'=0, K'=free_73, L'=free_76, P'=free_78, Q_1'=free_75, R'=free_74, S'=free_77, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_80, A1'=free_79, [ free_80>=free_79 && C>=2 && 0>=1+free_74 && free_75>=1 && B>=A && D>=1 ], cost: 1
     14: [5] -> f5 : G'=-3+C, H'=free_83, Q'=1, J'=0, K'=free_81, L'=free_84, P'=free_86, Q_1'=free_83, R'=free_82, S'=free_85, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_88, A1'=free_87, [ free_88>=free_87 && C>=2 && 0>=1+free_82 && free_83>=1 && B>=A && 0>=1+D ], cost: 1
     15: [5] -> f5 : G'=-3+C, H'=free_91, Q'=1, J'=0, K'=free_89, L'=free_92, P'=free_94, Q_1'=free_91, R'=free_90, S'=free_93, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_96, A1'=free_95, [ free_96>=free_95 && C>=2 && 0>=1+free_90 && 0>=1+free_91 && B>=A && D>=1 ], cost: 1
     16: [5] -> f5 : G'=-3+C, H'=free_99, Q'=1, J'=0, K'=free_97, L'=free_100, P'=free_102, Q_1'=free_99, R'=free_98, S'=free_101, T'=1, U'=-3+C, W'=D, X'=D, Y'=-2+C, Z'=free_104, A1'=free_103, [ free_104>=free_103 && C>=2 && 0>=1+free_98 && 0>=1+free_99 && B>=A && 0>=1+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f6
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f6
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

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

WORST_CASE(Omega(1),?)