Trying to load file: main.koat Initial Control flow graph problem: Start location: f33 0: f33 -> f3 : [], cost: 1 1: f3 -> f25 : A'=free, C'=B, D'=0, [ A>=1 && B>=1 && free>=1 ], cost: 1 2: f3 -> f25 : A'=free_1, C'=B, D'=0, [ A>=1 && 0>=1+B && free_1>=1 ], cost: 1 3: f3 -> f16 : A'=J, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=1+J, K'=free_2, [], cost: 1 4: f3 -> f16 : A'=1+free_4, F'=free_5, G'=free_5, H'=free_5, Q'=free_5, J'=1+J, K'=free_5, [ free_4>=0 && A>=0 ], cost: 1 5: f3 -> f22 : A'=free_6, B'=L, C'=0, D'=0, Q'=L, M'=L, N'=L, [ free_7>=1 && A>=1 && B==0 ], cost: 1 11: f16 -> f3 : A'=free_54, B'=free_43, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ A>=0 && free_57>=0 && free_58>=0 && J>=Q_1 && free_47>=1 ], cost: 1 12: f16 -> f3 : A'=free_70, B'=free_59, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ A>=0 && free_73>=0 && free_74>=0 && J>=Q_1 && 0>=1+free_63 ], cost: 1 9: f16 -> f16 : A'=1+free_28, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=1+free_30, K'=free_34, P'=free_33, Q_1'=free_27, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, [ A>=0 && free_36>=0 && Q_1>=1+J && free_28>=0 ], cost: 1 10: f16 -> f18 : A'=free_41, J'=free_37, M'=0, O'=0, P'=free_38, Q_1'=free_40, R'=0, Z'=free_39, [ A>=0 && free_42>=0 && J>=Q_1 && free_41>=0 ], cost: 1 13: f23 -> f16 : A'=free_77, F'=free_83, G'=free_83, H'=free_83, Q'=free_83, J'=1+free_77, K'=free_83, P'=free_82, Q_1'=free_76, U'=free_79, V'=free_80, W'=free_75, E1'=free_78, F1'=free_81, [ free_84>=1 ], cost: 1 6: f23 -> f17 : J'=free_8, K'=0, M'=0, O'=free_12, P'=free_9, Q_1'=free_11, R'=free_12, S'=free_10, [ free_12>=1 && 0>=free_13 ], cost: 1 7: f23 -> f17 : J'=free_14, K'=0, M'=0, O'=free_18, P'=free_15, Q_1'=free_17, R'=free_18, S'=free_16, [ 0>=1+free_18 && 0>=free_19 ], cost: 1 8: f23 -> f21 : Q'=free_24, J'=free_20, K'=0, M'=0, O'=0, P'=free_21, Q_1'=free_23, R'=0, S'=free_22, T'=0, [ 0>=free_25 ], cost: 1 Simplified the transitions: Start location: f33 0: f33 -> f3 : [], cost: 1 3: f3 -> f16 : A'=J, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=1+J, K'=free_2, [], cost: 1 4: f3 -> f16 : A'=1+free_4, F'=free_5, G'=free_5, H'=free_5, Q'=free_5, J'=1+J, K'=free_5, [ free_4>=0 && A>=0 ], cost: 1 11: f16 -> f3 : A'=free_54, B'=free_43, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ A>=0 && J>=Q_1 && free_47>=1 ], cost: 1 12: f16 -> f3 : A'=free_70, B'=free_59, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ A>=0 && J>=Q_1 && 0>=1+free_63 ], cost: 1 9: f16 -> f16 : A'=1+free_28, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=1+free_30, K'=free_34, P'=free_33, Q_1'=free_27, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, [ A>=0 && Q_1>=1+J && free_28>=0 ], cost: 1 Eliminating 1 self-loops for location f16 Removing the self-loops: 9. Adding an epsilon transition (to model nonexecution of the loops): 15. Removed all Self-loops using metering functions (where possible): Start location: f33 0: f33 -> f3 : [], cost: 1 3: f3 -> f16 : A'=J, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=1+J, K'=free_2, [], cost: 1 4: f3 -> f16 : A'=1+free_4, F'=free_5, G'=free_5, H'=free_5, Q'=free_5, J'=1+J, K'=free_5, [ free_4>=0 && A>=0 ], cost: 1 14: f16 -> [9] : A'=1+free_28, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=1+free_30, K'=free_34, P'=free_33, Q_1'=free_27, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, [ A>=0 && Q_1>=1+J && free_28>=0 ], cost: 1 15: f16 -> [9] : [], cost: 0 11: [9] -> f3 : A'=free_54, B'=free_43, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ A>=0 && J>=Q_1 && free_47>=1 ], cost: 1 12: [9] -> f3 : A'=free_70, B'=free_59, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ A>=0 && J>=Q_1 && 0>=1+free_63 ], cost: 1 Applied chaining over branches and pruning: Start location: f33 0: f33 -> f3 : [], cost: 1 16: f3 -> [9] : A'=1+free_28, E'=free_3, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=1+free_30, K'=free_34, P'=free_33, Q_1'=free_27, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, [ J>=0 && Q_1>=2+J && free_28>=0 ], cost: 2 17: f3 -> [9] : A'=J, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=1+J, K'=free_2, [], cost: 1 18: f3 -> [9] : A'=1+free_28, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=1+free_30, K'=free_34, P'=free_33, Q_1'=free_27, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, [ free_4>=0 && A>=0 && 1+free_4>=0 && Q_1>=2+J && free_28>=0 ], cost: 2 19: f3 -> [9] : A'=1+free_4, F'=free_5, G'=free_5, H'=free_5, Q'=free_5, J'=1+J, K'=free_5, [ free_4>=0 && A>=0 ], cost: 1 11: [9] -> f3 : A'=free_54, B'=free_43, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ A>=0 && J>=Q_1 && free_47>=1 ], cost: 1 12: [9] -> f3 : A'=free_70, B'=free_59, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ A>=0 && J>=Q_1 && 0>=1+free_63 ], cost: 1 Applied chaining over branches and pruning: Start location: f33 0: f33 -> f3 : [], cost: 1 20: f3 -> f3 : A'=free_54, B'=free_43, E'=free_3, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ J>=0 && Q_1>=2+J && free_28>=0 && 1+free_28>=0 && 1+free_30>=free_27 && free_47>=1 ], cost: 3 21: f3 -> f3 : A'=free_70, B'=free_59, E'=free_3, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ J>=0 && Q_1>=2+J && free_28>=0 && 1+free_28>=0 && 1+free_30>=free_27 && 0>=1+free_63 ], cost: 3 23: f3 -> f3 : A'=free_70, B'=free_59, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ J>=0 && 1+J>=Q_1 && 0>=1+free_63 ], cost: 2 24: f3 -> f3 : A'=free_54, B'=free_43, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ free_4>=0 && A>=0 && 1+free_4>=0 && Q_1>=2+J && free_28>=0 && 1+free_28>=0 && 1+free_30>=free_27 && free_47>=1 ], cost: 3 25: f3 -> f3 : A'=free_70, B'=free_59, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ free_4>=0 && A>=0 && 1+free_4>=0 && Q_1>=2+J && free_28>=0 && 1+free_28>=0 && 1+free_30>=free_27 && 0>=1+free_63 ], cost: 3 Eliminating 5 self-loops for location f3 Removing the self-loops: 20 21 23 24 25. Adding an epsilon transition (to model nonexecution of the loops): 33. Removed all Self-loops using metering functions (where possible): Start location: f33 0: f33 -> f3 : [], cost: 1 28: f3 -> [10] : A'=free_54, B'=free_43, E'=free_3, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ J>=0 && Q_1>=2+J && free_47>=1 ], cost: 3 29: f3 -> [10] : A'=free_70, B'=free_59, E'=free_3, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ J>=0 && Q_1>=2+J && 0>=1+free_63 ], cost: 3 30: f3 -> [10] : A'=free_70, B'=free_59, E'=free_3, F'=free_2, G'=free_2, H'=free_2, Q'=free_2, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ J>=0 && 1+J>=Q_1 && 0>=1+free_63 ], cost: 2 31: f3 -> [10] : A'=free_54, B'=free_43, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_49, K'=free_53, L'=free_55, M'=0, O'=free_45, P'=free_44, Q_1'=free_48, R'=free_52, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_50, A1'=free_47, B1'=free_51, C1'=free_56, D1'=free_46, [ A>=0 && Q_1>=2+J && free_47>=1 ], cost: 3 32: f3 -> [10] : A'=free_70, B'=free_59, F'=free_34, G'=free_34, H'=free_34, Q'=free_34, J'=free_65, K'=free_69, L'=free_71, M'=0, O'=free_61, P'=free_60, Q_1'=free_64, R'=free_68, U'=free_31, V'=free_26, W'=free_29, X'=free_32, Y'=free_35, Z'=free_66, A1'=free_63, B1'=free_67, C1'=free_72, D1'=free_62, [ A>=0 && Q_1>=2+J && 0>=1+free_63 ], cost: 3 33: f3 -> [10] : [], cost: 0 Applied chaining over branches and pruning: Start location: f33 Final control flow graph problem, now checking costs for infinitely many models: Start location: f33 Computing complexity for remaining 0 transitions. The final runtime is determined by this resulting transition: Final Guard: Final Cost: 1 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)