Trying to load file: main.koat Initial Control flow graph problem: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 14: f1 -> f10 : A'=free_79, B'=free_78, C'=free_85, D'=free_80, E'=free_87, J'=C, K'=T, L'=N, M'=N, O'=free_86, P'=C, Q_1'=C, R'=C, S'=free_84, Z'=free_82, A1'=free_81, B1'=free_77, D1'=1+T, E1'=Q, F1'=free_83, [ B>=A && B>=0 && free_89>=free_86 && free_88>=2 && free_78>=free_88 && C>=1+N && free_78>=0 && free_86>=2 && N>=1+C ], cost: 1 15: f1 -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, J'=C, K'=T, L'=N, M'=N, O'=free_99, P'=C, Q_1'=C, R'=C, S'=free_97, Z'=free_95, A1'=free_94, B1'=free_90, D1'=1+T, E1'=Q, F1'=free_96, [ B>=A && B>=0 && free_102>=free_99 && free_101>=2 && free_91>=free_101 && C>=1+N && free_91>=0 && free_99>=2 ], cost: 1 16: f1 -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, J'=C, K'=T, L'=N, M'=N, O'=free_112, P'=C, Q_1'=C, R'=C, S'=free_110, Z'=free_108, A1'=free_107, B1'=free_103, D1'=1+T, E1'=Q, F1'=free_109, [ B>=A && B>=0 && free_115>=free_112 && free_114>=2 && free_104>=free_114 && N>=1+C && free_104>=0 && free_112>=2 ], cost: 1 17: f1 -> f10 : A'=free_118, B'=free_117, C'=free_124, D'=free_119, E'=free_126, J'=C, K'=T, L'=N, M'=N, O'=free_125, P'=C, Q_1'=C, R'=C, S'=free_123, Z'=free_121, A1'=free_120, B1'=free_116, D1'=1+T, E1'=Q, F1'=free_122, [ B>=A && B>=0 && free_128>=free_125 && free_127>=2 && free_117>=free_127 && N>=1+C && free_117>=0 && free_125>=2 && C>=1+N ], cost: 1 1: f9 -> f10 : L'=M, N'=M, O'=free_3, P'=free_2, Q_1'=free_2, R'=J, [ free_4>=1+J && K>=0 && free_2>=1+free_4 && free_3>=2 ], cost: 1 2: f9 -> f10 : L'=M, N'=M, O'=free_6, P'=free_5, Q_1'=free_5, R'=J, [ free_7>=1+J && K>=0 && free_7>=1+free_5 && free_6>=2 ], cost: 1 3: f9 -> f10 : L'=M, N'=M, O'=free_9, P'=free_8, Q_1'=free_8, R'=J, [ J>=1+free_10 && K>=0 && free_8>=1+free_10 && free_9>=2 ], cost: 1 4: f9 -> f10 : L'=M, N'=M, O'=free_12, P'=free_11, Q_1'=free_11, R'=J, [ J>=1+free_13 && K>=0 && free_13>=1+free_11 && free_12>=2 ], cost: 1 5: f9 -> f4 : J'=free_19, L'=free_21, M'=free_17, O'=free_16, P'=free_20, Q_1'=free_15, R'=free_14, S'=free_18, [ K>=0 && free_21>=1+free_20 && free_16>=2 && M==J ], cost: 1 6: f9 -> f4 : J'=free_27, L'=free_29, M'=free_25, O'=free_24, P'=free_28, Q_1'=free_23, R'=free_22, S'=free_26, [ K>=0 && free_28>=1+free_29 && free_24>=2 && M==J ], cost: 1 7: f10 -> f10 : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1+T, U'=free_31, V'=Q, W'=-1+T, [ free_33>=1+J && T>=0 && free_30>=1+free_33 && free_32>=2 ], cost: 1 8: f10 -> f10 : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1+T, U'=free_35, V'=Q, W'=-1+T, [ free_37>=1+J && T>=0 && free_37>=1+free_34 && free_36>=2 ], cost: 1 9: f10 -> f10 : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1+T, U'=free_39, V'=Q, W'=-1+T, [ J>=1+free_41 && T>=0 && free_38>=1+free_41 && free_40>=2 ], cost: 1 10: f10 -> f10 : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1+T, U'=free_43, V'=Q, W'=-1+T, [ J>=1+free_45 && T>=0 && free_45>=1+free_42 && free_44>=2 ], cost: 1 11: f10 -> f4 : J'=free_46, M'=free_50, O'=free_51, Q_1'=free_49, R'=free_48, S'=free_47, [ free_51>=2 && T>=0 && M==J ], cost: 1 13: f3 -> f1 : A'=free_75, B'=2, C'=free_70, D'=free_72, E'=free_70, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 ], cost: 1 12: f3 -> f4 : A'=free_63, B'=free_62, C'=free_58, D'=free_67, E'=free_60, J'=free_65, L'=X, M'=free_61, N'=X, O'=free_59, P'=X, Q_1'=free_57, R'=free_55, S'=free_66, X'=free_64, Y'=free_54, Z'=free_53, A1'=free_52, B1'=free_56, [ 0>=free_68 && 0>=free_59 && 0>=free_69 ], cost: 1 18: f3 -> f4 : A'=free_141, B'=free_140, C'=free_136, D'=free_145, E'=free_138, J'=free_132, L'=free_142, M'=free_143, N'=D, O'=1, P'=free_134, Q_1'=free_139, R'=free_135, S'=free_144, X'=free_131, Y'=free_137, Z'=free_130, A1'=free_129, B1'=free_133, [ 0>=1 && free_142>=1+free_134 ], cost: 1 19: f3 -> f4 : A'=free_158, B'=free_157, C'=free_153, D'=free_162, E'=free_155, J'=free_149, L'=free_159, M'=free_160, N'=D, O'=1, P'=free_151, Q_1'=free_156, R'=free_152, S'=free_161, X'=free_148, Y'=free_154, Z'=free_147, A1'=free_146, B1'=free_150, [ 0>=1 && free_151>=1+free_159 ], cost: 1 20: f3 -> f4 : A'=free_175, B'=free_174, C'=free_170, D'=free_179, E'=free_172, J'=free_166, L'=free_176, M'=free_177, N'=D, O'=1, P'=free_168, Q_1'=free_173, R'=free_169, S'=free_178, X'=free_165, Y'=free_171, Z'=free_164, A1'=free_163, B1'=free_167, [ 0>=1 && free_176>=1+free_168 ], cost: 1 21: f3 -> f4 : A'=free_192, B'=free_191, C'=free_187, D'=free_196, E'=free_189, J'=free_183, L'=free_193, M'=free_194, N'=D, O'=1, P'=free_185, Q_1'=free_190, R'=free_186, S'=free_195, X'=free_182, Y'=free_188, Z'=free_181, A1'=free_180, B1'=free_184, [ 0>=1 && free_185>=1+free_193 ], cost: 1 Removed unsatisfiable initial transitions: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 14: f1 -> f10 : A'=free_79, B'=free_78, C'=free_85, D'=free_80, E'=free_87, J'=C, K'=T, L'=N, M'=N, O'=free_86, P'=C, Q_1'=C, R'=C, S'=free_84, Z'=free_82, A1'=free_81, B1'=free_77, D1'=1+T, E1'=Q, F1'=free_83, [ B>=A && B>=0 && free_89>=free_86 && free_88>=2 && free_78>=free_88 && C>=1+N && free_78>=0 && free_86>=2 && N>=1+C ], cost: 1 15: f1 -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, J'=C, K'=T, L'=N, M'=N, O'=free_99, P'=C, Q_1'=C, R'=C, S'=free_97, Z'=free_95, A1'=free_94, B1'=free_90, D1'=1+T, E1'=Q, F1'=free_96, [ B>=A && B>=0 && free_102>=free_99 && free_101>=2 && free_91>=free_101 && C>=1+N && free_91>=0 && free_99>=2 ], cost: 1 16: f1 -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, J'=C, K'=T, L'=N, M'=N, O'=free_112, P'=C, Q_1'=C, R'=C, S'=free_110, Z'=free_108, A1'=free_107, B1'=free_103, D1'=1+T, E1'=Q, F1'=free_109, [ B>=A && B>=0 && free_115>=free_112 && free_114>=2 && free_104>=free_114 && N>=1+C && free_104>=0 && free_112>=2 ], cost: 1 17: f1 -> f10 : A'=free_118, B'=free_117, C'=free_124, D'=free_119, E'=free_126, J'=C, K'=T, L'=N, M'=N, O'=free_125, P'=C, Q_1'=C, R'=C, S'=free_123, Z'=free_121, A1'=free_120, B1'=free_116, D1'=1+T, E1'=Q, F1'=free_122, [ B>=A && B>=0 && free_128>=free_125 && free_127>=2 && free_117>=free_127 && N>=1+C && free_117>=0 && free_125>=2 && C>=1+N ], cost: 1 1: f9 -> f10 : L'=M, N'=M, O'=free_3, P'=free_2, Q_1'=free_2, R'=J, [ free_4>=1+J && K>=0 && free_2>=1+free_4 && free_3>=2 ], cost: 1 2: f9 -> f10 : L'=M, N'=M, O'=free_6, P'=free_5, Q_1'=free_5, R'=J, [ free_7>=1+J && K>=0 && free_7>=1+free_5 && free_6>=2 ], cost: 1 3: f9 -> f10 : L'=M, N'=M, O'=free_9, P'=free_8, Q_1'=free_8, R'=J, [ J>=1+free_10 && K>=0 && free_8>=1+free_10 && free_9>=2 ], cost: 1 4: f9 -> f10 : L'=M, N'=M, O'=free_12, P'=free_11, Q_1'=free_11, R'=J, [ J>=1+free_13 && K>=0 && free_13>=1+free_11 && free_12>=2 ], cost: 1 5: f9 -> f4 : J'=free_19, L'=free_21, M'=free_17, O'=free_16, P'=free_20, Q_1'=free_15, R'=free_14, S'=free_18, [ K>=0 && free_21>=1+free_20 && free_16>=2 && M==J ], cost: 1 6: f9 -> f4 : J'=free_27, L'=free_29, M'=free_25, O'=free_24, P'=free_28, Q_1'=free_23, R'=free_22, S'=free_26, [ K>=0 && free_28>=1+free_29 && free_24>=2 && M==J ], cost: 1 7: f10 -> f10 : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1+T, U'=free_31, V'=Q, W'=-1+T, [ free_33>=1+J && T>=0 && free_30>=1+free_33 && free_32>=2 ], cost: 1 8: f10 -> f10 : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1+T, U'=free_35, V'=Q, W'=-1+T, [ free_37>=1+J && T>=0 && free_37>=1+free_34 && free_36>=2 ], cost: 1 9: f10 -> f10 : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1+T, U'=free_39, V'=Q, W'=-1+T, [ J>=1+free_41 && T>=0 && free_38>=1+free_41 && free_40>=2 ], cost: 1 10: f10 -> f10 : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1+T, U'=free_43, V'=Q, W'=-1+T, [ J>=1+free_45 && T>=0 && free_45>=1+free_42 && free_44>=2 ], cost: 1 11: f10 -> f4 : J'=free_46, M'=free_50, O'=free_51, Q_1'=free_49, R'=free_48, S'=free_47, [ free_51>=2 && T>=0 && M==J ], cost: 1 13: f3 -> f1 : A'=free_75, B'=2, C'=free_70, D'=free_72, E'=free_70, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 ], cost: 1 12: f3 -> f4 : A'=free_63, B'=free_62, C'=free_58, D'=free_67, E'=free_60, J'=free_65, L'=X, M'=free_61, N'=X, O'=free_59, P'=X, Q_1'=free_57, R'=free_55, S'=free_66, X'=free_64, Y'=free_54, Z'=free_53, A1'=free_52, B1'=free_56, [ 0>=free_68 && 0>=free_59 && 0>=free_69 ], cost: 1 Simplified the transitions: Start location: f3 0: f1 -> f1 : B'=1+B, C'=D, D'=free_1, E'=D, F'=free, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 14: f1 -> f10 : A'=free_79, B'=free_78, C'=free_85, D'=free_80, E'=free_87, J'=C, K'=T, L'=N, M'=N, O'=free_86, P'=C, Q_1'=C, R'=C, S'=free_84, Z'=free_82, A1'=free_81, B1'=free_77, D1'=1+T, E1'=Q, F1'=free_83, [ B>=A && B>=0 && C>=1+N && free_78>=0 && free_86>=2 && N>=1+C && 2<=free_78 ], cost: 1 15: f1 -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, J'=C, K'=T, L'=N, M'=N, O'=free_99, P'=C, Q_1'=C, R'=C, S'=free_97, Z'=free_95, A1'=free_94, B1'=free_90, D1'=1+T, E1'=Q, F1'=free_96, [ B>=A && B>=0 && C>=1+N && free_91>=0 && free_99>=2 && 2<=free_91 ], cost: 1 16: f1 -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, J'=C, K'=T, L'=N, M'=N, O'=free_112, P'=C, Q_1'=C, R'=C, S'=free_110, Z'=free_108, A1'=free_107, B1'=free_103, D1'=1+T, E1'=Q, F1'=free_109, [ B>=A && B>=0 && N>=1+C && free_104>=0 && free_112>=2 && 2<=free_104 ], cost: 1 17: f1 -> f10 : A'=free_118, B'=free_117, C'=free_124, D'=free_119, E'=free_126, J'=C, K'=T, L'=N, M'=N, O'=free_125, P'=C, Q_1'=C, R'=C, S'=free_123, Z'=free_121, A1'=free_120, B1'=free_116, D1'=1+T, E1'=Q, F1'=free_122, [ B>=A && B>=0 && N>=1+C && free_117>=0 && free_125>=2 && C>=1+N && 2<=free_117 ], cost: 1 7: f10 -> f10 : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1+T, U'=free_31, V'=Q, W'=-1+T, [ T>=0 && free_32>=2 && 1+J<=-1+free_30 ], cost: 1 8: f10 -> f10 : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1+T, U'=free_35, V'=Q, W'=-1+T, [ T>=0 && free_36>=2 ], cost: 1 9: f10 -> f10 : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1+T, U'=free_39, V'=Q, W'=-1+T, [ T>=0 && free_40>=2 ], cost: 1 10: f10 -> f10 : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1+T, U'=free_43, V'=Q, W'=-1+T, [ T>=0 && free_44>=2 && 1+free_42<=-1+J ], cost: 1 13: f3 -> f1 : A'=free_75, B'=2, C'=free_70, D'=free_72, E'=free_70, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 ], cost: 1 Eliminating 1 self-loops for location f1 Self-Loop 0 has the metering function: -B+A, resulting in the new transition 22. Removing the self-loops: 0. Eliminating 4 self-loops for location f10 Self-Loop 7 has the metering function: 1+T, resulting in the new transition 23. Self-Loop 8 has the metering function: 1+T, resulting in the new transition 24. Self-Loop 9 has the metering function: 1+T, resulting in the new transition 25. Self-Loop 10 has the metering function: 1+T, resulting in the new transition 26. Removing the self-loops: 7 8 9 10. Removed all Self-loops using metering functions (where possible): Start location: f3 22: f1 -> [5] : B'=A, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+A, H'=Q, [ A>=1+B && B>=0 ], cost: -B+A 23: f10 -> [6] : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1, U'=free_31, V'=Q, W'=-1, [ T>=0 && free_32>=2 && 1+J<=-1+free_30 ], cost: 1+T 24: f10 -> [6] : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1, U'=free_35, V'=Q, W'=-1, [ T>=0 && free_36>=2 ], cost: 1+T 25: f10 -> [6] : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1, U'=free_39, V'=Q, W'=-1, [ T>=0 && free_40>=2 ], cost: 1+T 26: f10 -> [6] : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1, U'=free_43, V'=Q, W'=-1, [ T>=0 && free_44>=2 && 1+free_42<=-1+J ], cost: 1+T 13: f3 -> f1 : A'=free_75, B'=2, C'=free_70, D'=free_72, E'=free_70, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 ], cost: 1 14: [5] -> f10 : A'=free_79, B'=free_78, C'=free_85, D'=free_80, E'=free_87, J'=C, K'=T, L'=N, M'=N, O'=free_86, P'=C, Q_1'=C, R'=C, S'=free_84, Z'=free_82, A1'=free_81, B1'=free_77, D1'=1+T, E1'=Q, F1'=free_83, [ B>=A && B>=0 && C>=1+N && free_78>=0 && free_86>=2 && N>=1+C && 2<=free_78 ], cost: 1 15: [5] -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, J'=C, K'=T, L'=N, M'=N, O'=free_99, P'=C, Q_1'=C, R'=C, S'=free_97, Z'=free_95, A1'=free_94, B1'=free_90, D1'=1+T, E1'=Q, F1'=free_96, [ B>=A && B>=0 && C>=1+N && free_91>=0 && free_99>=2 && 2<=free_91 ], cost: 1 16: [5] -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, J'=C, K'=T, L'=N, M'=N, O'=free_112, P'=C, Q_1'=C, R'=C, S'=free_110, Z'=free_108, A1'=free_107, B1'=free_103, D1'=1+T, E1'=Q, F1'=free_109, [ B>=A && B>=0 && N>=1+C && free_104>=0 && free_112>=2 && 2<=free_104 ], cost: 1 17: [5] -> f10 : A'=free_118, B'=free_117, C'=free_124, D'=free_119, E'=free_126, J'=C, K'=T, L'=N, M'=N, O'=free_125, P'=C, Q_1'=C, R'=C, S'=free_123, Z'=free_121, A1'=free_120, B1'=free_116, D1'=1+T, E1'=Q, F1'=free_122, [ B>=A && B>=0 && N>=1+C && free_117>=0 && free_125>=2 && C>=1+N && 2<=free_117 ], cost: 1 Applied simple chaining: Start location: f3 23: f10 -> [6] : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1, U'=free_31, V'=Q, W'=-1, [ T>=0 && free_32>=2 && 1+J<=-1+free_30 ], cost: 1+T 24: f10 -> [6] : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1, U'=free_35, V'=Q, W'=-1, [ T>=0 && free_36>=2 ], cost: 1+T 25: f10 -> [6] : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1, U'=free_39, V'=Q, W'=-1, [ T>=0 && free_40>=2 ], cost: 1+T 26: f10 -> [6] : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1, U'=free_43, V'=Q, W'=-1, [ T>=0 && free_44>=2 && 1+free_42<=-1+J ], cost: 1+T 13: f3 -> [5] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 14: [5] -> f10 : A'=free_79, B'=free_78, C'=free_85, D'=free_80, E'=free_87, J'=C, K'=T, L'=N, M'=N, O'=free_86, P'=C, Q_1'=C, R'=C, S'=free_84, Z'=free_82, A1'=free_81, B1'=free_77, D1'=1+T, E1'=Q, F1'=free_83, [ B>=A && B>=0 && C>=1+N && free_78>=0 && free_86>=2 && N>=1+C && 2<=free_78 ], cost: 1 15: [5] -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, J'=C, K'=T, L'=N, M'=N, O'=free_99, P'=C, Q_1'=C, R'=C, S'=free_97, Z'=free_95, A1'=free_94, B1'=free_90, D1'=1+T, E1'=Q, F1'=free_96, [ B>=A && B>=0 && C>=1+N && free_91>=0 && free_99>=2 && 2<=free_91 ], cost: 1 16: [5] -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, J'=C, K'=T, L'=N, M'=N, O'=free_112, P'=C, Q_1'=C, R'=C, S'=free_110, Z'=free_108, A1'=free_107, B1'=free_103, D1'=1+T, E1'=Q, F1'=free_109, [ B>=A && B>=0 && N>=1+C && free_104>=0 && free_112>=2 && 2<=free_104 ], cost: 1 17: [5] -> f10 : A'=free_118, B'=free_117, C'=free_124, D'=free_119, E'=free_126, J'=C, K'=T, L'=N, M'=N, O'=free_125, P'=C, Q_1'=C, R'=C, S'=free_123, Z'=free_121, A1'=free_120, B1'=free_116, D1'=1+T, E1'=Q, F1'=free_122, [ B>=A && B>=0 && N>=1+C && free_117>=0 && free_125>=2 && C>=1+N && 2<=free_117 ], cost: 1 Applied chaining over branches and pruning: Start location: f3 23: f10 -> [6] : L'=M, N'=M, O'=free_32, P'=free_30, Q_1'=free_30, R'=J, T'=-1, U'=free_31, V'=Q, W'=-1, [ T>=0 && free_32>=2 && 1+J<=-1+free_30 ], cost: 1+T 24: f10 -> [6] : L'=M, N'=M, O'=free_36, P'=free_34, Q_1'=free_34, R'=J, T'=-1, U'=free_35, V'=Q, W'=-1, [ T>=0 && free_36>=2 ], cost: 1+T 25: f10 -> [6] : L'=M, N'=M, O'=free_40, P'=free_38, Q_1'=free_38, R'=J, T'=-1, U'=free_39, V'=Q, W'=-1, [ T>=0 && free_40>=2 ], cost: 1+T 26: f10 -> [6] : L'=M, N'=M, O'=free_44, P'=free_42, Q_1'=free_42, R'=J, T'=-1, U'=free_43, V'=Q, W'=-1, [ T>=0 && free_44>=2 && 1+free_42<=-1+J ], cost: 1+T 28: f3 -> f10 : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_99, P'=free_1, Q_1'=free_1, R'=free_1, S'=free_97, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 ], cost: free_75 29: f3 -> f10 : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_112, P'=free_1, Q_1'=free_1, R'=free_1, S'=free_110, X'=free_71, Y'=free_73, Z'=free_108, A1'=free_107, B1'=free_103, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_109, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_76>=1+free_1 && free_104>=0 && free_112>=2 && 2<=free_104 ], cost: free_75 27: f3 -> [7] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 30: f3 -> [8] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 Applied chaining over branches and pruning: Start location: f3 31: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_32, P'=free_30, Q_1'=free_30, R'=free_1, S'=free_97, T'=-1, U'=free_31, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30 ], cost: 1+free_75+T 32: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_36, P'=free_34, Q_1'=free_34, R'=free_1, S'=free_97, T'=-1, U'=free_35, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_36>=2 ], cost: 1+free_75+T 34: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_44, P'=free_42, Q_1'=free_42, R'=free_1, S'=free_97, T'=-1, U'=free_43, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_44>=2 && 1+free_42<=-1+free_1 ], cost: 1+free_75+T 35: f3 -> [6] : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_32, P'=free_30, Q_1'=free_30, R'=free_1, S'=free_110, T'=-1, U'=free_31, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_108, A1'=free_107, B1'=free_103, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_109, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_76>=1+free_1 && free_104>=0 && free_112>=2 && 2<=free_104 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30 ], cost: 1+free_75+T 38: f3 -> [6] : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_44, P'=free_42, Q_1'=free_42, R'=free_1, S'=free_110, T'=-1, U'=free_43, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_108, A1'=free_107, B1'=free_103, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_109, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_76>=1+free_1 && free_104>=0 && free_112>=2 && 2<=free_104 && T>=0 && free_44>=2 && 1+free_42<=-1+free_1 ], cost: 1+free_75+T 27: f3 -> [7] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 30: f3 -> [8] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 Final control flow graph problem, now checking costs for infinitely many models: Start location: f3 31: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_32, P'=free_30, Q_1'=free_30, R'=free_1, S'=free_97, T'=-1, U'=free_31, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30 ], cost: 1+free_75+T 32: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_36, P'=free_34, Q_1'=free_34, R'=free_1, S'=free_97, T'=-1, U'=free_35, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_36>=2 ], cost: 1+free_75+T 34: f3 -> [6] : A'=free_92, B'=free_91, C'=free_98, D'=free_93, E'=free_100, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_44, P'=free_42, Q_1'=free_42, R'=free_1, S'=free_97, T'=-1, U'=free_43, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_95, A1'=free_94, B1'=free_90, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_96, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_44>=2 && 1+free_42<=-1+free_1 ], cost: 1+free_75+T 35: f3 -> [6] : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_32, P'=free_30, Q_1'=free_30, R'=free_1, S'=free_110, T'=-1, U'=free_31, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_108, A1'=free_107, B1'=free_103, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_109, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_76>=1+free_1 && free_104>=0 && free_112>=2 && 2<=free_104 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30 ], cost: 1+free_75+T 38: f3 -> [6] : A'=free_105, B'=free_104, C'=free_111, D'=free_106, E'=free_113, F'=free, G'=-1+free_75, H'=Q, J'=free_1, K'=T, L'=free_76, M'=free_76, N'=free_76, O'=free_44, P'=free_42, Q_1'=free_42, R'=free_1, S'=free_110, T'=-1, U'=free_43, V'=Q, W'=-1, X'=free_71, Y'=free_73, Z'=free_108, A1'=free_107, B1'=free_103, C1'=free_74, D1'=1+T, E1'=Q, F1'=free_109, [ free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_76>=1+free_1 && free_104>=0 && free_112>=2 && 2<=free_104 && T>=0 && free_44>=2 && 1+free_42<=-1+free_1 ], cost: 1+free_75+T 27: f3 -> [7] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 30: f3 -> [8] : A'=free_75, B'=free_75, C'=free_1, D'=free_1, E'=free_1, F'=free, G'=-1+free_75, H'=Q, L'=free_76, N'=free_76, O'=free_75, X'=free_71, Y'=free_73, Z'=free_76, B1'=free_70, C1'=free_74, [ free_75>=2 && free_75>=3 && 2>=0 ], cost: -1+free_75 Computing complexity for remaining 7 transitions. Found configuration with infinitely models for cost: 1+free_75+T and guard: free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30: free_99: Pos, free_30: Pos, free_75: Pos, free_91: Pos, free_76: Pos, free_1: Pos, free_32: Pos, T: Pos, where: free_30 > free_1 free_1 > free_76 Found new complexity INF, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: free_75>=2 && free_75>=3 && 2>=0 && free_75>=free_75 && free_75>=0 && free_1>=1+free_76 && free_91>=0 && free_99>=2 && 2<=free_91 && T>=0 && free_32>=2 && 1+free_1<=-1+free_30 Final Cost: 1+free_75+T Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)