Trying to load file: main.koat Initial Control flow graph problem: Start location: f8 0: f12 -> f12 : C'=free_1, D'=free, E'=B, F'=G, H'=A, [ A>=0 && free_1>=2 && 0>=1+free_2 && 0>=1+free && 0>=1+B ], cost: 1 1: f12 -> f12 : C'=free_4, D'=free_3, E'=B, F'=G, H'=A, [ A>=0 && free_4>=2 && 0>=1+free_5 && 0>=1+free_3 && B>=1 ], cost: 1 2: f12 -> f12 : C'=free_7, D'=free_6, E'=B, F'=G, H'=A, [ A>=0 && free_7>=2 && 0>=1+free_8 && free_6>=1 && 0>=1+B ], cost: 1 3: f12 -> f12 : C'=free_10, D'=free_9, E'=B, F'=G, H'=A, [ A>=0 && free_10>=2 && 0>=1+free_11 && free_9>=1 && B>=1 ], cost: 1 4: f12 -> f12 : C'=free_13, D'=free_12, E'=B, F'=G, H'=A, [ A>=0 && free_13>=2 && free_14>=1 && 0>=1+free_12 && 0>=1+B ], cost: 1 5: f12 -> f12 : C'=free_16, D'=free_15, E'=B, F'=G, H'=A, [ A>=0 && free_16>=2 && free_17>=1 && 0>=1+free_15 && B>=1 ], cost: 1 6: f12 -> f12 : C'=free_19, D'=free_18, E'=B, F'=G, H'=A, [ A>=0 && free_19>=2 && free_20>=1 && free_18>=1 && 0>=1+B ], cost: 1 7: f12 -> f12 : C'=free_22, D'=free_21, E'=B, F'=G, H'=A, [ A>=0 && free_22>=2 && free_23>=1 && free_21>=1 && B>=1 ], cost: 1 11: f1 -> f12 : B'=K, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, Q_1'=free_54, Y'=free_53, Z'=free_56, B1'=free_60, [ J>=Q && J>=0 && free_61>=2 && free_55>=free_61 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+K && 0>=1+free_52 ], cost: 1 12: f1 -> f12 : B'=K, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, Q_1'=free_66, Y'=free_65, Z'=free_68, B1'=free_72, [ J>=Q && J>=0 && free_73>=2 && free_67>=free_73 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+K && free_64>=1 ], cost: 1 13: f1 -> f12 : B'=K, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, Q_1'=free_78, Y'=free_77, Z'=free_80, B1'=free_84, [ J>=Q && J>=0 && free_85>=2 && free_79>=free_85 && free_79>=0 && free_84>=free_82 && free_82>=2 && K>=1 && 0>=1+free_76 ], cost: 1 14: f1 -> f12 : B'=K, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, Q_1'=free_90, Y'=free_89, Z'=free_92, B1'=free_96, [ J>=Q && J>=0 && free_97>=2 && free_91>=free_97 && free_91>=0 && free_96>=free_94 && free_94>=2 && K>=1 && free_88>=1 ], cost: 1 8: f1 -> f1 : J'=1+J, K'=L, L'=free_25, M'=L, N'=free_24, O'=J, [ Q>=1+J && J>=0 ], cost: 1 9: f8 -> f1 : C'=free_28, Q'=free_28, J'=2, K'=free_30, L'=free_27, M'=free_30, P'=free_26, Q_1'=free_30, R'=free_29, S'=2, [ free_28>=2 ], cost: 1 10: f8 -> f9 : B'=0, C'=free_42, D'=0, Q'=free_31, J'=free_37, K'=free_36, L'=free_34, M'=free_45, P'=free_41, Q_1'=free_40, T'=free_33, U'=free_44, V'=free_38, W'=free_43, X'=free_32, Y'=free_39, Z'=free_46, A1'=free_35, [ 0>=free_47 && 0>=free_48 && 0>=free_42 && 0>=free_49 ], cost: 1 Simplified the transitions: Start location: f8 0: f12 -> f12 : C'=free_1, D'=free, E'=B, F'=G, H'=A, [ A>=0 && free_1>=2 && 0>=1+free && 0>=1+B ], cost: 1 1: f12 -> f12 : C'=free_4, D'=free_3, E'=B, F'=G, H'=A, [ A>=0 && free_4>=2 && 0>=1+free_3 && B>=1 ], cost: 1 2: f12 -> f12 : C'=free_7, D'=free_6, E'=B, F'=G, H'=A, [ A>=0 && free_7>=2 && free_6>=1 && 0>=1+B ], cost: 1 3: f12 -> f12 : C'=free_10, D'=free_9, E'=B, F'=G, H'=A, [ A>=0 && free_10>=2 && free_9>=1 && B>=1 ], cost: 1 4: f12 -> f12 : C'=free_13, D'=free_12, E'=B, F'=G, H'=A, [ A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+B ], cost: 1 5: f12 -> f12 : C'=free_16, D'=free_15, E'=B, F'=G, H'=A, [ A>=0 && free_16>=2 && 0>=1+free_15 && B>=1 ], cost: 1 6: f12 -> f12 : C'=free_19, D'=free_18, E'=B, F'=G, H'=A, [ A>=0 && free_19>=2 && free_18>=1 && 0>=1+B ], cost: 1 7: f12 -> f12 : C'=free_22, D'=free_21, E'=B, F'=G, H'=A, [ A>=0 && free_22>=2 && free_21>=1 && B>=1 ], cost: 1 11: f1 -> f12 : B'=K, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, Q_1'=free_54, Y'=free_53, Z'=free_56, B1'=free_60, [ J>=Q && J>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+K && 0>=1+free_52 && 2<=free_55 ], cost: 1 12: f1 -> f12 : B'=K, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, Q_1'=free_66, Y'=free_65, Z'=free_68, B1'=free_72, [ J>=Q && J>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+K && free_64>=1 && 2<=free_67 ], cost: 1 13: f1 -> f12 : B'=K, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, Q_1'=free_78, Y'=free_77, Z'=free_80, B1'=free_84, [ J>=Q && J>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && K>=1 && 0>=1+free_76 && 2<=free_79 ], cost: 1 14: f1 -> f12 : B'=K, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, Q_1'=free_90, Y'=free_89, Z'=free_92, B1'=free_96, [ J>=Q && J>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && K>=1 && free_88>=1 && 2<=free_91 ], cost: 1 8: f1 -> f1 : J'=1+J, K'=L, L'=free_25, M'=L, N'=free_24, O'=J, [ Q>=1+J && J>=0 ], cost: 1 9: f8 -> f1 : C'=free_28, Q'=free_28, J'=2, K'=free_30, L'=free_27, M'=free_30, P'=free_26, Q_1'=free_30, R'=free_29, S'=2, [ free_28>=2 ], cost: 1 Eliminating 8 self-loops for location f12 Self-Loop 0 has unbounded runtime, resulting in the new transition 15. Self-Loop 1 has unbounded runtime, resulting in the new transition 16. Self-Loop 2 has unbounded runtime, resulting in the new transition 17. Self-Loop 3 has unbounded runtime, resulting in the new transition 18. Self-Loop 4 has unbounded runtime, resulting in the new transition 19. Self-Loop 5 has unbounded runtime, resulting in the new transition 20. Self-Loop 6 has unbounded runtime, resulting in the new transition 21. Self-Loop 7 has unbounded runtime, resulting in the new transition 22. Removing the self-loops: 0 1 2 3 4 5 6 7. Eliminating 1 self-loops for location f1 Self-Loop 8 has the metering function: Q-J, resulting in the new transition 23. Removing the self-loops: 8. Removed all Self-loops using metering functions (where possible): Start location: f8 15: f12 -> [4] : [ A>=0 && free_1>=2 && 0>=1+free && 0>=1+B ], cost: INF 16: f12 -> [4] : [ A>=0 && free_4>=2 && 0>=1+free_3 && B>=1 ], cost: INF 17: f12 -> [4] : [ A>=0 && free_7>=2 && free_6>=1 && 0>=1+B ], cost: INF 18: f12 -> [4] : [ A>=0 && free_10>=2 && free_9>=1 && B>=1 ], cost: INF 19: f12 -> [4] : [ A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+B ], cost: INF 20: f12 -> [4] : [ A>=0 && free_16>=2 && 0>=1+free_15 && B>=1 ], cost: INF 21: f12 -> [4] : [ A>=0 && free_19>=2 && free_18>=1 && 0>=1+B ], cost: INF 22: f12 -> [4] : [ A>=0 && free_22>=2 && free_21>=1 && B>=1 ], cost: INF 23: f1 -> [5] : J'=Q, K'=free_25, L'=free_25, M'=free_25, N'=free_24, O'=-1+Q, [ Q>=1+J && J>=0 ], cost: Q-J 9: f8 -> f1 : C'=free_28, Q'=free_28, J'=2, K'=free_30, L'=free_27, M'=free_30, P'=free_26, Q_1'=free_30, R'=free_29, S'=2, [ free_28>=2 ], cost: 1 11: [5] -> f12 : B'=K, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, Q_1'=free_54, Y'=free_53, Z'=free_56, B1'=free_60, [ J>=Q && J>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+K && 0>=1+free_52 && 2<=free_55 ], cost: 1 12: [5] -> f12 : B'=K, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, Q_1'=free_66, Y'=free_65, Z'=free_68, B1'=free_72, [ J>=Q && J>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+K && free_64>=1 && 2<=free_67 ], cost: 1 13: [5] -> f12 : B'=K, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, Q_1'=free_78, Y'=free_77, Z'=free_80, B1'=free_84, [ J>=Q && J>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && K>=1 && 0>=1+free_76 && 2<=free_79 ], cost: 1 14: [5] -> f12 : B'=K, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, Q_1'=free_90, Y'=free_89, Z'=free_92, B1'=free_96, [ J>=Q && J>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && K>=1 && free_88>=1 && 2<=free_91 ], cost: 1 Applied simple chaining: Start location: f8 15: f12 -> [4] : [ A>=0 && free_1>=2 && 0>=1+free && 0>=1+B ], cost: INF 16: f12 -> [4] : [ A>=0 && free_4>=2 && 0>=1+free_3 && B>=1 ], cost: INF 17: f12 -> [4] : [ A>=0 && free_7>=2 && free_6>=1 && 0>=1+B ], cost: INF 18: f12 -> [4] : [ A>=0 && free_10>=2 && free_9>=1 && B>=1 ], cost: INF 19: f12 -> [4] : [ A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+B ], cost: INF 20: f12 -> [4] : [ A>=0 && free_16>=2 && 0>=1+free_15 && B>=1 ], cost: INF 21: f12 -> [4] : [ A>=0 && free_19>=2 && free_18>=1 && 0>=1+B ], cost: INF 22: f12 -> [4] : [ A>=0 && free_22>=2 && free_21>=1 && B>=1 ], cost: INF 9: f8 -> [5] : C'=free_28, Q'=free_28, J'=free_28, K'=free_25, L'=free_25, M'=free_25, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_30, R'=free_29, S'=2, [ free_28>=2 && free_28>=3 && 2>=0 ], cost: -1+free_28 11: [5] -> f12 : B'=K, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, Q_1'=free_54, Y'=free_53, Z'=free_56, B1'=free_60, [ J>=Q && J>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+K && 0>=1+free_52 && 2<=free_55 ], cost: 1 12: [5] -> f12 : B'=K, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, Q_1'=free_66, Y'=free_65, Z'=free_68, B1'=free_72, [ J>=Q && J>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+K && free_64>=1 && 2<=free_67 ], cost: 1 13: [5] -> f12 : B'=K, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, Q_1'=free_78, Y'=free_77, Z'=free_80, B1'=free_84, [ J>=Q && J>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && K>=1 && 0>=1+free_76 && 2<=free_79 ], cost: 1 14: [5] -> f12 : B'=K, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, Q_1'=free_90, Y'=free_89, Z'=free_92, B1'=free_96, [ J>=Q && J>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && K>=1 && free_88>=1 && 2<=free_91 ], cost: 1 Applied chaining over branches and pruning: Start location: f8 15: f12 -> [4] : [ A>=0 && free_1>=2 && 0>=1+free && 0>=1+B ], cost: INF 16: f12 -> [4] : [ A>=0 && free_4>=2 && 0>=1+free_3 && B>=1 ], cost: INF 18: f12 -> [4] : [ A>=0 && free_10>=2 && free_9>=1 && B>=1 ], cost: INF 19: f12 -> [4] : [ A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+B ], cost: INF 20: f12 -> [4] : [ A>=0 && free_16>=2 && 0>=1+free_15 && B>=1 ], cost: INF 24: f8 -> f12 : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 25: f8 -> f12 : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 26: f8 -> f12 : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 ], cost: free_28 27: f8 -> f12 : B'=free_25, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_90, R'=free_29, S'=2, Y'=free_89, Z'=free_92, B1'=free_96, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && free_25>=1 && free_88>=1 && 2<=free_91 ], cost: free_28 Applied chaining over branches and pruning: Start location: f8 28: f8 -> [4] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 && A>=0 && free_1>=2 && 0>=1+free && 0>=1+free_25 ], cost: INF 31: f8 -> [4] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 && A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+free_25 ], cost: INF 36: f8 -> [4] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 && A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+free_25 ], cost: INF 39: f8 -> [4] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 && A>=0 && free_4>=2 && 0>=1+free_3 && free_25>=1 ], cost: INF 40: f8 -> [4] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 && A>=0 && free_10>=2 && free_9>=1 && free_25>=1 ], cost: INF 29: f8 -> [6] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 30: f8 -> [7] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 32: f8 -> [8] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 34: f8 -> [9] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 35: f8 -> [10] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 37: f8 -> [11] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 38: f8 -> [12] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 ], cost: free_28 41: f8 -> [13] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 ], cost: free_28 43: f8 -> [14] : B'=free_25, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_90, R'=free_29, S'=2, Y'=free_89, Z'=free_92, B1'=free_96, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && free_25>=1 && free_88>=1 && 2<=free_91 ], cost: free_28 46: f8 -> [15] : B'=free_25, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_90, R'=free_29, S'=2, Y'=free_89, Z'=free_92, B1'=free_96, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && free_25>=1 && free_88>=1 && 2<=free_91 ], cost: free_28 Final control flow graph problem, now checking costs for infinitely many models: Start location: f8 28: f8 -> [4] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 && A>=0 && free_1>=2 && 0>=1+free && 0>=1+free_25 ], cost: INF 31: f8 -> [4] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 && A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+free_25 ], cost: INF 36: f8 -> [4] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 && A>=0 && free_13>=2 && 0>=1+free_12 && 0>=1+free_25 ], cost: INF 39: f8 -> [4] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 && A>=0 && free_4>=2 && 0>=1+free_3 && free_25>=1 ], cost: INF 40: f8 -> [4] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 && A>=0 && free_10>=2 && free_9>=1 && free_25>=1 ], cost: INF 29: f8 -> [6] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 30: f8 -> [7] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 32: f8 -> [8] : B'=free_25, C'=free_58, D'=free_52, Q'=free_59, J'=free_55, K'=free_51, L'=free_50, M'=free_57, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_54, R'=free_29, S'=2, Y'=free_53, Z'=free_56, B1'=free_60, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 ], cost: free_28 34: f8 -> [9] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 35: f8 -> [10] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 37: f8 -> [11] : B'=free_25, C'=free_70, D'=free_64, Q'=free_71, J'=free_67, K'=free_63, L'=free_62, M'=free_69, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_66, R'=free_29, S'=2, Y'=free_65, Z'=free_68, B1'=free_72, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_67>=0 && free_72>=free_70 && free_70>=2 && 0>=1+free_25 && free_64>=1 && 2<=free_67 ], cost: free_28 38: f8 -> [12] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 ], cost: free_28 41: f8 -> [13] : B'=free_25, C'=free_82, D'=free_76, Q'=free_83, J'=free_79, K'=free_75, L'=free_74, M'=free_81, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_78, R'=free_29, S'=2, Y'=free_77, Z'=free_80, B1'=free_84, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_79>=0 && free_84>=free_82 && free_82>=2 && free_25>=1 && 0>=1+free_76 && 2<=free_79 ], cost: free_28 43: f8 -> [14] : B'=free_25, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_90, R'=free_29, S'=2, Y'=free_89, Z'=free_92, B1'=free_96, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && free_25>=1 && free_88>=1 && 2<=free_91 ], cost: free_28 46: f8 -> [15] : B'=free_25, C'=free_94, D'=free_88, Q'=free_95, J'=free_91, K'=free_87, L'=free_86, M'=free_93, N'=free_24, O'=-1+free_28, P'=free_26, Q_1'=free_90, R'=free_29, S'=2, Y'=free_89, Z'=free_92, B1'=free_96, [ free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_91>=0 && free_96>=free_94 && free_94>=2 && free_25>=1 && free_88>=1 && 2<=free_91 ], cost: free_28 Computing complexity for remaining 15 transitions. Found new complexity INF, because: INF sat. The final runtime is determined by this resulting transition: Final Guard: free_28>=2 && free_28>=3 && 2>=0 && free_28>=free_28 && free_28>=0 && free_55>=0 && free_60>=free_58 && free_58>=2 && 0>=1+free_25 && 0>=1+free_52 && 2<=free_55 && A>=0 && free_1>=2 && 0>=1+free && 0>=1+free_25 Final Cost: INF Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)