Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f11 -> f11 : B'=1+B, C'=D, D'=free, E'=D, F'=free_1, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 9: f11 -> f2 : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, W'=free_64, Z'=free_62, A1'=free_61, [ free_66>=2 && H1>=free_66 && free_67>=2 && H1>=free_67 && B>=A && B>=0 && free_59>=2 && 0>=1+J && H1>=0 ], cost: 1 10: f11 -> f2 : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, W'=free_76, Z'=free_74, A1'=free_73, [ free_78>=2 && H1>=free_78 && free_79>=2 && H1>=free_79 && B>=A && B>=0 && free_71>=2 && J>=1 && H1>=0 ], cost: 1 1: f2 -> f2 : K'=free_2, L'=free_3, M'=J, N'=free_3, O'=J, P'=Q_1, R'=Q, [ 0>=1+J && free_2>=2 ], cost: 1 2: f2 -> f2 : K'=free_4, L'=free_5, M'=J, N'=free_5, O'=J, P'=Q_1, R'=Q, [ J>=1 && free_4>=2 ], cost: 1 3: f5 -> f5 : K'=1, L'=free_6, M'=J, N'=free_6, O'=J, S'=Q, T'=U, [ 0>=1+J ], cost: 1 4: f5 -> f5 : K'=1, L'=free_7, M'=J, N'=free_7, O'=J, S'=Q, T'=U, [ J>=1 ], cost: 1 5: f0 -> f11 : A'=free_12, B'=2, C'=free_8, D'=free_9, E'=free_8, K'=free_12, V'=free_10, W'=free_8, X'=free_11, [ free_12>=2 ], cost: 1 7: f0 -> f5 : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J ], cost: 1 8: f0 -> f5 : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 ], cost: 1 6: f0 -> f1 : A'=free_14, B'=free_27, C'=free_20, D'=free_18, E'=free_33, J'=free_26, K'=free_29, L'=free_25, M'=free_31, O'=free_16, V'=free_22, W'=free_24, Y'=free_13, Z'=free_32, A1'=free_17, B1'=free_23, C1'=free_30, D1'=free_15, E1'=free_21, F1'=free_28, G1'=free_19, [ 0>=free_34 && 0>=free_29 && 0>=free_35 && Y==0 ], cost: 1 Simplified the transitions: Start location: f0 0: f11 -> f11 : B'=1+B, C'=D, D'=free, E'=D, F'=free_1, G'=B, H'=Q, [ A>=1+B && B>=0 ], cost: 1 9: f11 -> f2 : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, W'=free_64, Z'=free_62, A1'=free_61, [ B>=A && B>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 10: f11 -> f2 : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, W'=free_76, Z'=free_74, A1'=free_73, [ B>=A && B>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 1: f2 -> f2 : K'=free_2, L'=free_3, M'=J, N'=free_3, O'=J, P'=Q_1, R'=Q, [ 0>=1+J && free_2>=2 ], cost: 1 2: f2 -> f2 : K'=free_4, L'=free_5, M'=J, N'=free_5, O'=J, P'=Q_1, R'=Q, [ J>=1 && free_4>=2 ], cost: 1 3: f5 -> f5 : K'=1, L'=free_6, M'=J, N'=free_6, O'=J, S'=Q, T'=U, [ 0>=1+J ], cost: 1 4: f5 -> f5 : K'=1, L'=free_7, M'=J, N'=free_7, O'=J, S'=Q, T'=U, [ J>=1 ], cost: 1 5: f0 -> f11 : A'=free_12, B'=2, C'=free_8, D'=free_9, E'=free_8, K'=free_12, V'=free_10, W'=free_8, X'=free_11, [ free_12>=2 ], cost: 1 7: f0 -> f5 : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J ], cost: 1 8: f0 -> f5 : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 ], cost: 1 Eliminating 1 self-loops for location f11 Self-Loop 0 has the metering function: -B+A, resulting in the new transition 11. Removing the self-loops: 0. Eliminating 2 self-loops for location f2 Self-Loop 1 has unbounded runtime, resulting in the new transition 12. Self-Loop 2 has unbounded runtime, resulting in the new transition 13. Removing the self-loops: 1 2. Eliminating 2 self-loops for location f5 Self-Loop 3 has unbounded runtime, resulting in the new transition 14. Self-Loop 4 has unbounded runtime, resulting in the new transition 15. Removing the self-loops: 3 4. Removed all Self-loops using metering functions (where possible): Start location: f0 11: f11 -> [5] : B'=A, C'=free, D'=free, E'=free, F'=free_1, G'=-1+A, H'=Q, [ A>=1+B && B>=0 ], cost: -B+A 12: f2 -> [6] : [ 0>=1+J && free_2>=2 ], cost: INF 13: f2 -> [6] : [ J>=1 && free_4>=2 ], cost: INF 14: f5 -> [7] : [ 0>=1+J ], cost: INF 15: f5 -> [7] : [ J>=1 ], cost: INF 5: f0 -> f11 : A'=free_12, B'=2, C'=free_8, D'=free_9, E'=free_8, K'=free_12, V'=free_10, W'=free_8, X'=free_11, [ free_12>=2 ], cost: 1 7: f0 -> f5 : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J ], cost: 1 8: f0 -> f5 : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 ], cost: 1 9: [5] -> f2 : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, W'=free_64, Z'=free_62, A1'=free_61, [ B>=A && B>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 10: [5] -> f2 : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, W'=free_76, Z'=free_74, A1'=free_73, [ B>=A && B>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 Applied simple chaining: Start location: f0 12: f2 -> [6] : [ 0>=1+J && free_2>=2 ], cost: INF 13: f2 -> [6] : [ J>=1 && free_4>=2 ], cost: INF 14: f5 -> [7] : [ 0>=1+J ], cost: INF 15: f5 -> [7] : [ J>=1 ], cost: INF 7: f0 -> f5 : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J ], cost: 1 8: f0 -> f5 : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 ], cost: 1 5: f0 -> [5] : A'=free_12, B'=free_12, C'=free, D'=free, E'=free, F'=free_1, G'=-1+free_12, H'=Q, K'=free_12, V'=free_10, W'=free_8, X'=free_11, [ free_12>=2 && free_12>=3 && 2>=0 ], cost: -1+free_12 9: [5] -> f2 : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, W'=free_64, Z'=free_62, A1'=free_61, [ B>=A && B>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 10: [5] -> f2 : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, W'=free_76, Z'=free_74, A1'=free_73, [ B>=A && B>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: 1 Applied chaining over branches and pruning: Start location: f0 12: f2 -> [6] : [ 0>=1+J && free_2>=2 ], cost: INF 13: f2 -> [6] : [ J>=1 && free_4>=2 ], cost: INF 18: f0 -> f2 : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, F'=free_1, G'=-1+free_12, H'=Q, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, V'=free_10, W'=free_64, X'=free_11, Z'=free_62, A1'=free_61, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 19: f0 -> f2 : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, F'=free_1, G'=-1+free_12, H'=Q, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, V'=free_10, W'=free_76, X'=free_11, Z'=free_74, A1'=free_73, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 16: f0 -> [7] : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J && 0>=1+J ], cost: INF 17: f0 -> [7] : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 && J>=1 ], cost: INF Applied chaining over branches and pruning: Start location: f0 20: f0 -> [6] : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, F'=free_1, G'=-1+free_12, H'=Q, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, V'=free_10, W'=free_64, X'=free_11, Z'=free_62, A1'=free_61, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 && 0>=1+J && free_2>=2 ], cost: INF 23: f0 -> [6] : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, F'=free_1, G'=-1+free_12, H'=Q, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, V'=free_10, W'=free_76, X'=free_11, Z'=free_74, A1'=free_73, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 && J>=1 && free_4>=2 ], cost: INF 16: f0 -> [7] : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J && 0>=1+J ], cost: INF 17: f0 -> [7] : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 && J>=1 ], cost: INF 21: f0 -> [8] : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, F'=free_1, G'=-1+free_12, H'=Q, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, V'=free_10, W'=free_64, X'=free_11, Z'=free_62, A1'=free_61, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 22: f0 -> [9] : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, F'=free_1, G'=-1+free_12, H'=Q, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, V'=free_10, W'=free_76, X'=free_11, Z'=free_74, A1'=free_73, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 20: f0 -> [6] : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, F'=free_1, G'=-1+free_12, H'=Q, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, V'=free_10, W'=free_64, X'=free_11, Z'=free_62, A1'=free_61, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 && 0>=1+J && free_2>=2 ], cost: INF 23: f0 -> [6] : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, F'=free_1, G'=-1+free_12, H'=Q, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, V'=free_10, W'=free_76, X'=free_11, Z'=free_74, A1'=free_73, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 && J>=1 && free_4>=2 ], cost: INF 16: f0 -> [7] : A'=free_43, B'=free_38, C'=free_36, D'=free_40, E'=free_37, K'=1, L'=free_45, M'=J, N'=free_45, O'=J, V'=free_39, W'=free_44, Z'=free_42, A1'=free_41, [ 0>=1+J && 0>=1+J ], cost: INF 17: f0 -> [7] : A'=free_53, B'=free_48, C'=free_46, D'=free_50, E'=free_47, K'=1, L'=free_55, M'=J, N'=free_55, O'=J, V'=free_49, W'=free_54, Z'=free_52, A1'=free_51, [ J>=1 && J>=1 ], cost: INF 21: f0 -> [8] : A'=free_63, B'=free_58, C'=free_56, D'=free_60, E'=free_57, F'=free_1, G'=-1+free_12, H'=Q, K'=free_59, L'=free_65, M'=J, N'=free_65, O'=J, V'=free_10, W'=free_64, X'=free_11, Z'=free_62, A1'=free_61, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 22: f0 -> [9] : A'=free_75, B'=free_70, C'=free_68, D'=free_72, E'=free_69, F'=free_1, G'=-1+free_12, H'=Q, K'=free_71, L'=free_77, M'=J, N'=free_77, O'=J, V'=free_10, W'=free_76, X'=free_11, Z'=free_74, A1'=free_73, [ free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_71>=2 && J>=1 && H1>=0 && 2<=H1 && 2<=H1 ], cost: free_12 Computing complexity for remaining 6 transitions. Found new complexity INF, because: INF sat. The final runtime is determined by this resulting transition: Final Guard: free_12>=2 && free_12>=3 && 2>=0 && free_12>=free_12 && free_12>=0 && free_59>=2 && 0>=1+J && H1>=0 && 2<=H1 && 2<=H1 && 0>=1+J && free_2>=2 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,?)