Trying to load file: main.koat Initial Control flow graph problem: Start location: f2 0: f2 -> f5 : [], cost: 1 1: f5 -> f8 : [ A>=B ], cost: 1 41: f5 -> f17 : [ B>=1+A ], cost: 1 40: f8 -> f5 : B'=1+B, [ C>=1+A ], cost: 1 2: f8 -> f8 : C'=1+C, [ A>=C ], cost: 1 3: f17 -> f17 : B'=1+B, D'=free, [ A>=B ], cost: 1 39: f17 -> f27 : [ B>=1+A ], cost: 1 4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1 38: f27 -> f1 : [ E>=51 ], cost: 1 5: f31 -> f34 : [ A>=1+B ], cost: 1 35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1 36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1 37: f31 -> f1 : F'=0, [ B>=A && F==0 ], cost: 1 34: f34 -> f31 : B'=1+B, [ C>=1+A ], cost: 1 6: f34 -> f34 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1 7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1 8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1 9: f50 -> f53 : [ A>=1+B ], cost: 1 33: f50 -> f132 : [ B>=A ], cost: 1 32: f53 -> f50 : B'=1+B, [ C>=1+A ], cost: 1 11: f53 -> f53 : C'=1+C, J'=free_3, K'=100*free_3, L'=free_4, M'=100*free_3+free_4, N'=free_5, O'=100*free_3+free_5, [ A>=C && E>=5 ], cost: 1 12: f53 -> f69 : Q'=free_7, J'=free_6, K'=100*free_6, [ A>=C && 4>=E ], cost: 1 13: f53 -> f69 : Q'=free_10, J'=free_9, K'=100*free_9, L'=free_11, M'=free_11+100*free_9, N'=free_12, O'=free_8, [ E>=5 && A>=C && free_8>=1+free_12+100*free_9 ], cost: 1 14: f53 -> f69 : Q'=free_15, J'=free_14, K'=100*free_14, L'=free_16, M'=free_16+100*free_14, N'=free_17, O'=free_13, [ E>=5 && A>=C && free_17+100*free_14>=1+free_13 ], cost: 1 15: f53 -> f69 : Q'=free_18, J'=free_19, K'=100*free_19, L'=free_20, M'=free_21, [ E>=5 && A>=C && free_21>=1+100*free_19+free_20 ], cost: 1 16: f53 -> f69 : Q'=free_22, J'=free_23, K'=100*free_23, L'=free_24, M'=free_25, [ E>=5 && A>=C && 100*free_23+free_24>=1+free_25 ], cost: 1 10: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1 17: f69 -> f80 : P'=-free_31+free_28, Q_1'=free_33, R'=free_27, S'=free_30, T'=free_26, U'=free_32, V'=free_29, [ free_27>=1+K+free_33 && 1>=free_32*free_34+free_29*free_34 && free_32*free_34+free_34+free_29*free_34>=2 && free_30>=free_34 && 1>=free_29*free_35+free_32*free_35 && free_29*free_35+free_32*free_35+free_35>=2 && free_35>=free_30 && Q>=1+H ], cost: 1 18: f69 -> f80 : P'=-free_41+free_38, Q_1'=free_43, R'=free_37, S'=free_40, T'=free_36, U'=free_42, V'=free_39, [ K+free_43>=1+free_37 && 1>=free_39*free_44+free_42*free_44 && free_39*free_44+free_42*free_44+free_44>=2 && free_40>=free_44 && 1>=free_42*free_45+free_45*free_39 && free_45+free_42*free_45+free_45*free_39>=2 && free_45>=free_40 && Q>=1+H ], cost: 1 20: f69 -> f92 : P'=free_63, Q_1'=free_65, R'=K+free_65, S'=free_67, W'=free_62, X'=free_64, Y'=free_61, Z'=free_66, [ free_71>=free_71*free_81*free_62 && free_71*free_81*free_62+free_81>=1+free_71 && free_79>=free_79*free_62*free_91 && free_79*free_62*free_91+free_91>=1+free_79 && free_68>=free_89*free_68*free_62 && free_89+free_89*free_68*free_62>=1+free_68 && free_89*free_77+free_81>=free_77*free_91 && free_77+free_77*free_91>=1+free_89*free_77+free_81 && free_77>=free_61 && free_71>=free_71*free_87*free_62 && free_87+free_71*free_87*free_62>=1+free_71 && free_79>=free_79*free_62*free_95 && free_79*free_62*free_95+free_95>=1+free_79 && free_68>=free_73*free_68*free_62 && free_73+free_73*free_68*free_62>=1+free_68 && free_73*free_83+free_87>=free_83*free_95 && free_83*free_95+free_83>=1+free_73*free_83+free_87 && free_61>=free_83 && free_71>=free_96*free_71*free_62 && free_96*free_71*free_62+free_96>=1+free_71 && free_79>=free_79*free_62*free_75 && free_79*free_62*free_75+free_75>=1+free_79 && free_68>=free_85*free_68*free_62 && free_85+free_85*free_68*free_62>=1+free_68 && free_85*free_94+free_96>=free_94*free_75 && free_94*free_75+free_94>=1+free_85*free_94+free_96 && 1>=free_62*free_72 && free_62*free_72+free_72>=2 && free_94>=free_82+free_82*free_72 && 2*free_82+free_82*free_72>=1+free_94 && free_82>=free_66 && free_71>=free_92*free_71*free_62 && free_92*free_71*free_62+free_92>=1+free_71 && free_79>=free_79*free_70*free_62 && free_79*free_70*free_62+free_70>=1+free_79 && free_68>=free_80*free_68*free_62 && free_80*free_68*free_62+free_80>=1+free_68 && free_92+free_80*free_90>=free_70*free_90 && free_70*free_90+free_90>=1+free_92+free_80*free_90 && 1>=free_62*free_69 && free_62*free_69+free_69>=2 && free_90>=free_78+free_78*free_69 && 2*free_78+free_78*free_69>=1+free_90 && free_66>=free_78 && free_68*free_88+free_71>=free_79*free_88 && free_79*free_88+free_88>=1+free_68*free_88+free_71 && free_88>=free_67 && free_97*free_68+free_71>=free_79*free_97 && free_97+free_79*free_97>=1+free_97*free_68+free_71 && free_67>=free_97 && free_76*free_71+free_76*free_86*free_68>=free_76*free_79*free_86 && free_86+free_76*free_79*free_86>=1+free_76*free_71+free_76*free_86*free_68 && free_86>=free_63 && free_76*free_71+free_76*free_74*free_68>=free_76*free_79*free_74 && free_76*free_79*free_74+free_74>=1+free_76*free_71+free_76*free_74*free_68 && free_63>=free_74 && 1>=free_84*free_62 && free_84*free_62+free_84>=2 && free_64>=free_84 && 1>=free_93*free_62 && free_93+free_93*free_62>=2 && free_93>=free_64 && Q>=1+H ], cost: 1 19: f80 -> f92 : P'=S*free_47, W'=free_49, X'=free_50, Y'=free_46, Z'=free_48, [ T>=0 && S>=free_52*free_49*S && free_52+free_52*free_49*S>=1+S && free_52>=free_46 && S>=free_49*S*free_60 && free_60+free_49*S*free_60>=1+S && free_46>=free_60 && 1>=free_49*free_56 && free_56+free_49*free_56>=2 && free_50>=free_56 && 1>=free_49*free_53 && free_53+free_49*free_53>=2 && free_53>=free_50 && S>=free_49*free_59*S && free_49*free_59*S+free_59>=1+S && 1>=free_55*free_49 && free_55+free_55*free_49>=2 && free_59>=free_58*free_55+free_58 && free_58*free_55+2*free_58>=1+free_59 && free_58>=free_48 && S>=free_51*free_49*S && free_51+free_51*free_49*S>=1+S && 1>=free_49*free_54 && free_49*free_54+free_54>=2 && free_51>=free_57*free_54+free_57 && free_57*free_54+2*free_57>=1+free_51 && free_48>=free_57 ], cost: 1 21: f80 -> f92 : P'=-free_99*S, S'=-S, W'=free_101, X'=free_102, Y'=-S*free_98, Z'=free_100, [ 1>=free_101*free_98 && free_101*free_98+free_98>=2 && 0>=1+T && 1>=free_104*free_101 && free_104+free_104*free_101>=2 && free_102>=free_104 && 1>=free_110*free_101 && free_110*free_101+free_110>=2 && free_110>=free_102 && 1>=free_107*free_101 && free_107*free_101+free_107>=2 && 1>=free_105*free_101 && free_105+free_105*free_101>=2 && 0>=free_109+S*free_107+free_105*free_109 && 2*free_109+S*free_107+free_105*free_109>=1 && free_100>=free_109 && 1>=free_106*free_101 && free_106+free_106*free_101>=2 && 1>=free_108*free_101 && free_108+free_108*free_101>=2 && 0>=free_103+free_106*S+free_108*free_103 && 2*free_103+free_106*S+free_108*free_103>=1 && free_103>=free_100 ], cost: 1 22: f92 -> f92 : K'=free_111, P'=free_112, A1'=1+A1, [ B>=1+A1 ], cost: 1 31: f92 -> f101 : [ A1>=B ], cost: 1 23: f101 -> f101 : K'=free_113, P'=free_114, A1'=1+A1, [ C>=1+A1 ], cost: 1 30: f101 -> f110 : [ A1>=C ], cost: 1 24: f110 -> f110 : K'=free_115, P'=free_116, A1'=1+A1, [ A>=A1 ], cost: 1 29: f110 -> f119 : [ A1>=1+A ], cost: 1 28: f119 -> f53 : C'=1+C, [ A1>=1+A ], cost: 1 25: f119 -> f119 : K'=free_117, P'=free_118, A1'=1+A1, [ A>=A1 ], cost: 1 27: f132 -> f27 : E'=1+E, [ B>=1+A ], cost: 1 26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1 Simplified the transitions: Start location: f2 0: f2 -> f5 : [], cost: 1 1: f5 -> f8 : [ A>=B ], cost: 1 41: f5 -> f17 : [ B>=1+A ], cost: 1 40: f8 -> f5 : B'=1+B, [ C>=1+A ], cost: 1 2: f8 -> f8 : C'=1+C, [ A>=C ], cost: 1 3: f17 -> f17 : B'=1+B, D'=free, [ A>=B ], cost: 1 39: f17 -> f27 : [ B>=1+A ], cost: 1 4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1 5: f31 -> f34 : [ A>=1+B ], cost: 1 35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1 36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1 34: f34 -> f31 : B'=1+B, [ C>=1+A ], cost: 1 6: f34 -> f34 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1 7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1 8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1 9: f50 -> f53 : [ A>=1+B ], cost: 1 33: f50 -> f132 : [ B>=A ], cost: 1 32: f53 -> f50 : B'=1+B, [ C>=1+A ], cost: 1 11: f53 -> f53 : C'=1+C, J'=free_3, K'=100*free_3, L'=free_4, M'=100*free_3+free_4, N'=free_5, O'=100*free_3+free_5, [ A>=C && E>=5 ], cost: 1 12: f53 -> f69 : Q'=free_7, J'=free_6, K'=100*free_6, [ A>=C && 4>=E ], cost: 1 13: f53 -> f69 : Q'=free_10, J'=free_9, K'=100*free_9, L'=free_11, M'=free_11+100*free_9, N'=free_12, O'=free_8, [ E>=5 && A>=C && free_8>=1+free_12+100*free_9 ], cost: 1 14: f53 -> f69 : Q'=free_15, J'=free_14, K'=100*free_14, L'=free_16, M'=free_16+100*free_14, N'=free_17, O'=free_13, [ E>=5 && A>=C && free_17+100*free_14>=1+free_13 ], cost: 1 15: f53 -> f69 : Q'=free_18, J'=free_19, K'=100*free_19, L'=free_20, M'=free_21, [ E>=5 && A>=C && free_21>=1+100*free_19+free_20 ], cost: 1 16: f53 -> f69 : Q'=free_22, J'=free_23, K'=100*free_23, L'=free_24, M'=free_25, [ E>=5 && A>=C && 100*free_23+free_24>=1+free_25 ], cost: 1 10: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1 17: f69 -> f80 : P'=-free_31+free_28, Q_1'=free_33, R'=free_27, S'=free_30, T'=free_26, U'=free_32, V'=free_29, [ free_27>=1+K+free_33 && 1>=free_32*free_34+free_29*free_34 && free_32*free_34+free_34+free_29*free_34>=2 && free_30>=free_34 && 1>=free_29*free_35+free_32*free_35 && free_29*free_35+free_32*free_35+free_35>=2 && free_35>=free_30 && Q>=1+H ], cost: 1 18: f69 -> f80 : P'=-free_41+free_38, Q_1'=free_43, R'=free_37, S'=free_40, T'=free_36, U'=free_42, V'=free_39, [ K+free_43>=1+free_37 && 1>=free_39*free_44+free_42*free_44 && free_39*free_44+free_42*free_44+free_44>=2 && free_40>=free_44 && 1>=free_42*free_45+free_45*free_39 && free_45+free_42*free_45+free_45*free_39>=2 && free_45>=free_40 && Q>=1+H ], cost: 1 20: f69 -> f92 : P'=free_63, Q_1'=free_65, R'=K+free_65, S'=free_67, W'=free_62, X'=free_64, Y'=free_61, Z'=free_66, [ free_71>=free_71*free_81*free_62 && free_71*free_81*free_62+free_81>=1+free_71 && free_79>=free_79*free_62*free_91 && free_79*free_62*free_91+free_91>=1+free_79 && free_68>=free_89*free_68*free_62 && free_89+free_89*free_68*free_62>=1+free_68 && free_89*free_77+free_81>=free_77*free_91 && free_77+free_77*free_91>=1+free_89*free_77+free_81 && free_77>=free_61 && free_71>=free_71*free_87*free_62 && free_87+free_71*free_87*free_62>=1+free_71 && free_79>=free_79*free_62*free_95 && free_79*free_62*free_95+free_95>=1+free_79 && free_68>=free_73*free_68*free_62 && free_73+free_73*free_68*free_62>=1+free_68 && free_73*free_83+free_87>=free_83*free_95 && free_83*free_95+free_83>=1+free_73*free_83+free_87 && free_61>=free_83 && free_71>=free_96*free_71*free_62 && free_96*free_71*free_62+free_96>=1+free_71 && free_79>=free_79*free_62*free_75 && free_79*free_62*free_75+free_75>=1+free_79 && free_68>=free_85*free_68*free_62 && free_85+free_85*free_68*free_62>=1+free_68 && free_85*free_94+free_96>=free_94*free_75 && free_94*free_75+free_94>=1+free_85*free_94+free_96 && 1>=free_62*free_72 && free_62*free_72+free_72>=2 && free_94>=free_82+free_82*free_72 && 2*free_82+free_82*free_72>=1+free_94 && free_82>=free_66 && free_71>=free_92*free_71*free_62 && free_92*free_71*free_62+free_92>=1+free_71 && free_79>=free_79*free_70*free_62 && free_79*free_70*free_62+free_70>=1+free_79 && free_68>=free_80*free_68*free_62 && free_80*free_68*free_62+free_80>=1+free_68 && free_92+free_80*free_90>=free_70*free_90 && free_70*free_90+free_90>=1+free_92+free_80*free_90 && 1>=free_62*free_69 && free_62*free_69+free_69>=2 && free_90>=free_78+free_78*free_69 && 2*free_78+free_78*free_69>=1+free_90 && free_66>=free_78 && free_68*free_88+free_71>=free_79*free_88 && free_79*free_88+free_88>=1+free_68*free_88+free_71 && free_88>=free_67 && free_97*free_68+free_71>=free_79*free_97 && free_97+free_79*free_97>=1+free_97*free_68+free_71 && free_67>=free_97 && free_76*free_71+free_76*free_86*free_68>=free_76*free_79*free_86 && free_86+free_76*free_79*free_86>=1+free_76*free_71+free_76*free_86*free_68 && free_86>=free_63 && free_76*free_71+free_76*free_74*free_68>=free_76*free_79*free_74 && free_76*free_79*free_74+free_74>=1+free_76*free_71+free_76*free_74*free_68 && free_63>=free_74 && 1>=free_84*free_62 && free_84*free_62+free_84>=2 && free_64>=free_84 && 1>=free_93*free_62 && free_93+free_93*free_62>=2 && free_93>=free_64 && Q>=1+H ], cost: 1 19: f80 -> f92 : P'=S*free_47, W'=free_49, X'=free_50, Y'=free_46, Z'=free_48, [ T>=0 && S>=free_52*free_49*S && free_52+free_52*free_49*S>=1+S && free_52>=free_46 && S>=free_49*S*free_60 && free_60+free_49*S*free_60>=1+S && free_46>=free_60 && 1>=free_49*free_56 && free_56+free_49*free_56>=2 && free_50>=free_56 && 1>=free_49*free_53 && free_53+free_49*free_53>=2 && free_53>=free_50 && S>=free_49*free_59*S && free_49*free_59*S+free_59>=1+S && 1>=free_55*free_49 && free_55+free_55*free_49>=2 && free_59>=free_58*free_55+free_58 && free_58*free_55+2*free_58>=1+free_59 && free_58>=free_48 && S>=free_51*free_49*S && free_51+free_51*free_49*S>=1+S && 1>=free_49*free_54 && free_49*free_54+free_54>=2 && free_51>=free_57*free_54+free_57 && free_57*free_54+2*free_57>=1+free_51 && free_48>=free_57 ], cost: 1 21: f80 -> f92 : P'=-free_99*S, S'=-S, W'=free_101, X'=free_102, Y'=-S*free_98, Z'=free_100, [ 1>=free_101*free_98 && free_101*free_98+free_98>=2 && 0>=1+T && 1>=free_104*free_101 && free_104+free_104*free_101>=2 && free_102>=free_104 && 1>=free_110*free_101 && free_110*free_101+free_110>=2 && free_110>=free_102 && 1>=free_107*free_101 && free_107*free_101+free_107>=2 && 1>=free_105*free_101 && free_105+free_105*free_101>=2 && 0>=free_109+S*free_107+free_105*free_109 && 2*free_109+S*free_107+free_105*free_109>=1 && free_100>=free_109 && 1>=free_106*free_101 && free_106+free_106*free_101>=2 && 1>=free_108*free_101 && free_108+free_108*free_101>=2 && 0>=free_103+free_106*S+free_108*free_103 && 2*free_103+free_106*S+free_108*free_103>=1 && free_103>=free_100 ], cost: 1 22: f92 -> f92 : K'=free_111, P'=free_112, A1'=1+A1, [ B>=1+A1 ], cost: 1 31: f92 -> f101 : [ A1>=B ], cost: 1 23: f101 -> f101 : K'=free_113, P'=free_114, A1'=1+A1, [ C>=1+A1 ], cost: 1 30: f101 -> f110 : [ A1>=C ], cost: 1 24: f110 -> f110 : K'=free_115, P'=free_116, A1'=1+A1, [ A>=A1 ], cost: 1 29: f110 -> f119 : [ A1>=1+A ], cost: 1 28: f119 -> f53 : C'=1+C, [ A1>=1+A ], cost: 1 25: f119 -> f119 : K'=free_117, P'=free_118, A1'=1+A1, [ A>=A1 ], cost: 1 27: f132 -> f27 : E'=1+E, [ B>=1+A ], cost: 1 26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1 Eliminating 1 self-loops for location f8 Self-Loop 2 has the metering function: 1-C+A, resulting in the new transition 42. Removing the self-loops: 2. Eliminating 1 self-loops for location f17 Self-Loop 3 has the metering function: 1-B+A, resulting in the new transition 43. Removing the self-loops: 3. Eliminating 1 self-loops for location f34 Self-Loop 6 has the metering function: 1-C+A, resulting in the new transition 44. Removing the self-loops: 6. Eliminating 1 self-loops for location f53 Self-Loop 11 has the metering function: 1-C+A, resulting in the new transition 45. Removing the self-loops: 11. Eliminating 1 self-loops for location f92 Self-Loop 22 has the metering function: -A1+B, resulting in the new transition 46. Removing the self-loops: 22. Eliminating 1 self-loops for location f101 Self-Loop 23 has the metering function: -A1+C, resulting in the new transition 47. Removing the self-loops: 23. Eliminating 1 self-loops for location f110 Self-Loop 24 has the metering function: 1-A1+A, resulting in the new transition 48. Removing the self-loops: 24. Eliminating 1 self-loops for location f119 Self-Loop 25 has the metering function: 1-A1+A, resulting in the new transition 49. Removing the self-loops: 25. Eliminating 1 self-loops for location f132 Self-Loop 26 has the metering function: 1-B+A, resulting in the new transition 50. Removing the self-loops: 26. Removed all Self-loops using metering functions (where possible): Start location: f2 0: f2 -> f5 : [], cost: 1 1: f5 -> f8 : [ A>=B ], cost: 1 41: f5 -> f17 : [ B>=1+A ], cost: 1 42: f8 -> [18] : C'=1+A, [ A>=C ], cost: 1-C+A 43: f17 -> [19] : B'=1+A, D'=free, [ A>=B ], cost: 1-B+A 4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1 5: f31 -> f34 : [ A>=1+B ], cost: 1 35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1 36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1 44: f34 -> [20] : C'=1+A, F'=-free_1*(-1+C-A)+F, G'=free_1, [ A>=C ], cost: 1-C+A 7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1 8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1 9: f50 -> f53 : [ A>=1+B ], cost: 1 33: f50 -> f132 : [ B>=A ], cost: 1 45: f53 -> [21] : C'=1+A, J'=free_3, K'=100*free_3, L'=free_4, M'=100*free_3+free_4, N'=free_5, O'=100*free_3+free_5, [ A>=C && E>=5 ], cost: 1-C+A 10: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1 17: f69 -> f80 : P'=-free_31+free_28, Q_1'=free_33, R'=free_27, S'=free_30, T'=free_26, U'=free_32, V'=free_29, [ free_27>=1+K+free_33 && 1>=free_32*free_34+free_29*free_34 && free_32*free_34+free_34+free_29*free_34>=2 && free_30>=free_34 && 1>=free_29*free_35+free_32*free_35 && free_29*free_35+free_32*free_35+free_35>=2 && free_35>=free_30 && Q>=1+H ], cost: 1 18: f69 -> f80 : P'=-free_41+free_38, Q_1'=free_43, R'=free_37, S'=free_40, T'=free_36, U'=free_42, V'=free_39, [ K+free_43>=1+free_37 && 1>=free_39*free_44+free_42*free_44 && free_39*free_44+free_42*free_44+free_44>=2 && free_40>=free_44 && 1>=free_42*free_45+free_45*free_39 && free_45+free_42*free_45+free_45*free_39>=2 && free_45>=free_40 && Q>=1+H ], cost: 1 20: f69 -> f92 : P'=free_63, Q_1'=free_65, R'=K+free_65, S'=free_67, W'=free_62, X'=free_64, Y'=free_61, Z'=free_66, [ free_71>=free_71*free_81*free_62 && free_71*free_81*free_62+free_81>=1+free_71 && free_79>=free_79*free_62*free_91 && free_79*free_62*free_91+free_91>=1+free_79 && free_68>=free_89*free_68*free_62 && free_89+free_89*free_68*free_62>=1+free_68 && free_89*free_77+free_81>=free_77*free_91 && free_77+free_77*free_91>=1+free_89*free_77+free_81 && free_77>=free_61 && free_71>=free_71*free_87*free_62 && free_87+free_71*free_87*free_62>=1+free_71 && free_79>=free_79*free_62*free_95 && free_79*free_62*free_95+free_95>=1+free_79 && free_68>=free_73*free_68*free_62 && free_73+free_73*free_68*free_62>=1+free_68 && free_73*free_83+free_87>=free_83*free_95 && free_83*free_95+free_83>=1+free_73*free_83+free_87 && free_61>=free_83 && free_71>=free_96*free_71*free_62 && free_96*free_71*free_62+free_96>=1+free_71 && free_79>=free_79*free_62*free_75 && free_79*free_62*free_75+free_75>=1+free_79 && free_68>=free_85*free_68*free_62 && free_85+free_85*free_68*free_62>=1+free_68 && free_85*free_94+free_96>=free_94*free_75 && free_94*free_75+free_94>=1+free_85*free_94+free_96 && 1>=free_62*free_72 && free_62*free_72+free_72>=2 && free_94>=free_82+free_82*free_72 && 2*free_82+free_82*free_72>=1+free_94 && free_82>=free_66 && free_71>=free_92*free_71*free_62 && free_92*free_71*free_62+free_92>=1+free_71 && free_79>=free_79*free_70*free_62 && free_79*free_70*free_62+free_70>=1+free_79 && free_68>=free_80*free_68*free_62 && free_80*free_68*free_62+free_80>=1+free_68 && free_92+free_80*free_90>=free_70*free_90 && free_70*free_90+free_90>=1+free_92+free_80*free_90 && 1>=free_62*free_69 && free_62*free_69+free_69>=2 && free_90>=free_78+free_78*free_69 && 2*free_78+free_78*free_69>=1+free_90 && free_66>=free_78 && free_68*free_88+free_71>=free_79*free_88 && free_79*free_88+free_88>=1+free_68*free_88+free_71 && free_88>=free_67 && free_97*free_68+free_71>=free_79*free_97 && free_97+free_79*free_97>=1+free_97*free_68+free_71 && free_67>=free_97 && free_76*free_71+free_76*free_86*free_68>=free_76*free_79*free_86 && free_86+free_76*free_79*free_86>=1+free_76*free_71+free_76*free_86*free_68 && free_86>=free_63 && free_76*free_71+free_76*free_74*free_68>=free_76*free_79*free_74 && free_76*free_79*free_74+free_74>=1+free_76*free_71+free_76*free_74*free_68 && free_63>=free_74 && 1>=free_84*free_62 && free_84*free_62+free_84>=2 && free_64>=free_84 && 1>=free_93*free_62 && free_93+free_93*free_62>=2 && free_93>=free_64 && Q>=1+H ], cost: 1 19: f80 -> f92 : P'=S*free_47, W'=free_49, X'=free_50, Y'=free_46, Z'=free_48, [ T>=0 && S>=free_52*free_49*S && free_52+free_52*free_49*S>=1+S && free_52>=free_46 && S>=free_49*S*free_60 && free_60+free_49*S*free_60>=1+S && free_46>=free_60 && 1>=free_49*free_56 && free_56+free_49*free_56>=2 && free_50>=free_56 && 1>=free_49*free_53 && free_53+free_49*free_53>=2 && free_53>=free_50 && S>=free_49*free_59*S && free_49*free_59*S+free_59>=1+S && 1>=free_55*free_49 && free_55+free_55*free_49>=2 && free_59>=free_58*free_55+free_58 && free_58*free_55+2*free_58>=1+free_59 && free_58>=free_48 && S>=free_51*free_49*S && free_51+free_51*free_49*S>=1+S && 1>=free_49*free_54 && free_49*free_54+free_54>=2 && free_51>=free_57*free_54+free_57 && free_57*free_54+2*free_57>=1+free_51 && free_48>=free_57 ], cost: 1 21: f80 -> f92 : P'=-free_99*S, S'=-S, W'=free_101, X'=free_102, Y'=-S*free_98, Z'=free_100, [ 1>=free_101*free_98 && free_101*free_98+free_98>=2 && 0>=1+T && 1>=free_104*free_101 && free_104+free_104*free_101>=2 && free_102>=free_104 && 1>=free_110*free_101 && free_110*free_101+free_110>=2 && free_110>=free_102 && 1>=free_107*free_101 && free_107*free_101+free_107>=2 && 1>=free_105*free_101 && free_105+free_105*free_101>=2 && 0>=free_109+S*free_107+free_105*free_109 && 2*free_109+S*free_107+free_105*free_109>=1 && free_100>=free_109 && 1>=free_106*free_101 && free_106+free_106*free_101>=2 && 1>=free_108*free_101 && free_108+free_108*free_101>=2 && 0>=free_103+free_106*S+free_108*free_103 && 2*free_103+free_106*S+free_108*free_103>=1 && free_103>=free_100 ], cost: 1 46: f92 -> [22] : K'=free_111, P'=free_112, A1'=B, [ B>=1+A1 ], cost: -A1+B 47: f101 -> [23] : K'=free_113, P'=free_114, A1'=C, [ C>=1+A1 ], cost: -A1+C 48: f110 -> [24] : K'=free_115, P'=free_116, A1'=1+A, [ A>=A1 ], cost: 1-A1+A 49: f119 -> [25] : K'=free_117, P'=free_118, A1'=1+A, [ A>=A1 ], cost: 1-A1+A 50: f132 -> [26] : B'=1+A, [ A>=B ], cost: 1-B+A 40: [18] -> f5 : B'=1+B, [ C>=1+A ], cost: 1 39: [19] -> f27 : [ B>=1+A ], cost: 1 34: [20] -> f31 : B'=1+B, [ C>=1+A ], cost: 1 32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1 12: [21] -> f69 : Q'=free_7, J'=free_6, K'=100*free_6, [ A>=C && 4>=E ], cost: 1 13: [21] -> f69 : Q'=free_10, J'=free_9, K'=100*free_9, L'=free_11, M'=free_11+100*free_9, N'=free_12, O'=free_8, [ E>=5 && A>=C && free_8>=1+free_12+100*free_9 ], cost: 1 14: [21] -> f69 : Q'=free_15, J'=free_14, K'=100*free_14, L'=free_16, M'=free_16+100*free_14, N'=free_17, O'=free_13, [ E>=5 && A>=C && free_17+100*free_14>=1+free_13 ], cost: 1 15: [21] -> f69 : Q'=free_18, J'=free_19, K'=100*free_19, L'=free_20, M'=free_21, [ E>=5 && A>=C && free_21>=1+100*free_19+free_20 ], cost: 1 16: [21] -> f69 : Q'=free_22, J'=free_23, K'=100*free_23, L'=free_24, M'=free_25, [ E>=5 && A>=C && 100*free_23+free_24>=1+free_25 ], cost: 1 31: [22] -> f101 : [ A1>=B ], cost: 1 30: [23] -> f110 : [ A1>=C ], cost: 1 29: [24] -> f119 : [ A1>=1+A ], cost: 1 28: [25] -> f53 : C'=1+C, [ A1>=1+A ], cost: 1 27: [26] -> f27 : E'=1+E, [ B>=1+A ], cost: 1 Applied simple chaining: Start location: f2 0: f2 -> f5 : [], cost: 1 1: f5 -> f5 : B'=1+B, C'=1+A, [ A>=B && A>=C && 1+A>=1+A ], cost: 3-C+A 41: f5 -> f17 : [ B>=1+A ], cost: 1 43: f17 -> f27 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A 4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1 5: f31 -> f31 : B'=1+B, C'=1+A, F'=-free_1*(-1+C-A)+F, G'=free_1, [ A>=1+B && A>=C && 1+A>=1+A ], cost: 3-C+A 35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1 36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1 7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1 8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1 33: f50 -> f27 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A 9: f50 -> f53 : [ A>=1+B ], cost: 1 45: f53 -> [21] : C'=1+A, J'=free_3, K'=100*free_3, L'=free_4, M'=100*free_3+free_4, N'=free_5, O'=100*free_3+free_5, [ A>=C && E>=5 ], cost: 1-C+A 10: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1 17: f69 -> f80 : P'=-free_31+free_28, Q_1'=free_33, R'=free_27, S'=free_30, T'=free_26, U'=free_32, V'=free_29, [ free_27>=1+K+free_33 && 1>=free_32*free_34+free_29*free_34 && free_32*free_34+free_34+free_29*free_34>=2 && free_30>=free_34 && 1>=free_29*free_35+free_32*free_35 && free_29*free_35+free_32*free_35+free_35>=2 && free_35>=free_30 && Q>=1+H ], cost: 1 18: f69 -> f80 : P'=-free_41+free_38, Q_1'=free_43, R'=free_37, S'=free_40, T'=free_36, U'=free_42, V'=free_39, [ K+free_43>=1+free_37 && 1>=free_39*free_44+free_42*free_44 && free_39*free_44+free_42*free_44+free_44>=2 && free_40>=free_44 && 1>=free_42*free_45+free_45*free_39 && free_45+free_42*free_45+free_45*free_39>=2 && free_45>=free_40 && Q>=1+H ], cost: 1 20: f69 -> f92 : P'=free_63, Q_1'=free_65, R'=K+free_65, S'=free_67, W'=free_62, X'=free_64, Y'=free_61, Z'=free_66, [ free_71>=free_71*free_81*free_62 && free_71*free_81*free_62+free_81>=1+free_71 && free_79>=free_79*free_62*free_91 && free_79*free_62*free_91+free_91>=1+free_79 && free_68>=free_89*free_68*free_62 && free_89+free_89*free_68*free_62>=1+free_68 && free_89*free_77+free_81>=free_77*free_91 && free_77+free_77*free_91>=1+free_89*free_77+free_81 && free_77>=free_61 && free_71>=free_71*free_87*free_62 && free_87+free_71*free_87*free_62>=1+free_71 && free_79>=free_79*free_62*free_95 && free_79*free_62*free_95+free_95>=1+free_79 && free_68>=free_73*free_68*free_62 && free_73+free_73*free_68*free_62>=1+free_68 && free_73*free_83+free_87>=free_83*free_95 && free_83*free_95+free_83>=1+free_73*free_83+free_87 && free_61>=free_83 && free_71>=free_96*free_71*free_62 && free_96*free_71*free_62+free_96>=1+free_71 && free_79>=free_79*free_62*free_75 && free_79*free_62*free_75+free_75>=1+free_79 && free_68>=free_85*free_68*free_62 && free_85+free_85*free_68*free_62>=1+free_68 && free_85*free_94+free_96>=free_94*free_75 && free_94*free_75+free_94>=1+free_85*free_94+free_96 && 1>=free_62*free_72 && free_62*free_72+free_72>=2 && free_94>=free_82+free_82*free_72 && 2*free_82+free_82*free_72>=1+free_94 && free_82>=free_66 && free_71>=free_92*free_71*free_62 && free_92*free_71*free_62+free_92>=1+free_71 && free_79>=free_79*free_70*free_62 && free_79*free_70*free_62+free_70>=1+free_79 && free_68>=free_80*free_68*free_62 && free_80*free_68*free_62+free_80>=1+free_68 && free_92+free_80*free_90>=free_70*free_90 && free_70*free_90+free_90>=1+free_92+free_80*free_90 && 1>=free_62*free_69 && free_62*free_69+free_69>=2 && free_90>=free_78+free_78*free_69 && 2*free_78+free_78*free_69>=1+free_90 && free_66>=free_78 && free_68*free_88+free_71>=free_79*free_88 && free_79*free_88+free_88>=1+free_68*free_88+free_71 && free_88>=free_67 && free_97*free_68+free_71>=free_79*free_97 && free_97+free_79*free_97>=1+free_97*free_68+free_71 && free_67>=free_97 && free_76*free_71+free_76*free_86*free_68>=free_76*free_79*free_86 && free_86+free_76*free_79*free_86>=1+free_76*free_71+free_76*free_86*free_68 && free_86>=free_63 && free_76*free_71+free_76*free_74*free_68>=free_76*free_79*free_74 && free_76*free_79*free_74+free_74>=1+free_76*free_71+free_76*free_74*free_68 && free_63>=free_74 && 1>=free_84*free_62 && free_84*free_62+free_84>=2 && free_64>=free_84 && 1>=free_93*free_62 && free_93+free_93*free_62>=2 && free_93>=free_64 && Q>=1+H ], cost: 1 19: f80 -> f92 : P'=S*free_47, W'=free_49, X'=free_50, Y'=free_46, Z'=free_48, [ T>=0 && S>=free_52*free_49*S && free_52+free_52*free_49*S>=1+S && free_52>=free_46 && S>=free_49*S*free_60 && free_60+free_49*S*free_60>=1+S && free_46>=free_60 && 1>=free_49*free_56 && free_56+free_49*free_56>=2 && free_50>=free_56 && 1>=free_49*free_53 && free_53+free_49*free_53>=2 && free_53>=free_50 && S>=free_49*free_59*S && free_49*free_59*S+free_59>=1+S && 1>=free_55*free_49 && free_55+free_55*free_49>=2 && free_59>=free_58*free_55+free_58 && free_58*free_55+2*free_58>=1+free_59 && free_58>=free_48 && S>=free_51*free_49*S && free_51+free_51*free_49*S>=1+S && 1>=free_49*free_54 && free_49*free_54+free_54>=2 && free_51>=free_57*free_54+free_57 && free_57*free_54+2*free_57>=1+free_51 && free_48>=free_57 ], cost: 1 21: f80 -> f92 : P'=-free_99*S, S'=-S, W'=free_101, X'=free_102, Y'=-S*free_98, Z'=free_100, [ 1>=free_101*free_98 && free_101*free_98+free_98>=2 && 0>=1+T && 1>=free_104*free_101 && free_104+free_104*free_101>=2 && free_102>=free_104 && 1>=free_110*free_101 && free_110*free_101+free_110>=2 && free_110>=free_102 && 1>=free_107*free_101 && free_107*free_101+free_107>=2 && 1>=free_105*free_101 && free_105+free_105*free_101>=2 && 0>=free_109+S*free_107+free_105*free_109 && 2*free_109+S*free_107+free_105*free_109>=1 && free_100>=free_109 && 1>=free_106*free_101 && free_106+free_106*free_101>=2 && 1>=free_108*free_101 && free_108+free_108*free_101>=2 && 0>=free_103+free_106*S+free_108*free_103 && 2*free_103+free_106*S+free_108*free_103>=1 && free_103>=free_100 ], cost: 1 46: f92 -> f119 : K'=free_115, P'=free_116, A1'=1+A, [ B>=1+A1 && B>=B && C>=1+B && C>=C && A>=C && 1+A>=1+A ], cost: 4-A1+A 49: f119 -> f53 : C'=1+C, K'=free_117, P'=free_118, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A 32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1 12: [21] -> f69 : Q'=free_7, J'=free_6, K'=100*free_6, [ A>=C && 4>=E ], cost: 1 13: [21] -> f69 : Q'=free_10, J'=free_9, K'=100*free_9, L'=free_11, M'=free_11+100*free_9, N'=free_12, O'=free_8, [ E>=5 && A>=C && free_8>=1+free_12+100*free_9 ], cost: 1 14: [21] -> f69 : Q'=free_15, J'=free_14, K'=100*free_14, L'=free_16, M'=free_16+100*free_14, N'=free_17, O'=free_13, [ E>=5 && A>=C && free_17+100*free_14>=1+free_13 ], cost: 1 15: [21] -> f69 : Q'=free_18, J'=free_19, K'=100*free_19, L'=free_20, M'=free_21, [ E>=5 && A>=C && free_21>=1+100*free_19+free_20 ], cost: 1 16: [21] -> f69 : Q'=free_22, J'=free_23, K'=100*free_23, L'=free_24, M'=free_25, [ E>=5 && A>=C && 100*free_23+free_24>=1+free_25 ], cost: 1 Eliminating 1 self-loops for location f5 Removing the self-loops: 1. Adding an epsilon transition (to model nonexecution of the loops): 52. Eliminating 1 self-loops for location f31 Removing the self-loops: 5. Adding an epsilon transition (to model nonexecution of the loops): 54. Removed all Self-loops using metering functions (where possible): Start location: f2 0: f2 -> f5 : [], cost: 1 51: f5 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 3-C+A 52: f5 -> [27] : [], cost: 0 43: f17 -> f27 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A 4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1 53: f31 -> [28] : B'=1+B, C'=1+A, F'=-free_1*(-1+C-A)+F, G'=free_1, [ A>=1+B && A>=C ], cost: 3-C+A 54: f31 -> [28] : [], cost: 0 7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1 8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1 33: f50 -> f27 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A 9: f50 -> f53 : [ A>=1+B ], cost: 1 45: f53 -> [21] : C'=1+A, J'=free_3, K'=100*free_3, L'=free_4, M'=100*free_3+free_4, N'=free_5, O'=100*free_3+free_5, [ A>=C && E>=5 ], cost: 1-C+A 10: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1 17: f69 -> f80 : P'=-free_31+free_28, Q_1'=free_33, R'=free_27, S'=free_30, T'=free_26, U'=free_32, V'=free_29, [ free_27>=1+K+free_33 && 1>=free_32*free_34+free_29*free_34 && free_32*free_34+free_34+free_29*free_34>=2 && free_30>=free_34 && 1>=free_29*free_35+free_32*free_35 && free_29*free_35+free_32*free_35+free_35>=2 && free_35>=free_30 && Q>=1+H ], cost: 1 18: f69 -> f80 : P'=-free_41+free_38, Q_1'=free_43, R'=free_37, S'=free_40, T'=free_36, U'=free_42, V'=free_39, [ K+free_43>=1+free_37 && 1>=free_39*free_44+free_42*free_44 && free_39*free_44+free_42*free_44+free_44>=2 && free_40>=free_44 && 1>=free_42*free_45+free_45*free_39 && free_45+free_42*free_45+free_45*free_39>=2 && free_45>=free_40 && Q>=1+H ], cost: 1 20: f69 -> f92 : P'=free_63, Q_1'=free_65, R'=K+free_65, S'=free_67, W'=free_62, X'=free_64, Y'=free_61, Z'=free_66, [ free_71>=free_71*free_81*free_62 && free_71*free_81*free_62+free_81>=1+free_71 && free_79>=free_79*free_62*free_91 && free_79*free_62*free_91+free_91>=1+free_79 && free_68>=free_89*free_68*free_62 && free_89+free_89*free_68*free_62>=1+free_68 && free_89*free_77+free_81>=free_77*free_91 && free_77+free_77*free_91>=1+free_89*free_77+free_81 && free_77>=free_61 && free_71>=free_71*free_87*free_62 && free_87+free_71*free_87*free_62>=1+free_71 && free_79>=free_79*free_62*free_95 && free_79*free_62*free_95+free_95>=1+free_79 && free_68>=free_73*free_68*free_62 && free_73+free_73*free_68*free_62>=1+free_68 && free_73*free_83+free_87>=free_83*free_95 && free_83*free_95+free_83>=1+free_73*free_83+free_87 && free_61>=free_83 && free_71>=free_96*free_71*free_62 && free_96*free_71*free_62+free_96>=1+free_71 && free_79>=free_79*free_62*free_75 && free_79*free_62*free_75+free_75>=1+free_79 && free_68>=free_85*free_68*free_62 && free_85+free_85*free_68*free_62>=1+free_68 && free_85*free_94+free_96>=free_94*free_75 && free_94*free_75+free_94>=1+free_85*free_94+free_96 && 1>=free_62*free_72 && free_62*free_72+free_72>=2 && free_94>=free_82+free_82*free_72 && 2*free_82+free_82*free_72>=1+free_94 && free_82>=free_66 && free_71>=free_92*free_71*free_62 && free_92*free_71*free_62+free_92>=1+free_71 && free_79>=free_79*free_70*free_62 && free_79*free_70*free_62+free_70>=1+free_79 && free_68>=free_80*free_68*free_62 && free_80*free_68*free_62+free_80>=1+free_68 && free_92+free_80*free_90>=free_70*free_90 && free_70*free_90+free_90>=1+free_92+free_80*free_90 && 1>=free_62*free_69 && free_62*free_69+free_69>=2 && free_90>=free_78+free_78*free_69 && 2*free_78+free_78*free_69>=1+free_90 && free_66>=free_78 && free_68*free_88+free_71>=free_79*free_88 && free_79*free_88+free_88>=1+free_68*free_88+free_71 && free_88>=free_67 && free_97*free_68+free_71>=free_79*free_97 && free_97+free_79*free_97>=1+free_97*free_68+free_71 && free_67>=free_97 && free_76*free_71+free_76*free_86*free_68>=free_76*free_79*free_86 && free_86+free_76*free_79*free_86>=1+free_76*free_71+free_76*free_86*free_68 && free_86>=free_63 && free_76*free_71+free_76*free_74*free_68>=free_76*free_79*free_74 && free_76*free_79*free_74+free_74>=1+free_76*free_71+free_76*free_74*free_68 && free_63>=free_74 && 1>=free_84*free_62 && free_84*free_62+free_84>=2 && free_64>=free_84 && 1>=free_93*free_62 && free_93+free_93*free_62>=2 && free_93>=free_64 && Q>=1+H ], cost: 1 19: f80 -> f92 : P'=S*free_47, W'=free_49, X'=free_50, Y'=free_46, Z'=free_48, [ T>=0 && S>=free_52*free_49*S && free_52+free_52*free_49*S>=1+S && free_52>=free_46 && S>=free_49*S*free_60 && free_60+free_49*S*free_60>=1+S && free_46>=free_60 && 1>=free_49*free_56 && free_56+free_49*free_56>=2 && free_50>=free_56 && 1>=free_49*free_53 && free_53+free_49*free_53>=2 && free_53>=free_50 && S>=free_49*free_59*S && free_49*free_59*S+free_59>=1+S && 1>=free_55*free_49 && free_55+free_55*free_49>=2 && free_59>=free_58*free_55+free_58 && free_58*free_55+2*free_58>=1+free_59 && free_58>=free_48 && S>=free_51*free_49*S && free_51+free_51*free_49*S>=1+S && 1>=free_49*free_54 && free_49*free_54+free_54>=2 && free_51>=free_57*free_54+free_57 && free_57*free_54+2*free_57>=1+free_51 && free_48>=free_57 ], cost: 1 21: f80 -> f92 : P'=-free_99*S, S'=-S, W'=free_101, X'=free_102, Y'=-S*free_98, Z'=free_100, [ 1>=free_101*free_98 && free_101*free_98+free_98>=2 && 0>=1+T && 1>=free_104*free_101 && free_104+free_104*free_101>=2 && free_102>=free_104 && 1>=free_110*free_101 && free_110*free_101+free_110>=2 && free_110>=free_102 && 1>=free_107*free_101 && free_107*free_101+free_107>=2 && 1>=free_105*free_101 && free_105+free_105*free_101>=2 && 0>=free_109+S*free_107+free_105*free_109 && 2*free_109+S*free_107+free_105*free_109>=1 && free_100>=free_109 && 1>=free_106*free_101 && free_106+free_106*free_101>=2 && 1>=free_108*free_101 && free_108+free_108*free_101>=2 && 0>=free_103+free_106*S+free_108*free_103 && 2*free_103+free_106*S+free_108*free_103>=1 && free_103>=free_100 ], cost: 1 46: f92 -> f119 : K'=free_115, P'=free_116, A1'=1+A, [ B>=1+A1 && B>=B && C>=1+B && C>=C && A>=C && 1+A>=1+A ], cost: 4-A1+A 49: f119 -> f53 : C'=1+C, K'=free_117, P'=free_118, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A 32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1 12: [21] -> f69 : Q'=free_7, J'=free_6, K'=100*free_6, [ A>=C && 4>=E ], cost: 1 13: [21] -> f69 : Q'=free_10, J'=free_9, K'=100*free_9, L'=free_11, M'=free_11+100*free_9, N'=free_12, O'=free_8, [ E>=5 && A>=C && free_8>=1+free_12+100*free_9 ], cost: 1 14: [21] -> f69 : Q'=free_15, J'=free_14, K'=100*free_14, L'=free_16, M'=free_16+100*free_14, N'=free_17, O'=free_13, [ E>=5 && A>=C && free_17+100*free_14>=1+free_13 ], cost: 1 15: [21] -> f69 : Q'=free_18, J'=free_19, K'=100*free_19, L'=free_20, M'=free_21, [ E>=5 && A>=C && free_21>=1+100*free_19+free_20 ], cost: 1 16: [21] -> f69 : Q'=free_22, J'=free_23, K'=100*free_23, L'=free_24, M'=free_25, [ E>=5 && A>=C && 100*free_23+free_24>=1+free_25 ], cost: 1 41: [27] -> f17 : [ B>=1+A ], cost: 1 35: [28] -> f46 : [ B>=A && 0>=1+F ], cost: 1 36: [28] -> f46 : [ B>=A && F>=1 ], cost: 1 Applied chaining over branches and pruning: Start location: f2 55: f2 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 4-C+A Final control flow graph problem, now checking costs for infinitely many models: Start location: f2 55: f2 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 4-C+A Computing complexity for remaining 1 transitions. Found configuration with infinitely models for cost: 4-C+A and guard: A>=B && A>=C: B: Pos, C: Pos, A: Pos, where: A > B A > C Found new complexity n^1, because: Found infinity configuration. The final runtime is determined by this resulting transition: Final Guard: A>=B && A>=C Final Cost: 4-C+A 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),?)