WORST_CASE(?, O(1)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47) -> Com_1(f75(2, Fresh_0, Fresh_0, Fresh_0, Fresh_0, Fresh_0, 2, Fresh_1, Fresh_1, Fresh_1, Fresh_1, Fresh_1, 2, Fresh_2, Fresh_2, Fresh_2, Fresh_2, Fresh_2, 2, Fresh_3, Fresh_3, Fresh_3, Fresh_3, Fresh_3, 2, Fresh_4, Fresh_4, Fresh_4, Fresh_4, Fresh_4, 2, Fresh_5, Fresh_5, Fresh_5, Fresh_5, Fresh_5, 2, Fresh_6, Fresh_6, Fresh_6, Fresh_6, Fresh_6, 2, Fresh_7, Fresh_7, Fresh_7, Fresh_7, Fresh_7)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables []. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start() -> Com_1(f0()) [ 0 <= 0 ] (Comp: ?, Cost: 1) f0() -> Com_1(f75()) start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (Comp: 1, Cost: 0) koat_start() -> Com_1(f0()) [ 0 <= 0 ] (Comp: 1, Cost: 1) f0() -> Com_1(f75()) start location: koat_start leaf cost: 0 Complexity upper bound 1 Time: 0.015 sec (SMT: 0.014 sec)