Trying to load file: main.koat Initial Control flow graph problem: Start location: f26 1: f29 -> f29 : B'=-1+B, D'=free_8, E'=M, F'=free_6, L'=free_7, N'=B, O'=A, [ A>=free_8 && A>=0 && B>=1 && free_8>=2 ], cost: 1 0: f29 -> f34 : C'=1, D'=free_4, E'=free_1, F'=0, G'=H, Q'=free_3, J'=1+H, K'=free, L'=free_2, [ A>=0 && B>=1 && free_4>=2 && free_5>=free_4 && C==1 ], cost: 1 55: f29 -> f17 : B'=free_327, D'=free_328, M'=E, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, V3'=W3, Y3'=1+W3, [ A>=free_331 && A>=0 && 0>=B && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 ], cost: 1 8: f34 -> f34 : C'=1+C, D'=free_41, E'=free_38, F'=0, H'=-1+H, Q'=free_40, L'=free_37, G1'=M, H1'=free_39, Q1'=1+C, J1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_41>=2 ], cost: 1 7: f34 -> f35 : B'=-1+free_35, D'=free_36, E'=free_33, F'=free_32, L'=free_34, E1'=free_35, F1'=-1+free_35, [ C>=0 && B>=1 && H>=0 && free_35>=1 && free_36>=2 ], cost: 1 58: f34 -> f15 : B'=free_340, C'=1+T3, D'=free_341, F'=0, M'=0, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, S3'=T3, [ H>=0 && C>=0 && free_343>=1 && free_342>=2 && free_340>=1 && free_341>=2 && M==0 ], cost: 1 3: f30 -> f34 : C'=2, D'=free_19, E'=free_16, F'=0, H'=-1+G, L'=free_18, S'=M, T'=free_15, U'=free_17, [ B>=1 && free_19>=2 && G>=0 && 1+H==G && C==2 ], cost: 1 2: f30 -> f35 : B'=-1+free_13, C'=1, D'=free_14, E'=free_11, F'=free_10, H'=G, L'=free_12, P'=free_13, Q_1'=free_9, R'=-1+free_13, [ B>=1 && H>=0 && free_14>=2 && free_13>=1 && G==H && C==1 ], cost: 1 56: f30 -> f15 : B'=free_332, C'=1+T3, D'=free_333, F'=0, G'=0, M'=0, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, S3'=T3, [ free_335>=1 && free_334>=2 && free_332>=1 && free_333>=2 && M==0 && G==0 && C==1 ], cost: 1 10: f35 -> f34 : C'=1+C, D'=free_52, E'=free_49, F'=0, H'=-1+H, Q'=free_51, L'=free_48, K1'=free_50, O1'=M, P1'=free_47, Q1_1'=1+C, R1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_52>=2 ], cost: 1 9: f35 -> f35 : B'=-1+B, D'=free_46, E'=free_43, F'=free_45, L'=free_42, K1'=free_44, L1'=B, M1'=C, N1'=H, [ C>=0 && B>=1 && H>=0 && free_46>=2 ], cost: 1 59: f35 -> f10 : B'=free_346, D'=free_347, F'=free_344, M'=free_345, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, [ 0>=B && H>=0 && C>=0 && free_347>=2 && 0>=free_346 ], cost: 1 5: f31 -> f34 : D'=free_29, E'=free_26, F'=0, L'=free_28, Z'=free_25, A1'=free_27, [ B>=1 && free_29>=2 && G>=0 ], cost: 1 4: f31 -> f35 : B'=-1+B, C'=1, D'=free_24, E'=free_21, F'=free_23, H'=G, L'=free_20, V'=free_22, W'=B, X'=Q, Y'=G, [ B>=1 && G>=0 && free_24>=2 && H==G && C==1 ], cost: 1 57: f31 -> f10 : B'=free_338, C'=1, D'=free_339, F'=free_336, H'=G, M'=free_337, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, [ 0>=B && H>=0 && 0>=free_338 && free_339>=2 && C==1 && G==H ], cost: 1 6: f32 -> f32 : B'=-1+B, D'=1, E'=M, F'=free_31, L'=free_30, B1'=B, C1'=D1, [ B>=1 ], cost: 1 63: f32 -> f27 : B'=free_388, D'=1, E'=0, M'=free_389, A2'=free_381, B2'=free_386, C2'=free_382, D2'=free_385, E2'=free_387, F2'=free_383, H2'=free_384, [ 0>=B && 0>=free_391 && 0>=free_388 && 0>=free_390 && E==0 ], cost: 1 64: f32 -> f27 : B'=free_400, D'=1, E'=free_393, F'=0, L'=free_392, M'=0, A2'=free_395, B2'=free_394, C2'=free_397, D2'=free_401, E2'=free_396, F2'=free_399, H2'=free_398, [ B>=1 && free_402>=1 && free_400>=1 && free_403>=1 && M==0 ], cost: 1 12: f1 -> f29 : A'=free_59, D'=free_63, E'=T1, M'=T1, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, Y1'=free_60, Z1'=free_55, A2'=free_58, [ A>=S1 && A>=0 && free_59>=free_63 && free_63>=2 ], cost: 1 11: f1 -> f1 : A'=1+A, T1'=U1, U1'=free_54, V1'=U1, W1'=free_53, X1'=A, [ S1>=1+A && A>=0 ], cost: 1 13: f10 -> f13 : B'=free_65, C'=1+G2, D'=free_67, E'=C2, F'=free_66, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_64, L2'=-1+free_64, M2'=H, N2'=G2, [ free_68>=0 && H>=0 && 0>=free_65 && free_67>=2 && B2==0 && C==0 ], cost: 1 14: f10 -> f13 : B'=free_72, C'=1+G2, D'=free_73, E'=C2, F'=free_69, H'=free_71, M'=free_70, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_71, M2'=H, N2'=G2, O2'=-1+C, P2'=free_71, [ C>=0 && H>=0 && 0>=free_72 && free_73>=2 && B2==0 ], cost: 1 15: f10 -> f13 : B'=free_75, C'=0, D'=free_78, E'=C2, F'=free_77, H'=free_74, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_76, L2'=-1+free_76, M2'=H, Q2_1'=-1+free_74, R2'=-1+free_74, [ free_79>=0 && H>=0 && 0>=free_75 && free_78>=2 && B2==0 && C==0 ], cost: 1 16: f10 -> f13 : B'=free_81, D'=free_84, E'=C2, F'=free_83, H'=free_80, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_80, M2'=H, O2'=-1+C, P2'=free_80, Q2_1'=-1+free_82, R2'=-1+free_82, [ C>=0 && H>=0 && 0>=free_81 && free_84>=2 && B2==0 ], cost: 1 17: f10 -> f13 : B'=free_86, C'=free_85, D'=free_89, E'=C2, F'=free_88, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_85, J2'=H, K2'=free_87, L2'=-1+free_87, N2'=-1+free_85, Q2_1'=S2, [ free_90>=0 && H>=0 && 0>=free_86 && free_89>=2 && B2==0 && C==0 ], cost: 1 18: f10 -> f13 : B'=free_92, C'=free_91, D'=free_95, E'=C2, F'=free_94, H'=free_93, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_91, J2'=H, K2'=free_93, N2'=-1+free_91, O2'=-1+C, P2'=free_93, Q2_1'=S2, [ C>=0 && H>=0 && 0>=free_92 && free_95>=2 && B2==0 ], cost: 1 19: f10 -> f13 : B'=free_97, C'=0, D'=free_99, E'=C2, F'=free_98, H'=1+S2, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_96, L2'=-1+free_96, Q2_1'=S2, R2'=S2, [ free_100>=0 && H>=0 && 0>=free_97 && free_99>=2 && B2==0 && C==0 ], cost: 1 20: f10 -> f13 : B'=free_102, D'=free_104, E'=C2, F'=free_103, H'=free_101, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_101, O2'=-1+C, P2'=free_101, Q2_1'=S2, R2'=S2, [ C>=0 && H>=0 && 0>=free_102 && free_104>=2 && B2==0 ], cost: 1 21: f10 -> f13 : B'=free_106, C'=free_105, D'=free_109, E'=C2, F'=free_108, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_105, J2'=H, K2'=free_107, L2'=-1+free_107, N2'=-1+free_105, T2'=U2, [ free_110>=0 && H>=0 && 0>=free_106 && free_109>=2 && B2==0 && C==0 ], cost: 1 22: f10 -> f13 : B'=free_112, C'=free_111, D'=free_115, E'=C2, F'=free_114, H'=free_113, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_111, J2'=H, K2'=free_113, N2'=-1+free_111, O2'=-1+C, P2'=free_113, T2'=U2, [ C>=0 && H>=0 && 0>=free_112 && free_115>=2 && B2==0 ], cost: 1 23: f10 -> f13 : B'=free_117, C'=0, D'=free_120, E'=C2, F'=free_119, H'=free_116, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_118, L2'=-1+free_118, Q2_1'=-1+free_116, R2'=-1+free_116, T2'=U2, [ free_121>=0 && H>=0 && 0>=free_117 && free_120>=2 && B2==0 && C==0 ], cost: 1 24: f10 -> f13 : B'=free_123, D'=free_126, E'=C2, F'=free_125, H'=free_122, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_122, O2'=-1+C, P2'=free_122, Q2_1'=-1+free_124, R2'=-1+free_124, T2'=U2, [ C>=0 && H>=0 && 0>=free_123 && free_126>=2 && B2==0 ], cost: 1 41: f13 -> f13 : B'=free_224, D'=free_230, E'=free_228, F'=free_227, M'=free_226, B2'=0, D2'=free_228, E2'=0, F2'=free_228, G2'=0, H2'=C2, S2'=-1+H, C3'=free_223, D3'=free_229, E3'=free_222, F3'=free_225, G3'=-1+H, [ free_230>=2 && 0>=free_224 && B2==0 && G2==0 ], cost: 1 42: f13 -> f13 : B'=free_233, D'=free_239, E'=free_237, F'=free_236, M'=free_235, B2'=0, D2'=free_237, E2'=0, F2'=free_237, G2'=-1+G2, H2'=C2, C3'=free_232, D3'=free_238, H3'=free_231, Q3'=free_234, J3'=H, K3'=-1+G2, [ 0>=free_233 && free_239>=2 && B2==0 ], cost: 1 43: f13 -> f13 : B'=free_245, D'=free_247, E'=free_243, F'=free_242, Q'=free_244, M'=free_243, B2'=0, D2'=free_243, E2'=0, F2'=free_243, H2'=C2, U2'=-1+L3, C3'=free_241, D3'=free_246, M3'=free_240, N3'=-1+L3, [ free_247>=2 && 0>=free_245 && B2==0 ], cost: 1 44: f13 -> f13 : B'=free_250, D'=free_255, E'=free_253, F'=free_252, M'=free_251, B2'=0, D2'=free_253, E2'=0, F2'=free_253, H2'=C2, U2'=-1+S2, C3'=free_251, D3'=free_249, N3'=-1+S2, O3'=free_254, P3'=free_248, [ free_255>=2 && 0>=free_250 && B2==0 ], cost: 1 45: f13 -> f13 : B'=free_258, D'=free_264, E'=free_262, F'=free_261, M'=free_260, B2'=0, D2'=free_262, E2'=0, F2'=free_262, H2'=C2, U2'=-1+U2, C3'=free_257, D3'=free_263, N3'=-1+U2, Q3_1'=free_256, R3'=free_259, [ free_264>=2 && 0>=free_258 && B2==0 ], cost: 1 46: f13 -> f27 : D'=free_272, A2'=free_271, B2'=free_269, C2'=free_266, D2'=free_268, E2'=free_270, F2'=free_267, H2'=free_265, [ free_272>=2 && B2==C2 ], cost: 1 25: f11 -> f13 : B'=free_130, D'=free_131, E'=free_128, F'=free_127, M'=C2, B2'=0, D2'=free_128, E2'=0, F2'=free_128, H2'=C2, Q2'=G2, M2'=H, N2'=1+G2, V2'=free_129, W2'=-1+free_129, [ 0>=free_130 && free_131>=2 && B2==0 && N2==0 ], cost: 1 26: f11 -> f13 : B'=free_133, D'=free_137, E'=free_136, F'=free_135, H'=free_132, M'=free_134, B2'=0, D2'=free_136, E2'=0, F2'=free_136, H2'=C2, Q2'=G2, M2'=H, N2'=1+G2, V2'=free_132, X2'=-1+N2, Y2'=free_132, [ 0>=free_133 && free_137>=2 && B2==0 ], cost: 1 27: f11 -> f13 : B'=free_140, D'=free_141, E'=free_139, F'=free_138, M'=free_139, B2'=0, D2'=free_139, E2'=0, F2'=free_139, H2'=C2, Q2'=G2, M2'=H, N2'=1+G2, Z2'=-1+R2, [ 0>=free_140 && free_141>=2 && B2==0 ], cost: 1 28: f11 -> f13 : B'=free_145, D'=free_146, E'=free_143, F'=free_142, H'=1+S2, M'=C2, B2'=0, D2'=free_143, E2'=0, F2'=free_143, H2'=C2, N2'=0, Q2_1'=S2, V2'=free_144, W2'=-1+free_144, [ 0>=free_145 && free_146>=2 && B2==0 && N2==0 ], cost: 1 29: f11 -> f13 : B'=free_150, D'=free_151, E'=free_148, F'=free_147, H'=free_149, M'=C2, B2'=0, D2'=free_148, E2'=0, F2'=free_148, H2'=C2, Q2_1'=S2, V2'=free_149, X2'=-1+N2, Y2'=free_149, [ 0>=free_150 && free_151>=2 && B2==0 ], cost: 1 30: f11 -> f13 : B'=free_152, D'=free_154, E'=C2, F'=free_153, H'=1+S2, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2_1'=S2, Z2'=-1+R2, [ 0>=free_152 && free_154>=2 && B2==0 ], cost: 1 31: f11 -> f13 : B'=free_156, D'=free_158, E'=C2, F'=free_157, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, N2'=0, R2'=1+U2, T2'=U2, V2'=free_155, W2'=-1+free_155, [ 0>=free_156 && free_158>=2 && B2==0 && N2==0 ], cost: 1 32: f11 -> f13 : B'=free_162, D'=free_163, E'=free_160, F'=free_159, H'=free_161, M'=free_160, B2'=0, D2'=free_160, E2'=0, F2'=free_160, H2'=C2, R2'=1+U2, T2'=U2, V2'=free_161, X2'=-1+N2, Y2'=free_161, [ 0>=free_162 && free_163>=2 && B2==0 ], cost: 1 33: f11 -> f13 : B'=free_166, D'=free_167, E'=free_165, F'=free_164, M'=free_165, B2'=0, D2'=free_165, E2'=0, F2'=free_165, H2'=C2, R2'=1+U2, T2'=U2, Z2'=-1+R2, [ 0>=free_166 && free_167>=2 && B2==0 ], cost: 1 34: f11 -> f27 : B'=free_169, D'=free_178, E'=free_173, F'=free_172, M'=free_173, A2'=free_175, B2'=free_170, C2'=free_177, D2'=free_176, E2'=free_171, F2'=free_174, H2'=free_168, [ free_178>=2 && 0>=free_169 && B2==C2 ], cost: 1 35: f12 -> f13 : B'=free_182, D'=free_183, E'=free_180, F'=free_179, M'=C2, B2'=0, D2'=free_180, E2'=0, F2'=free_180, H2'=C2, Q2'=0, S2'=-1+H, A3'=free_181, [ 0>=free_182 && free_183>=2 && B2==0 && Q2==0 ], cost: 1 36: f12 -> f13 : B'=free_185, D'=free_189, E'=free_188, F'=free_187, M'=free_186, B2'=0, D2'=free_188, E2'=0, F2'=free_188, G2'=-1+Q2, H2'=C2, A3'=free_184, B3'=H, [ 0>=free_185 && free_189>=2 && B2==0 ], cost: 1 37: f12 -> f13 : B'=free_193, D'=free_194, E'=free_191, F'=free_190, M'=free_191, B2'=0, D2'=free_191, E2'=0, F2'=free_191, H2'=C2, Q2_1'=T2, U2'=-1+T2, A3'=free_192, [ 0>=free_193 && free_194>=2 && B2==0 ], cost: 1 38: f12 -> f13 : B'=free_195, D'=free_199, E'=free_198, F'=free_197, M'=free_196, B2'=0, D2'=free_198, E2'=0, F2'=free_198, H2'=C2, U2'=-1+Q2_1, A3'=free_196, [ 0>=free_195 && free_199>=2 && B2==0 ], cost: 1 39: f12 -> f27 : B'=free_204, D'=free_210, E'=free_201, F'=free_207, M'=free_205, A2'=free_200, B2'=free_202, C2'=free_209, D2'=free_208, E2'=free_203, F2'=free_206, H2'=free_205, Q2_1'=0, [ free_210>=2 && 0>=free_204 && B2==C2 && Q2_1==0 ], cost: 1 40: f12 -> f27 : B'=free_212, D'=free_221, E'=free_216, F'=free_215, M'=free_216, A2'=free_218, B2'=free_213, C2'=free_220, D2'=free_219, E2'=free_214, F2'=free_217, H2'=free_211, T2'=0, [ free_221>=2 && 0>=free_212 && B2==C2 && T2==0 ], cost: 1 48: f14 -> f27 : B'=free_276, D'=free_285, E'=free_284, A2'=free_279, B2'=free_281, C2'=free_277, D2'=free_280, E2'=free_283, F2'=free_278, H2'=free_282, [ S3>=0 && free_276>=1 && free_285>=2 && B2==C2 ], cost: 1 47: f14 -> f15 : B'=free_274, D'=free_275, E'=free_273, F'=0, M'=0, B2'=0, D2'=free_273, E2'=0, F2'=free_273, H2'=C2, [ S3>=0 && free_274>=1 && free_275>=2 && B2==0 ], cost: 1 50: f15 -> f27 : B'=free_290, D'=free_299, E'=free_298, A2'=free_293, B2'=free_295, C2'=free_291, D2'=free_294, E2'=free_297, F2'=free_292, H2'=free_296, [ T3>=0 && free_290>=1 && free_299>=2 && B2==C2 ], cost: 1 49: f15 -> f15 : B'=free_288, D'=free_289, E'=free_287, F'=0, Q'=free_286, M'=0, B2'=0, D2'=free_287, E2'=0, F2'=free_287, H2'=C2, T3'=-1+T3, U3'=-1+T3, [ T3>=0 && free_288>=1 && free_289>=2 && B2==0 ], cost: 1 52: f16 -> f27 : B'=free_303, D'=free_312, M'=free_307, A2'=free_306, B2'=free_304, C2'=free_311, D2'=free_310, E2'=free_305, F2'=free_308, H2'=free_309, [ V3>=0 && free_312>=2 && 0>=free_303 && B2==C2 ], cost: 1 51: f16 -> f17 : B'=free_301, D'=free_302, E'=free_300, M'=free_300, B2'=0, D2'=free_300, E2'=0, F2'=free_300, H2'=C2, [ V3>=0 && free_302>=2 && 0>=free_301 && B2==0 ], cost: 1 54: f17 -> f27 : B'=free_317, D'=free_326, M'=free_321, A2'=free_320, B2'=free_318, C2'=free_325, D2'=free_324, E2'=free_319, F2'=free_322, H2'=free_323, [ W3>=0 && free_326>=2 && 0>=free_317 && B2==C2 ], cost: 1 53: f17 -> f17 : B'=free_315, D'=free_316, E'=free_314, Q'=free_313, M'=free_314, B2'=0, D2'=free_314, E2'=0, F2'=free_314, H2'=C2, W3'=-1+W3, X3'=-1+W3, [ W3>=0 && free_316>=2 && 0>=free_315 && B2==0 ], cost: 1 61: f26 -> f32 : A'=free_361, D'=1, E'=U1, L'=free_357, M'=U1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [], cost: 1 60: f26 -> f1 : A'=2, D'=free_352, L'=free_349, S1'=free_352, T1'=free_351, U1'=free_348, V1'=free_351, Y1'=free_351, Z3'=free_350, A4'=2, [ free_352>=2 ], cost: 1 62: f26 -> f27 : A'=free_375, D'=free_376, E'=0, L'=free_363, M'=0, S1'=free_368, T1'=free_373, U1'=free_372, V1'=free_367, Y1'=free_362, Z1'=free_377, A2'=free_366, B2'=free_370, C2'=free_364, D2'=free_369, E2'=free_374, F2'=free_365, H2'=free_371, [ 0>=free_378 && 0>=free_379 && 0>=free_376 && 0>=free_380 ], cost: 1 Simplified the transitions: Start location: f26 1: f29 -> f29 : B'=-1+B, D'=free_8, E'=M, F'=free_6, L'=free_7, N'=B, O'=A, [ A>=free_8 && A>=0 && B>=1 && free_8>=2 ], cost: 1 0: f29 -> f34 : C'=1, D'=free_4, E'=free_1, F'=0, G'=H, Q'=free_3, J'=1+H, K'=free, L'=free_2, [ A>=0 && B>=1 && free_4>=2 && C==1 ], cost: 1 55: f29 -> f17 : B'=free_327, D'=free_328, M'=E, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, V3'=W3, Y3'=1+W3, [ A>=free_331 && A>=0 && 0>=B && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 ], cost: 1 8: f34 -> f34 : C'=1+C, D'=free_41, E'=free_38, F'=0, H'=-1+H, Q'=free_40, L'=free_37, G1'=M, H1'=free_39, Q1'=1+C, J1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_41>=2 ], cost: 1 7: f34 -> f35 : B'=-1+free_35, D'=free_36, E'=free_33, F'=free_32, L'=free_34, E1'=free_35, F1'=-1+free_35, [ C>=0 && B>=1 && H>=0 && free_35>=1 && free_36>=2 ], cost: 1 58: f34 -> f15 : B'=free_340, C'=1+T3, D'=free_341, F'=0, M'=0, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, S3'=T3, [ H>=0 && C>=0 && free_343>=1 && free_342>=2 && free_340>=1 && free_341>=2 && M==0 ], cost: 1 10: f35 -> f34 : C'=1+C, D'=free_52, E'=free_49, F'=0, H'=-1+H, Q'=free_51, L'=free_48, K1'=free_50, O1'=M, P1'=free_47, Q1_1'=1+C, R1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_52>=2 ], cost: 1 9: f35 -> f35 : B'=-1+B, D'=free_46, E'=free_43, F'=free_45, L'=free_42, K1'=free_44, L1'=B, M1'=C, N1'=H, [ C>=0 && B>=1 && H>=0 && free_46>=2 ], cost: 1 59: f35 -> f10 : B'=free_346, D'=free_347, F'=free_344, M'=free_345, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, [ 0>=B && H>=0 && C>=0 && free_347>=2 && 0>=free_346 ], cost: 1 6: f32 -> f32 : B'=-1+B, D'=1, E'=M, F'=free_31, L'=free_30, B1'=B, C1'=D1, [ B>=1 ], cost: 1 12: f1 -> f29 : A'=free_59, D'=free_63, E'=T1, M'=T1, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, Y1'=free_60, Z1'=free_55, A2'=free_58, [ A>=S1 && A>=0 && free_59>=free_63 && free_63>=2 ], cost: 1 11: f1 -> f1 : A'=1+A, T1'=U1, U1'=free_54, V1'=U1, W1'=free_53, X1'=A, [ S1>=1+A && A>=0 ], cost: 1 13: f10 -> f13 : B'=free_65, C'=1+G2, D'=free_67, E'=C2, F'=free_66, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_64, L2'=-1+free_64, M2'=H, N2'=G2, [ H>=0 && 0>=free_65 && free_67>=2 && B2==0 && C==0 ], cost: 1 14: f10 -> f13 : B'=free_72, C'=1+G2, D'=free_73, E'=C2, F'=free_69, H'=free_71, M'=free_70, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_71, M2'=H, N2'=G2, O2'=-1+C, P2'=free_71, [ C>=0 && H>=0 && 0>=free_72 && free_73>=2 && B2==0 ], cost: 1 15: f10 -> f13 : B'=free_75, C'=0, D'=free_78, E'=C2, F'=free_77, H'=free_74, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_76, L2'=-1+free_76, M2'=H, Q2_1'=-1+free_74, R2'=-1+free_74, [ H>=0 && 0>=free_75 && free_78>=2 && B2==0 && C==0 ], cost: 1 16: f10 -> f13 : B'=free_81, D'=free_84, E'=C2, F'=free_83, H'=free_80, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_80, M2'=H, O2'=-1+C, P2'=free_80, Q2_1'=-1+free_82, R2'=-1+free_82, [ C>=0 && H>=0 && 0>=free_81 && free_84>=2 && B2==0 ], cost: 1 17: f10 -> f13 : B'=free_86, C'=free_85, D'=free_89, E'=C2, F'=free_88, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_85, J2'=H, K2'=free_87, L2'=-1+free_87, N2'=-1+free_85, Q2_1'=S2, [ H>=0 && 0>=free_86 && free_89>=2 && B2==0 && C==0 ], cost: 1 18: f10 -> f13 : B'=free_92, C'=free_91, D'=free_95, E'=C2, F'=free_94, H'=free_93, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_91, J2'=H, K2'=free_93, N2'=-1+free_91, O2'=-1+C, P2'=free_93, Q2_1'=S2, [ C>=0 && H>=0 && 0>=free_92 && free_95>=2 && B2==0 ], cost: 1 19: f10 -> f13 : B'=free_97, C'=0, D'=free_99, E'=C2, F'=free_98, H'=1+S2, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_96, L2'=-1+free_96, Q2_1'=S2, R2'=S2, [ H>=0 && 0>=free_97 && free_99>=2 && B2==0 && C==0 ], cost: 1 20: f10 -> f13 : B'=free_102, D'=free_104, E'=C2, F'=free_103, H'=free_101, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_101, O2'=-1+C, P2'=free_101, Q2_1'=S2, R2'=S2, [ C>=0 && H>=0 && 0>=free_102 && free_104>=2 && B2==0 ], cost: 1 21: f10 -> f13 : B'=free_106, C'=free_105, D'=free_109, E'=C2, F'=free_108, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_105, J2'=H, K2'=free_107, L2'=-1+free_107, N2'=-1+free_105, T2'=U2, [ free_110>=0 && H>=0 && 0>=free_106 && free_109>=2 && B2==0 && C==0 ], cost: 1 22: f10 -> f13 : B'=free_112, C'=free_111, D'=free_115, E'=C2, F'=free_114, H'=free_113, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_111, J2'=H, K2'=free_113, N2'=-1+free_111, O2'=-1+C, P2'=free_113, T2'=U2, [ C>=0 && H>=0 && 0>=free_112 && free_115>=2 && B2==0 ], cost: 1 23: f10 -> f13 : B'=free_117, C'=0, D'=free_120, E'=C2, F'=free_119, H'=free_116, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_118, L2'=-1+free_118, Q2_1'=-1+free_116, R2'=-1+free_116, T2'=U2, [ free_121>=0 && H>=0 && 0>=free_117 && free_120>=2 && B2==0 && C==0 ], cost: 1 24: f10 -> f13 : B'=free_123, D'=free_126, E'=C2, F'=free_125, H'=free_122, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_122, O2'=-1+C, P2'=free_122, Q2_1'=-1+free_124, R2'=-1+free_124, T2'=U2, [ C>=0 && H>=0 && 0>=free_123 && free_126>=2 && B2==0 ], cost: 1 41: f13 -> f13 : B'=free_224, D'=free_230, E'=free_228, F'=free_227, M'=free_226, B2'=0, D2'=free_228, E2'=0, F2'=free_228, G2'=0, H2'=C2, S2'=-1+H, C3'=free_223, D3'=free_229, E3'=free_222, F3'=free_225, G3'=-1+H, [ free_230>=2 && 0>=free_224 && B2==0 && G2==0 ], cost: 1 42: f13 -> f13 : B'=free_233, D'=free_239, E'=free_237, F'=free_236, M'=free_235, B2'=0, D2'=free_237, E2'=0, F2'=free_237, G2'=-1+G2, H2'=C2, C3'=free_232, D3'=free_238, H3'=free_231, Q3'=free_234, J3'=H, K3'=-1+G2, [ 0>=free_233 && free_239>=2 && B2==0 ], cost: 1 43: f13 -> f13 : B'=free_245, D'=free_247, E'=free_243, F'=free_242, Q'=free_244, M'=free_243, B2'=0, D2'=free_243, E2'=0, F2'=free_243, H2'=C2, U2'=-1+L3, C3'=free_241, D3'=free_246, M3'=free_240, N3'=-1+L3, [ free_247>=2 && 0>=free_245 && B2==0 ], cost: 1 44: f13 -> f13 : B'=free_250, D'=free_255, E'=free_253, F'=free_252, M'=free_251, B2'=0, D2'=free_253, E2'=0, F2'=free_253, H2'=C2, U2'=-1+S2, C3'=free_251, D3'=free_249, N3'=-1+S2, O3'=free_254, P3'=free_248, [ free_255>=2 && 0>=free_250 && B2==0 ], cost: 1 45: f13 -> f13 : B'=free_258, D'=free_264, E'=free_262, F'=free_261, M'=free_260, B2'=0, D2'=free_262, E2'=0, F2'=free_262, H2'=C2, U2'=-1+U2, C3'=free_257, D3'=free_263, N3'=-1+U2, Q3_1'=free_256, R3'=free_259, [ free_264>=2 && 0>=free_258 && B2==0 ], cost: 1 49: f15 -> f15 : B'=free_288, D'=free_289, E'=free_287, F'=0, Q'=free_286, M'=0, B2'=0, D2'=free_287, E2'=0, F2'=free_287, H2'=C2, T3'=-1+T3, U3'=-1+T3, [ T3>=0 && free_288>=1 && free_289>=2 && B2==0 ], cost: 1 53: f17 -> f17 : B'=free_315, D'=free_316, E'=free_314, Q'=free_313, M'=free_314, B2'=0, D2'=free_314, E2'=0, F2'=free_314, H2'=C2, W3'=-1+W3, X3'=-1+W3, [ W3>=0 && free_316>=2 && 0>=free_315 && B2==0 ], cost: 1 61: f26 -> f32 : A'=free_361, D'=1, E'=U1, L'=free_357, M'=U1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [], cost: 1 60: f26 -> f1 : A'=2, D'=free_352, L'=free_349, S1'=free_352, T1'=free_351, U1'=free_348, V1'=free_351, Y1'=free_351, Z3'=free_350, A4'=2, [ free_352>=2 ], cost: 1 Eliminating 1 self-loops for location f29 Self-Loop 1 has the metering function: B, resulting in the new transition 65. Removing the self-loops: 1. Eliminating 1 self-loops for location f34 Self-Loop 8 has the metering function: 1+H, resulting in the new transition 66. Removing the self-loops: 8. Eliminating 1 self-loops for location f35 Self-Loop 9 has the metering function: B, resulting in the new transition 67. Removing the self-loops: 9. Eliminating 1 self-loops for location f32 Self-Loop 6 has the metering function: B, resulting in the new transition 68. Removing the self-loops: 6. Eliminating 1 self-loops for location f1 Self-Loop 11 has the metering function: S1-A, resulting in the new transition 69. Removing the self-loops: 11. Eliminating 5 self-loops for location f13 Self-Loop 41 has unbounded runtime, resulting in the new transition 70. Self-Loop 42 has unbounded runtime, resulting in the new transition 71. Self-Loop 43 has unbounded runtime, resulting in the new transition 72. Self-Loop 44 has unbounded runtime, resulting in the new transition 73. Self-Loop 45 has unbounded runtime, resulting in the new transition 74. Removing the self-loops: 41 42 43 44 45. Eliminating 1 self-loops for location f15 Self-Loop 49 has the metering function: 1+T3, resulting in the new transition 75. Removing the self-loops: 49. Eliminating 1 self-loops for location f17 Self-Loop 53 has the metering function: 1+W3, resulting in the new transition 76. Removing the self-loops: 53. Removed all Self-loops using metering functions (where possible): Start location: f26 65: f29 -> [17] : B'=0, D'=free_8, E'=M, F'=free_6, L'=free_7, N'=1, O'=A, [ A>=free_8 && A>=0 && B>=1 && free_8>=2 ], cost: B 66: f34 -> [18] : C'=1+H+C, D'=free_41, E'=free_38, F'=0, H'=-1, Q'=free_40, L'=free_37, G1'=M, H1'=free_39, Q1'=1+H+C, J1'=-1, [ C>=0 && B>=1 && H>=0 && free_41>=2 ], cost: 1+H 67: f35 -> [19] : B'=0, D'=free_46, E'=free_43, F'=free_45, L'=free_42, K1'=free_44, L1'=1, M1'=C, N1'=H, [ C>=0 && B>=1 && H>=0 && free_46>=2 ], cost: B 68: f32 -> [20] : B'=0, D'=1, E'=M, F'=free_31, L'=free_30, B1'=1, C1'=D1, [ B>=1 ], cost: B 69: f1 -> [21] : A'=S1, T1'=free_54, U1'=free_54, V1'=free_54, W1'=free_53, X1'=-1+S1, [ S1>=1+A && A>=0 ], cost: S1-A 13: f10 -> f13 : B'=free_65, C'=1+G2, D'=free_67, E'=C2, F'=free_66, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_64, L2'=-1+free_64, M2'=H, N2'=G2, [ H>=0 && 0>=free_65 && free_67>=2 && B2==0 && C==0 ], cost: 1 14: f10 -> f13 : B'=free_72, C'=1+G2, D'=free_73, E'=C2, F'=free_69, H'=free_71, M'=free_70, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_71, M2'=H, N2'=G2, O2'=-1+C, P2'=free_71, [ C>=0 && H>=0 && 0>=free_72 && free_73>=2 && B2==0 ], cost: 1 15: f10 -> f13 : B'=free_75, C'=0, D'=free_78, E'=C2, F'=free_77, H'=free_74, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_76, L2'=-1+free_76, M2'=H, Q2_1'=-1+free_74, R2'=-1+free_74, [ H>=0 && 0>=free_75 && free_78>=2 && B2==0 && C==0 ], cost: 1 16: f10 -> f13 : B'=free_81, D'=free_84, E'=C2, F'=free_83, H'=free_80, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_80, M2'=H, O2'=-1+C, P2'=free_80, Q2_1'=-1+free_82, R2'=-1+free_82, [ C>=0 && H>=0 && 0>=free_81 && free_84>=2 && B2==0 ], cost: 1 17: f10 -> f13 : B'=free_86, C'=free_85, D'=free_89, E'=C2, F'=free_88, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_85, J2'=H, K2'=free_87, L2'=-1+free_87, N2'=-1+free_85, Q2_1'=S2, [ H>=0 && 0>=free_86 && free_89>=2 && B2==0 && C==0 ], cost: 1 18: f10 -> f13 : B'=free_92, C'=free_91, D'=free_95, E'=C2, F'=free_94, H'=free_93, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_91, J2'=H, K2'=free_93, N2'=-1+free_91, O2'=-1+C, P2'=free_93, Q2_1'=S2, [ C>=0 && H>=0 && 0>=free_92 && free_95>=2 && B2==0 ], cost: 1 19: f10 -> f13 : B'=free_97, C'=0, D'=free_99, E'=C2, F'=free_98, H'=1+S2, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_96, L2'=-1+free_96, Q2_1'=S2, R2'=S2, [ H>=0 && 0>=free_97 && free_99>=2 && B2==0 && C==0 ], cost: 1 20: f10 -> f13 : B'=free_102, D'=free_104, E'=C2, F'=free_103, H'=free_101, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_101, O2'=-1+C, P2'=free_101, Q2_1'=S2, R2'=S2, [ C>=0 && H>=0 && 0>=free_102 && free_104>=2 && B2==0 ], cost: 1 21: f10 -> f13 : B'=free_106, C'=free_105, D'=free_109, E'=C2, F'=free_108, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_105, J2'=H, K2'=free_107, L2'=-1+free_107, N2'=-1+free_105, T2'=U2, [ free_110>=0 && H>=0 && 0>=free_106 && free_109>=2 && B2==0 && C==0 ], cost: 1 22: f10 -> f13 : B'=free_112, C'=free_111, D'=free_115, E'=C2, F'=free_114, H'=free_113, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_111, J2'=H, K2'=free_113, N2'=-1+free_111, O2'=-1+C, P2'=free_113, T2'=U2, [ C>=0 && H>=0 && 0>=free_112 && free_115>=2 && B2==0 ], cost: 1 23: f10 -> f13 : B'=free_117, C'=0, D'=free_120, E'=C2, F'=free_119, H'=free_116, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_118, L2'=-1+free_118, Q2_1'=-1+free_116, R2'=-1+free_116, T2'=U2, [ free_121>=0 && H>=0 && 0>=free_117 && free_120>=2 && B2==0 && C==0 ], cost: 1 24: f10 -> f13 : B'=free_123, D'=free_126, E'=C2, F'=free_125, H'=free_122, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_122, O2'=-1+C, P2'=free_122, Q2_1'=-1+free_124, R2'=-1+free_124, T2'=U2, [ C>=0 && H>=0 && 0>=free_123 && free_126>=2 && B2==0 ], cost: 1 70: f13 -> [22] : [ free_230>=2 && 0>=free_224 && B2==0 && G2==0 ], cost: INF 71: f13 -> [22] : [ 0>=free_233 && free_239>=2 && B2==0 ], cost: INF 72: f13 -> [22] : [ free_247>=2 && 0>=free_245 && B2==0 ], cost: INF 73: f13 -> [22] : [ free_255>=2 && 0>=free_250 && B2==0 ], cost: INF 74: f13 -> [22] : [ free_264>=2 && 0>=free_258 && B2==0 ], cost: INF 75: f15 -> [23] : B'=free_288, D'=free_289, E'=free_287, F'=0, Q'=free_286, M'=0, B2'=0, D2'=free_287, E2'=0, F2'=free_287, H2'=C2, T3'=-1, U3'=-1, [ T3>=0 && free_288>=1 && free_289>=2 && B2==0 ], cost: 1+T3 76: f17 -> [24] : B'=free_315, D'=free_316, E'=free_314, Q'=free_313, M'=free_314, B2'=0, D2'=free_314, E2'=0, F2'=free_314, H2'=C2, W3'=-1, X3'=-1, [ W3>=0 && free_316>=2 && 0>=free_315 && B2==0 ], cost: 1+W3 61: f26 -> f32 : A'=free_361, D'=1, E'=U1, L'=free_357, M'=U1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [], cost: 1 60: f26 -> f1 : A'=2, D'=free_352, L'=free_349, S1'=free_352, T1'=free_351, U1'=free_348, V1'=free_351, Y1'=free_351, Z3'=free_350, A4'=2, [ free_352>=2 ], cost: 1 0: [17] -> f34 : C'=1, D'=free_4, E'=free_1, F'=0, G'=H, Q'=free_3, J'=1+H, K'=free, L'=free_2, [ A>=0 && B>=1 && free_4>=2 && C==1 ], cost: 1 55: [17] -> f17 : B'=free_327, D'=free_328, M'=E, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, V3'=W3, Y3'=1+W3, [ A>=free_331 && A>=0 && 0>=B && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 ], cost: 1 7: [18] -> f35 : B'=-1+free_35, D'=free_36, E'=free_33, F'=free_32, L'=free_34, E1'=free_35, F1'=-1+free_35, [ C>=0 && B>=1 && H>=0 && free_35>=1 && free_36>=2 ], cost: 1 58: [18] -> f15 : B'=free_340, C'=1+T3, D'=free_341, F'=0, M'=0, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, H2'=E, S3'=T3, [ H>=0 && C>=0 && free_343>=1 && free_342>=2 && free_340>=1 && free_341>=2 && M==0 ], cost: 1 10: [19] -> f34 : C'=1+C, D'=free_52, E'=free_49, F'=0, H'=-1+H, Q'=free_51, L'=free_48, K1'=free_50, O1'=M, P1'=free_47, Q1_1'=1+C, R1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_52>=2 ], cost: 1 59: [19] -> f10 : B'=free_346, D'=free_347, F'=free_344, M'=free_345, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, [ 0>=B && H>=0 && C>=0 && free_347>=2 && 0>=free_346 ], cost: 1 12: [21] -> f29 : A'=free_59, D'=free_63, E'=T1, M'=T1, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, Y1'=free_60, Z1'=free_55, A2'=free_58, [ A>=S1 && A>=0 && free_59>=free_63 && free_63>=2 ], cost: 1 Applied simple chaining: Start location: f26 66: f34 -> [18] : C'=1+H+C, D'=free_41, E'=free_38, F'=0, H'=-1, Q'=free_40, L'=free_37, G1'=M, H1'=free_39, Q1'=1+H+C, J1'=-1, [ C>=0 && B>=1 && H>=0 && free_41>=2 ], cost: 1+H 13: f10 -> f13 : B'=free_65, C'=1+G2, D'=free_67, E'=C2, F'=free_66, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_64, L2'=-1+free_64, M2'=H, N2'=G2, [ H>=0 && 0>=free_65 && free_67>=2 && B2==0 && C==0 ], cost: 1 14: f10 -> f13 : B'=free_72, C'=1+G2, D'=free_73, E'=C2, F'=free_69, H'=free_71, M'=free_70, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, J2'=H, K2'=free_71, M2'=H, N2'=G2, O2'=-1+C, P2'=free_71, [ C>=0 && H>=0 && 0>=free_72 && free_73>=2 && B2==0 ], cost: 1 15: f10 -> f13 : B'=free_75, C'=0, D'=free_78, E'=C2, F'=free_77, H'=free_74, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_76, L2'=-1+free_76, M2'=H, Q2_1'=-1+free_74, R2'=-1+free_74, [ H>=0 && 0>=free_75 && free_78>=2 && B2==0 && C==0 ], cost: 1 16: f10 -> f13 : B'=free_81, D'=free_84, E'=C2, F'=free_83, H'=free_80, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=G2, K2'=free_80, M2'=H, O2'=-1+C, P2'=free_80, Q2_1'=-1+free_82, R2'=-1+free_82, [ C>=0 && H>=0 && 0>=free_81 && free_84>=2 && B2==0 ], cost: 1 17: f10 -> f13 : B'=free_86, C'=free_85, D'=free_89, E'=C2, F'=free_88, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_85, J2'=H, K2'=free_87, L2'=-1+free_87, N2'=-1+free_85, Q2_1'=S2, [ H>=0 && 0>=free_86 && free_89>=2 && B2==0 && C==0 ], cost: 1 18: f10 -> f13 : B'=free_92, C'=free_91, D'=free_95, E'=C2, F'=free_94, H'=free_93, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_91, J2'=H, K2'=free_93, N2'=-1+free_91, O2'=-1+C, P2'=free_93, Q2_1'=S2, [ C>=0 && H>=0 && 0>=free_92 && free_95>=2 && B2==0 ], cost: 1 19: f10 -> f13 : B'=free_97, C'=0, D'=free_99, E'=C2, F'=free_98, H'=1+S2, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_96, L2'=-1+free_96, Q2_1'=S2, R2'=S2, [ H>=0 && 0>=free_97 && free_99>=2 && B2==0 && C==0 ], cost: 1 20: f10 -> f13 : B'=free_102, D'=free_104, E'=C2, F'=free_103, H'=free_101, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_101, O2'=-1+C, P2'=free_101, Q2_1'=S2, R2'=S2, [ C>=0 && H>=0 && 0>=free_102 && free_104>=2 && B2==0 ], cost: 1 21: f10 -> f13 : B'=free_106, C'=free_105, D'=free_109, E'=C2, F'=free_108, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_105, J2'=H, K2'=free_107, L2'=-1+free_107, N2'=-1+free_105, T2'=U2, [ free_110>=0 && H>=0 && 0>=free_106 && free_109>=2 && B2==0 && C==0 ], cost: 1 22: f10 -> f13 : B'=free_112, C'=free_111, D'=free_115, E'=C2, F'=free_114, H'=free_113, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, Q2'=-1+free_111, J2'=H, K2'=free_113, N2'=-1+free_111, O2'=-1+C, P2'=free_113, T2'=U2, [ C>=0 && H>=0 && 0>=free_112 && free_115>=2 && B2==0 ], cost: 1 23: f10 -> f13 : B'=free_117, C'=0, D'=free_120, E'=C2, F'=free_119, H'=free_116, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_118, L2'=-1+free_118, Q2_1'=-1+free_116, R2'=-1+free_116, T2'=U2, [ free_121>=0 && H>=0 && 0>=free_117 && free_120>=2 && B2==0 && C==0 ], cost: 1 24: f10 -> f13 : B'=free_123, D'=free_126, E'=C2, F'=free_125, H'=free_122, M'=C2, B2'=0, D2'=C2, E2'=0, F2'=C2, H2'=C2, K2'=free_122, O2'=-1+C, P2'=free_122, Q2_1'=-1+free_124, R2'=-1+free_124, T2'=U2, [ C>=0 && H>=0 && 0>=free_123 && free_126>=2 && B2==0 ], cost: 1 70: f13 -> [22] : [ free_230>=2 && 0>=free_224 && B2==0 && G2==0 ], cost: INF 71: f13 -> [22] : [ 0>=free_233 && free_239>=2 && B2==0 ], cost: INF 72: f13 -> [22] : [ free_247>=2 && 0>=free_245 && B2==0 ], cost: INF 73: f13 -> [22] : [ free_255>=2 && 0>=free_250 && B2==0 ], cost: INF 74: f13 -> [22] : [ free_264>=2 && 0>=free_258 && B2==0 ], cost: INF 60: f26 -> [17] : A'=free_59, B'=0, D'=free_8, E'=free_54, F'=free_6, L'=free_7, M'=free_54, N'=1, O'=free_59, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, W1'=free_53, X1'=-1+free_352, Y1'=free_60, Z1'=free_55, A2'=free_58, Z3'=free_350, A4'=2, [ free_352>=2 && free_352>=3 && 2>=0 && free_352>=free_352 && free_352>=0 && free_59>=free_63 && free_63>=2 && free_59>=free_8 && free_59>=0 && B>=1 && free_8>=2 ], cost: B+free_352 61: f26 -> [20] : A'=free_361, B'=0, D'=1, E'=U1, F'=free_31, L'=free_30, M'=U1, B1'=1, C1'=D1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [ B>=1 ], cost: 1+B 0: [17] -> f34 : C'=1, D'=free_4, E'=free_1, F'=0, G'=H, Q'=free_3, J'=1+H, K'=free, L'=free_2, [ A>=0 && B>=1 && free_4>=2 && C==1 ], cost: 1 55: [17] -> [24] : B'=free_315, D'=free_316, E'=free_314, Q'=free_313, M'=free_314, B2'=0, C2'=E, D2'=free_314, E2'=0, F2'=free_314, H2'=E, V3'=W3, W3'=-1, X3'=-1, Y3'=1+W3, [ A>=free_331 && A>=0 && 0>=B && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 && W3>=0 && free_316>=2 && 0>=free_315 && 0==0 ], cost: 2+W3 7: [18] -> [19] : B'=0, D'=free_46, E'=free_43, F'=free_45, L'=free_42, E1'=free_35, F1'=-1+free_35, K1'=free_44, L1'=1, M1'=C, N1'=H, [ C>=0 && B>=1 && H>=0 && free_35>=1 && free_36>=2 && C>=0 && -1+free_35>=1 && H>=0 && free_46>=2 ], cost: free_35 58: [18] -> [23] : B'=free_288, C'=1+T3, D'=free_289, E'=free_287, F'=0, Q'=free_286, M'=0, B2'=0, C2'=E, D2'=free_287, E2'=0, F2'=free_287, H2'=E, S3'=T3, T3'=-1, U3'=-1, [ H>=0 && C>=0 && free_343>=1 && free_342>=2 && free_340>=1 && free_341>=2 && M==0 && T3>=0 && free_288>=1 && free_289>=2 && 0==0 ], cost: 2+T3 10: [19] -> f34 : C'=1+C, D'=free_52, E'=free_49, F'=0, H'=-1+H, Q'=free_51, L'=free_48, K1'=free_50, O1'=M, P1'=free_47, Q1_1'=1+C, R1'=-1+H, [ C>=0 && B>=1 && H>=0 && free_52>=2 ], cost: 1 59: [19] -> f10 : B'=free_346, D'=free_347, F'=free_344, M'=free_345, B2'=0, C2'=E, D2'=E, E2'=0, F2'=E, [ 0>=B && H>=0 && C>=0 && free_347>=2 && 0>=free_346 ], cost: 1 Applied chaining over branches and pruning: Start location: f26 61: f26 -> [20] : A'=free_361, B'=0, D'=1, E'=U1, F'=free_31, L'=free_30, M'=U1, B1'=1, C1'=D1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [ B>=1 ], cost: 1+B 78: f26 -> [24] : A'=free_59, B'=free_315, D'=free_316, E'=free_314, F'=free_6, Q'=free_313, L'=free_7, M'=free_314, N'=1, O'=free_59, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, W1'=free_53, X1'=-1+free_352, Y1'=free_60, Z1'=free_55, A2'=free_58, B2'=0, C2'=free_54, D2'=free_314, E2'=0, F2'=free_314, H2'=free_54, V3'=W3, W3'=-1, X3'=-1, Y3'=1+W3, Z3'=free_350, A4'=2, [ free_352>=2 && free_352>=3 && 2>=0 && free_352>=free_352 && free_352>=0 && free_59>=free_63 && free_63>=2 && free_59>=free_8 && free_59>=0 && B>=1 && free_8>=2 && free_59>=free_331 && free_59>=0 && 0>=0 && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 && W3>=0 && free_316>=2 && 0>=free_315 && 0==0 ], cost: 2+B+free_352+W3 77: f26 -> [25] : A'=free_59, B'=0, D'=free_8, E'=free_54, F'=free_6, L'=free_7, M'=free_54, N'=1, O'=free_59, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, W1'=free_53, X1'=-1+free_352, Y1'=free_60, Z1'=free_55, A2'=free_58, Z3'=free_350, A4'=2, [ free_352>=2 && free_352>=3 && 2>=0 && free_352>=free_352 && free_352>=0 && free_59>=free_63 && free_63>=2 && free_59>=free_8 && free_59>=0 && B>=1 && free_8>=2 ], cost: B+free_352 Final control flow graph problem, now checking costs for infinitely many models: Start location: f26 61: f26 -> [20] : A'=free_361, B'=0, D'=1, E'=U1, F'=free_31, L'=free_30, M'=U1, B1'=1, C1'=D1, S1'=free_359, T1'=free_355, U1'=free_360, V1'=free_354, Y1'=free_358, Z1'=free_353, A2'=free_356, [ B>=1 ], cost: 1+B 78: f26 -> [24] : A'=free_59, B'=free_315, D'=free_316, E'=free_314, F'=free_6, Q'=free_313, L'=free_7, M'=free_314, N'=1, O'=free_59, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, W1'=free_53, X1'=-1+free_352, Y1'=free_60, Z1'=free_55, A2'=free_58, B2'=0, C2'=free_54, D2'=free_314, E2'=0, F2'=free_314, H2'=free_54, V3'=W3, W3'=-1, X3'=-1, Y3'=1+W3, Z3'=free_350, A4'=2, [ free_352>=2 && free_352>=3 && 2>=0 && free_352>=free_352 && free_352>=0 && free_59>=free_63 && free_63>=2 && free_59>=free_8 && free_59>=0 && B>=1 && free_8>=2 && free_59>=free_331 && free_59>=0 && 0>=0 && free_329>=free_328 && 0>=free_330 && free_331>=2 && 0>=free_327 && free_328>=2 && W3>=0 && free_316>=2 && 0>=free_315 && 0==0 ], cost: 2+B+free_352+W3 77: f26 -> [25] : A'=free_59, B'=0, D'=free_8, E'=free_54, F'=free_6, L'=free_7, M'=free_54, N'=1, O'=free_59, S1'=free_61, T1'=free_57, U1'=free_62, V1'=free_56, W1'=free_53, X1'=-1+free_352, Y1'=free_60, Z1'=free_55, A2'=free_58, Z3'=free_350, A4'=2, [ free_352>=2 && free_352>=3 && 2>=0 && free_352>=free_352 && free_352>=0 && free_59>=free_63 && free_63>=2 && free_59>=free_8 && free_59>=0 && B>=1 && free_8>=2 ], cost: B+free_352 Computing complexity for remaining 3 transitions. Found configuration with infinitely models for cost: 1+B and guard: B>=1: B: Pos Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: B>=1 Final Cost: 1+B Obtained the following complexity w.r.t. the length of the input n: Complexity class: n^1 Complexity value: 1 WORST_CASE(Omega(n^1),?)