YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1) 1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1) 2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [A >= 0 && B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [A >= 0 && B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= 0 && A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) [A + -1*B >= 0 && A >= 0] (?,1) Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2)} Flow Graph: [0->{1},1->{2,3},2->{8,9},3->{4,5,6},4->{7},5->{7},6->{8,9},7->{2,3},8->{10},9->{11},10->{8,9},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,8),(6,9)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True (1,1) 1. evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True (?,1) 2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [A >= 0 && B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [A >= 0 && B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= 0 && A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) [A + -1*B >= 0 && A >= 0] (?,1) Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2)} Flow Graph: [0->{1},1->{2,3},2->{9},3->{4,5,6},4->{7},5->{7},6->{8},7->{2,3},8->{10},9->{11},10->{8,9},11->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + C] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= 0 && A >= B] evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) [A + -1*B >= 0 && A >= 0] Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2)} Rule Graph: [0->{1},1->{2,3},2->{9},3->{4,5,6},4->{7},5->{7},6->{8},7->{2,3},8->{10},9->{11},10->{8,9},11->{}] + Applied Processor: AddSinks + Details: () * Step 4: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + C] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= 0 && A >= B] evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) [A + -1*B >= 0 && A >= 0] evalSequentialSinglestop(A,B) -> exitus616(A,B) True evalSequentialSinglestop(A,B) -> exitus616(A,B) True Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2,3},2->{9},3->{4,5,6},4->{7},5->{7},6->{8},7->{2,3},8->{10},9->{11},10->{8,9},11->{12,13}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | +- p:[3,7,4,5] c: [3,4,5,7] | `- p:[8,10] c: [8,10] * Step 5: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalSequentialSinglestart(A,B) -> evalSequentialSingleentryin(A,B) True evalSequentialSingleentryin(A,B) -> evalSequentialSinglebb1in(0,B) True evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + C] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [A >= 0 && B >= 1 + A] evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= 0 && A >= B] evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) [A + -1*B >= 0 && A >= 0] evalSequentialSinglestop(A,B) -> exitus616(A,B) True evalSequentialSinglestop(A,B) -> exitus616(A,B) True Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2,3},2->{9},3->{4,5,6},4->{7},5->{7},6->{8},7->{2,3},8->{10},9->{11},10->{8,9},11->{12,13}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | +- p:[3,7,4,5] c: [3,4,5,7] | `- p:[8,10] c: [8,10]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.1] evalSequentialSinglestart ~> evalSequentialSingleentryin [A <= A, B <= B] evalSequentialSingleentryin ~> evalSequentialSinglebb1in [A <= 0*K, B <= B] evalSequentialSinglebb1in ~> evalSequentialSinglebb5in [A <= A, B <= B] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [A <= A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebb5in [A <= A, B <= B] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [A <= B, B <= B] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [A <= A, B <= B] evalSequentialSinglebb5in ~> evalSequentialSinglereturnin [A <= A, B <= B] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A <= B, B <= B] evalSequentialSinglereturnin ~> evalSequentialSinglestop [A <= A, B <= B] evalSequentialSinglestop ~> exitus616 [A <= A, B <= B] evalSequentialSinglestop ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= A + B] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [A <= A, B <= B] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [A <= B, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] + Loop: [0.1 <= K + A + B] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [A <= A, B <= B] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A <= B, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.1] evalSequentialSinglestart ~> evalSequentialSingleentryin [] evalSequentialSingleentryin ~> evalSequentialSinglebb1in [K ~=> A] evalSequentialSinglebb1in ~> evalSequentialSinglebb5in [] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] evalSequentialSinglebb2in ~> evalSequentialSinglebb5in [] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [B ~=> A] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [] evalSequentialSinglebb5in ~> evalSequentialSinglereturnin [] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [B ~=> A] evalSequentialSinglereturnin ~> evalSequentialSinglestop [] evalSequentialSinglestop ~> exitus616 [] evalSequentialSinglestop ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [B ~=> A] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~+> 0.1] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [B ~=> A] + Applied Processor: Lare + Details: evalSequentialSinglestart ~> exitus616 [B ~=> A ,K ~=> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,B ~*> 0.0 ,B ~*> 0.1 ,B ~*> tick ,K ~*> 0.1 ,K ~*> tick] + evalSequentialSinglebb2in> [B ~=> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick] evalSequentialSinglebb1in> [B ~=> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick] + evalSequentialSinglebb5in> [B ~=> A ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick] YES(?,POLY)