YES(?,POLY) * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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,1) 2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] (1,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,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,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,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 3: AddSinks 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,1) 2. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb5in(A,B) [A >= 0 && A >= B] (1,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,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,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,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: AddSinks + Details: () * Step 4: 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) 12. evalSequentialSinglereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2) ;(exitus616,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,12},10->{8,9},11->{} ,12->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,8),(6,9)] * Step 5: LooptreeTransformer 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) 12. evalSequentialSinglereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2) ;(exitus616,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,12},10->{8,9},11->{} ,12->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3,7,4,5] c: [7] | `- p:[8,10] c: [10] * Step 6: SizeAbstraction 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) 12. evalSequentialSinglereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalSequentialSinglebb1in,2) ;(evalSequentialSinglebb2in,2) ;(evalSequentialSinglebb4in,2) ;(evalSequentialSinglebb5in,2) ;(evalSequentialSinglebbin,2) ;(evalSequentialSingleentryin,2) ;(evalSequentialSinglereturnin,2) ;(evalSequentialSinglestart,2) ;(evalSequentialSinglestop,2) ;(exitus616,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,12},10->{8,9},11->{} ,12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[3,7,4,5] c: [7] | `- p:[8,10] c: [10]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction 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] evalSequentialSinglereturnin ~> 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 <= A + B] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [A <= A, B <= B] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A <= B, B <= B] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor 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 [] evalSequentialSinglereturnin ~> 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] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [B ~=> A] + Applied Processor: LareProcessor + Details: evalSequentialSinglestart ~> evalSequentialSinglestop [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 ~*> tick] 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 ~*> 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] YES(?,POLY)