MAYBE Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f300(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) -> Com_1(f1(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Fresh_72, 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)) (Comp: ?, Cost: 1) f1(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) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, 256, Fresh_60, Fresh_61, Fresh_62, Fresh_63, Fresh_64, Fresh_65, Fresh_66, Fresh_67, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20)) [ A1 >= 1 /\ Ar_5 + 1 = Ar_6 /\ Ar_7 = 256 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_53, Fresh_54, Fresh_55, Fresh_56, Fresh_57, Fresh_58, Fresh_59, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20)) [ 0 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_45, Fresh_46, Fresh_47, Fresh_48, Fresh_49, Fresh_50, Fresh_51, Fresh_52, 256, Ar_17, Ar_18, Ar_19, Ar_20)) [ A1 >= 1 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 /\ Ar_16 = 256 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_38, Fresh_39, Fresh_40, Fresh_41, Fresh_42, Fresh_43, Fresh_44, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20)) [ 0 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f2(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_36, Fresh_37, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, 0, 0, 0, Ar_20)) [ Ar_5 >= Ar_6 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_27, Fresh_28, Fresh_29, Fresh_30, Fresh_31, Fresh_32, Fresh_33, Fresh_34, Ar_16, Ar_7, Ar_7, Ar_7, Fresh_35)) [ Ar_7 >= 1 /\ Ar_7 >= 257 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_18, Fresh_19, Fresh_20, Fresh_21, Fresh_22, Fresh_23, Fresh_24, Fresh_25, Ar_16, Ar_7, Ar_7, Ar_7, Fresh_26)) [ Ar_7 >= 1 /\ 255 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_9, Fresh_10, Fresh_11, Fresh_12, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Ar_16, Ar_16, Ar_16, Ar_16, Fresh_17)) [ Ar_16 >= 1 /\ Ar_16 >= 257 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(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) -> Com_1(f3(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Fresh_0, Fresh_1, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Fresh_7, Ar_16, Ar_16, Ar_16, Ar_16, Fresh_8)) [ Ar_16 >= 1 /\ 255 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (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) -> Com_1(f300(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)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_5, Ar_6, Ar_7, Ar_16]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f300(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_16 >= 1 /\ 255 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_16 >= 1 /\ Ar_16 >= 257 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_7 >= 1 /\ 255 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_7 >= 1 /\ Ar_7 >= 257 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f2(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_5 >= Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, 256)) [ A1 >= 1 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 /\ Ar_16 = 256 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, 256, Ar_16)) [ A1 >= 1 /\ Ar_5 + 1 = Ar_6 /\ Ar_7 = 256 ] (Comp: ?, Cost: 1) f300(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) 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(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f300(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_16 >= 1 /\ 255 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: 1, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_16 >= 1 /\ Ar_16 >= 257 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: 1, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_7 >= 1 /\ 255 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: 1, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f3(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_7 >= 1 /\ Ar_7 >= 257 /\ Ar_5 + 1 = Ar_6 ] (Comp: 1, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f2(Ar_5, Ar_6, Ar_7, Ar_16)) [ Ar_5 >= Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 >= Ar_16 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, 256)) [ A1 >= 1 /\ Ar_6 >= Ar_5 + 1 /\ Ar_6 >= Ar_5 + 2 /\ Ar_16 = 256 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) [ 0 >= Ar_7 /\ Ar_5 + 1 = Ar_6 ] (Comp: ?, Cost: 1) f1(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, 256, Ar_16)) [ A1 >= 1 /\ Ar_5 + 1 = Ar_6 /\ Ar_7 = 256 ] (Comp: 1, Cost: 1) f300(Ar_5, Ar_6, Ar_7, Ar_16) -> Com_1(f1(Ar_5, Ar_6, Ar_7, Ar_16)) start location: koat_start leaf cost: 0 Complexity upper bound ? Time: 1.986 sec (SMT: 1.899 sec)