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 >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,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 >= B] (1,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (1,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (1,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (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)] * 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 >= B] (1,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (1,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (1,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (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,9},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 >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,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)] * 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 >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,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,9},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: [3] | `- p:[8,10] c: [8] * 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 >= B] (?,1) 3. evalSequentialSinglebb1in(A,B) -> evalSequentialSinglebb2in(A,B) [B >= 1 + A] (?,1) 4. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [0 >= 1 + C] (?,1) 5. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebbin(A,B) [C >= 1] (?,1) 6. evalSequentialSinglebb2in(A,B) -> evalSequentialSinglebb5in(A,B) True (?,1) 7. evalSequentialSinglebbin(A,B) -> evalSequentialSinglebb1in(1 + A,B) True (?,1) 8. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglebb4in(A,B) [B >= 1 + A] (?,1) 9. evalSequentialSinglebb5in(A,B) -> evalSequentialSinglereturnin(A,B) [A >= B] (?,1) 10. evalSequentialSinglebb4in(A,B) -> evalSequentialSinglebb5in(1 + A,B) True (?,1) 11. evalSequentialSinglereturnin(A,B) -> evalSequentialSinglestop(A,B) True (?,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,9},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: [3] | `- p:[8,10] c: [8]) + 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 <= K + A, B <= B] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [A <= A, B <= B] evalSequentialSinglebb5in ~> evalSequentialSinglereturnin [A <= A, B <= B] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A <= K + A, B <= B] evalSequentialSinglereturnin ~> evalSequentialSinglestop [A <= A, B <= B] evalSequentialSinglereturnin ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= 2*K + A + B] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [A <= A, B <= B] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [A <= K + A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [A <= A, B <= B] + Loop: [0.1 <= 2*K + A + B] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [A <= A, B <= B] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A <= K + A, 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 [A ~+> A,K ~+> A] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [] evalSequentialSinglebb5in ~> evalSequentialSinglereturnin [] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A ~+> A,K ~+> A] evalSequentialSinglereturnin ~> evalSequentialSinglestop [] evalSequentialSinglereturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] evalSequentialSinglebb1in ~> evalSequentialSinglebb2in [] evalSequentialSinglebbin ~> evalSequentialSinglebb1in [A ~+> A,K ~+> A] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] evalSequentialSinglebb2in ~> evalSequentialSinglebbin [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~*> 0.1] evalSequentialSinglebb5in ~> evalSequentialSinglebb4in [] evalSequentialSinglebb4in ~> evalSequentialSinglebb5in [A ~+> A,K ~+> A] + Applied Processor: LareProcessor + Details: evalSequentialSinglestart ~> evalSequentialSinglestop [K ~=> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,B ~*> A ,B ~*> 0.0 ,B ~*> 0.1 ,B ~*> tick ,K ~*> A ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] evalSequentialSinglestart ~> exitus616 [K ~=> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> tick ,B ~*> A ,B ~*> 0.0 ,B ~*> 0.1 ,B ~*> tick ,K ~*> A ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] + evalSequentialSinglebb2in> [A ~+> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,A ~*> A ,B ~*> A ,K ~*> A ,K ~*> 0.0 ,K ~*> tick] evalSequentialSinglebb1in> [A ~+> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,A ~*> A ,B ~*> A ,K ~*> A ,K ~*> 0.0 ,K ~*> tick] + evalSequentialSinglebb5in> [A ~+> A ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,A ~*> A ,B ~*> A ,K ~*> A ,K ~*> 0.1 ,K ~*> tick] YES(?,POLY)