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