YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1) 1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1) 2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1) 3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1) 4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1) 5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1) 6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1) 7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1) 8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1) 9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1) Signature: {(evalwcet2bb1in,2) ;(evalwcet2bb2in,2) ;(evalwcet2bb4in,2) ;(evalwcet2bb5in,2) ;(evalwcet2entryin,2) ;(evalwcet2returnin,2) ;(evalwcet2start,2) ;(evalwcet2stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,6)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwcet2start(A,B) -> evalwcet2entryin(A,B) True (1,1) 1. evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True (?,1) 2. evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] (?,1) 3. evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] (?,1) 4. evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] (?,1) 5. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] (?,1) 6. evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] (?,1) 7. evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True (?,1) 8. evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True (?,1) 9. evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True (?,1) Signature: {(evalwcet2bb1in,2) ;(evalwcet2bb2in,2) ;(evalwcet2bb4in,2) ;(evalwcet2bb5in,2) ;(evalwcet2entryin,2) ;(evalwcet2returnin,2) ;(evalwcet2start,2) ;(evalwcet2stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalwcet2start(A,B) -> evalwcet2entryin(A,B) True evalwcet2entryin(A,B) -> evalwcet2bb5in(A,B) True evalwcet2bb5in(A,B) -> evalwcet2bb2in(A,0) [4 >= A] evalwcet2bb5in(A,B) -> evalwcet2returnin(A,B) [A >= 5] evalwcet2bb2in(A,B) -> evalwcet2bb1in(A,B) [A >= 3 && 9 >= B] evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [2 >= A] evalwcet2bb2in(A,B) -> evalwcet2bb4in(A,B) [B >= 10] evalwcet2bb1in(A,B) -> evalwcet2bb2in(A,1 + B) True evalwcet2bb4in(A,B) -> evalwcet2bb5in(1 + A,B) True evalwcet2returnin(A,B) -> evalwcet2stop(A,B) True Signature: {(evalwcet2bb1in,2) ;(evalwcet2bb2in,2) ;(evalwcet2bb4in,2) ;(evalwcet2bb5in,2) ;(evalwcet2entryin,2) ;(evalwcet2returnin,2) ;(evalwcet2start,2) ;(evalwcet2stop,2)} Rule Graph: [0->{1},1->{2,3},2->{4,5},3->{9},4->{7},5->{8},6->{8},7->{4,5,6},8->{2,3},9->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalwcet2start.0(A,B) -> evalwcet2entryin.1(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.2(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.3(A,B) True evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.4(A,0) [4 >= A] evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.5(A,0) [4 >= A] evalwcet2bb5in.3(A,B) -> evalwcet2returnin.9(A,B) [A >= 5] evalwcet2bb2in.4(A,B) -> evalwcet2bb1in.7(A,B) [A >= 3 && 9 >= B] evalwcet2bb2in.5(A,B) -> evalwcet2bb4in.8(A,B) [2 >= A] evalwcet2bb2in.6(A,B) -> evalwcet2bb4in.8(A,B) [B >= 10] evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.4(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.5(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.6(A,1 + B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.2(1 + A,B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.3(1 + A,B) True evalwcet2returnin.9(A,B) -> evalwcet2stop.10(A,B) True Signature: {(evalwcet2bb1in.7,2) ;(evalwcet2bb2in.4,2) ;(evalwcet2bb2in.5,2) ;(evalwcet2bb2in.6,2) ;(evalwcet2bb4in.8,2) ;(evalwcet2bb5in.2,2) ;(evalwcet2bb5in.3,2) ;(evalwcet2entryin.1,2) ;(evalwcet2returnin.9,2) ;(evalwcet2start.0,2) ;(evalwcet2stop.10,2)} Rule Graph: [0->{1,2},1->{3,4},2->{5},3->{6},4->{7},5->{14},6->{9,10,11},7->{12,13},8->{12,13},9->{6},10->{7},11->{8} ,12->{3,4},13->{5},14->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalwcet2start.0(A,B) -> evalwcet2entryin.1(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.2(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.3(A,B) True evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.4(A,0) [4 >= A] evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.5(A,0) [4 >= A] evalwcet2bb5in.3(A,B) -> evalwcet2returnin.9(A,B) [A >= 5] evalwcet2bb2in.4(A,B) -> evalwcet2bb1in.7(A,B) [A >= 3 && 9 >= B] evalwcet2bb2in.5(A,B) -> evalwcet2bb4in.8(A,B) [2 >= A] evalwcet2bb2in.6(A,B) -> evalwcet2bb4in.8(A,B) [B >= 10] evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.4(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.5(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.6(A,1 + B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.2(1 + A,B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.3(1 + A,B) True evalwcet2returnin.9(A,B) -> evalwcet2stop.10(A,B) True evalwcet2stop.10(A,B) -> exitus616(A,B) True evalwcet2stop.10(A,B) -> exitus616(A,B) True Signature: {(evalwcet2bb1in.7,2) ;(evalwcet2bb2in.4,2) ;(evalwcet2bb2in.5,2) ;(evalwcet2bb2in.6,2) ;(evalwcet2bb4in.8,2) ;(evalwcet2bb5in.2,2) ;(evalwcet2bb5in.3,2) ;(evalwcet2entryin.1,2) ;(evalwcet2returnin.9,2) ;(evalwcet2start.0,2) ;(evalwcet2stop.10,2) ;(exitus616,2)} Rule Graph: [0->{1,2},1->{3,4},2->{5},3->{6},4->{7},5->{14},6->{9,10,11},7->{12,13},8->{12,13},9->{6},10->{7},11->{8} ,12->{3,4},13->{5},14->{15,16}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | `- p:[3,12,7,4,10,6,9,8,11] c: [3,4,7,8,10,11,12] | `- p:[6,9] c: [6,9] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalwcet2start.0(A,B) -> evalwcet2entryin.1(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.2(A,B) True evalwcet2entryin.1(A,B) -> evalwcet2bb5in.3(A,B) True evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.4(A,0) [4 >= A] evalwcet2bb5in.2(A,B) -> evalwcet2bb2in.5(A,0) [4 >= A] evalwcet2bb5in.3(A,B) -> evalwcet2returnin.9(A,B) [A >= 5] evalwcet2bb2in.4(A,B) -> evalwcet2bb1in.7(A,B) [A >= 3 && 9 >= B] evalwcet2bb2in.5(A,B) -> evalwcet2bb4in.8(A,B) [2 >= A] evalwcet2bb2in.6(A,B) -> evalwcet2bb4in.8(A,B) [B >= 10] evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.4(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.5(A,1 + B) True evalwcet2bb1in.7(A,B) -> evalwcet2bb2in.6(A,1 + B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.2(1 + A,B) True evalwcet2bb4in.8(A,B) -> evalwcet2bb5in.3(1 + A,B) True evalwcet2returnin.9(A,B) -> evalwcet2stop.10(A,B) True evalwcet2stop.10(A,B) -> exitus616(A,B) True evalwcet2stop.10(A,B) -> exitus616(A,B) True Signature: {(evalwcet2bb1in.7,2) ;(evalwcet2bb2in.4,2) ;(evalwcet2bb2in.5,2) ;(evalwcet2bb2in.6,2) ;(evalwcet2bb4in.8,2) ;(evalwcet2bb5in.2,2) ;(evalwcet2bb5in.3,2) ;(evalwcet2entryin.1,2) ;(evalwcet2returnin.9,2) ;(evalwcet2start.0,2) ;(evalwcet2stop.10,2) ;(exitus616,2)} Rule Graph: [0->{1,2},1->{3,4},2->{5},3->{6},4->{7},5->{14},6->{9,10,11},7->{12,13},8->{12,13},9->{6},10->{7},11->{8} ,12->{3,4},13->{5},14->{15,16}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | `- p:[3,12,7,4,10,6,9,8,11] c: [3,4,7,8,10,11,12] | `- p:[6,9] c: [6,9]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.0.0] evalwcet2start.0 ~> evalwcet2entryin.1 [A <= A, B <= B] evalwcet2entryin.1 ~> evalwcet2bb5in.2 [A <= A, B <= B] evalwcet2entryin.1 ~> evalwcet2bb5in.3 [A <= A, B <= B] evalwcet2bb5in.2 ~> evalwcet2bb2in.4 [A <= A, B <= 0*K] evalwcet2bb5in.2 ~> evalwcet2bb2in.5 [A <= A, B <= 0*K] evalwcet2bb5in.3 ~> evalwcet2returnin.9 [A <= A, B <= B] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [A <= A, B <= B] evalwcet2bb2in.5 ~> evalwcet2bb4in.8 [A <= A, B <= B] evalwcet2bb2in.6 ~> evalwcet2bb4in.8 [A <= A, B <= B] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [A <= A, B <= K + B] evalwcet2bb1in.7 ~> evalwcet2bb2in.5 [A <= A, B <= K + B] evalwcet2bb1in.7 ~> evalwcet2bb2in.6 [A <= A, B <= K + B] evalwcet2bb4in.8 ~> evalwcet2bb5in.2 [A <= K + A, B <= B] evalwcet2bb4in.8 ~> evalwcet2bb5in.3 [A <= K + A, B <= B] evalwcet2returnin.9 ~> evalwcet2stop.10 [A <= A, B <= B] evalwcet2stop.10 ~> exitus616 [A <= A, B <= B] evalwcet2stop.10 ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= 4*K + A] evalwcet2bb5in.2 ~> evalwcet2bb2in.4 [A <= A, B <= 0*K] evalwcet2bb4in.8 ~> evalwcet2bb5in.2 [A <= K + A, B <= B] evalwcet2bb2in.5 ~> evalwcet2bb4in.8 [A <= A, B <= B] evalwcet2bb5in.2 ~> evalwcet2bb2in.5 [A <= A, B <= 0*K] evalwcet2bb1in.7 ~> evalwcet2bb2in.5 [A <= A, B <= K + B] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [A <= A, B <= B] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [A <= A, B <= K + B] evalwcet2bb2in.6 ~> evalwcet2bb4in.8 [A <= A, B <= B] evalwcet2bb1in.7 ~> evalwcet2bb2in.6 [A <= A, B <= K + B] + Loop: [0.0.0 <= 9*K + B] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [A <= A, B <= B] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [A <= A, B <= K + B] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.0.0] evalwcet2start.0 ~> evalwcet2entryin.1 [] evalwcet2entryin.1 ~> evalwcet2bb5in.2 [] evalwcet2entryin.1 ~> evalwcet2bb5in.3 [] evalwcet2bb5in.2 ~> evalwcet2bb2in.4 [K ~=> B] evalwcet2bb5in.2 ~> evalwcet2bb2in.5 [K ~=> B] evalwcet2bb5in.3 ~> evalwcet2returnin.9 [] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [] evalwcet2bb2in.5 ~> evalwcet2bb4in.8 [] evalwcet2bb2in.6 ~> evalwcet2bb4in.8 [] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [B ~+> B,K ~+> B] evalwcet2bb1in.7 ~> evalwcet2bb2in.5 [B ~+> B,K ~+> B] evalwcet2bb1in.7 ~> evalwcet2bb2in.6 [B ~+> B,K ~+> B] evalwcet2bb4in.8 ~> evalwcet2bb5in.2 [A ~+> A,K ~+> A] evalwcet2bb4in.8 ~> evalwcet2bb5in.3 [A ~+> A,K ~+> A] evalwcet2returnin.9 ~> evalwcet2stop.10 [] evalwcet2stop.10 ~> exitus616 [] evalwcet2stop.10 ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] evalwcet2bb5in.2 ~> evalwcet2bb2in.4 [K ~=> B] evalwcet2bb4in.8 ~> evalwcet2bb5in.2 [A ~+> A,K ~+> A] evalwcet2bb2in.5 ~> evalwcet2bb4in.8 [] evalwcet2bb5in.2 ~> evalwcet2bb2in.5 [K ~=> B] evalwcet2bb1in.7 ~> evalwcet2bb2in.5 [B ~+> B,K ~+> B] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [B ~+> B,K ~+> B] evalwcet2bb2in.6 ~> evalwcet2bb4in.8 [] evalwcet2bb1in.7 ~> evalwcet2bb2in.6 [B ~+> B,K ~+> B] + Loop: [B ~+> 0.0.0,K ~*> 0.0.0] evalwcet2bb2in.4 ~> evalwcet2bb1in.7 [] evalwcet2bb1in.7 ~> evalwcet2bb2in.4 [B ~+> B,K ~+> B] + Applied Processor: Lare + Details: evalwcet2start.0 ~> exitus616 [K ~=> B ,A ~+> A ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalwcet2bb4in.8> [K ~=> B ,A ~+> A ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalwcet2bb1in.7> [B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,B ~*> B ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick] YES(?,POLY)