YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (?,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (?,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (?,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (?,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2)} Flow Graph: [0->{1,2},1->{3,4},2->{11},3->{5,6},4->{11},5->{7,8},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},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. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (1,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (1,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (1,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (1,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2)} Flow Graph: [0->{1,2},1->{3,4},2->{11},3->{5,6},4->{11},5->{7,8},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(5,8)] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (1,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (1,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (1,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (1,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2)} Flow Graph: [0->{1,2},1->{3},2->{11},3->{5,6},4->{11},5->{7},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},11->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (?,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (?,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (?,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (?,1) 12. evalloopsreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3,4},2->{11,12},3->{5,6},4->{11,12},5->{7,8},6->{10},7->{9},8->{10},9->{7,8},10->{3,4} ,11->{},12->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(5,8)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (?,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (?,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (?,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (?,1) 12. evalloopsreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3},2->{11,12},3->{5,6},4->{11,12},5->{7},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},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,10,6,8,9,7,5] c: [10] | `- p:[7,9] c: [9] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. evalloopsstart(A,B) -> evalloopsentryin(A,B) True (1,1) 1. evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] (?,1) 2. evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] (?,1) 3. evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] (?,1) 4. evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] (?,1) 5. evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] (?,1) 6. evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] (?,1) 7. evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] (?,1) 8. evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] (?,1) 9. evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] (?,1) 11. evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] (?,1) 12. evalloopsreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3},2->{11,12},3->{5,6},4->{11,12},5->{7},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},11->{} ,12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[3,10,6,8,9,7,5] c: [10] | `- p:[7,9] c: [9]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.0.0] evalloopsstart ~> evalloopsentryin [A <= A, B <= B] evalloopsentryin ~> evalloopsbb6in [A <= A, B <= B] evalloopsentryin ~> evalloopsreturnin [A <= A, B <= B] evalloopsbb6in ~> evalloopsbb1in [A <= A, B <= B] evalloopsbb6in ~> evalloopsreturnin [A <= A, B <= B] evalloopsbb1in ~> evalloopsbb4in [A <= A, B <= K] evalloopsbb1in ~> evalloopsbb5in [A <= A, B <= unknown] evalloopsbb4in ~> evalloopsbb3in [A <= A, B <= B] evalloopsbb4in ~> evalloopsbb5in [A <= A, B <= B] evalloopsbb3in ~> evalloopsbb4in [A <= A, B <= A + B] evalloopsbb5in ~> evalloopsbb6in [A <= K + A, B <= B] evalloopsreturnin ~> evalloopsstop [A <= A, B <= B] evalloopsreturnin ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= K + A] evalloopsbb6in ~> evalloopsbb1in [A <= A, B <= B] evalloopsbb5in ~> evalloopsbb6in [A <= K + A, B <= B] evalloopsbb1in ~> evalloopsbb5in [A <= A, B <= unknown] evalloopsbb4in ~> evalloopsbb5in [A <= A, B <= B] evalloopsbb3in ~> evalloopsbb4in [A <= A, B <= A + B] evalloopsbb4in ~> evalloopsbb3in [A <= A, B <= B] evalloopsbb1in ~> evalloopsbb4in [A <= A, B <= K] + Loop: [0.0.0 <= A + B] evalloopsbb4in ~> evalloopsbb3in [A <= A, B <= B] evalloopsbb3in ~> evalloopsbb4in [A <= A, B <= A + B] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.0.0] evalloopsstart ~> evalloopsentryin [] evalloopsentryin ~> evalloopsbb6in [] evalloopsentryin ~> evalloopsreturnin [] evalloopsbb6in ~> evalloopsbb1in [] evalloopsbb6in ~> evalloopsreturnin [] evalloopsbb1in ~> evalloopsbb4in [K ~=> B] evalloopsbb1in ~> evalloopsbb5in [huge ~=> B] evalloopsbb4in ~> evalloopsbb3in [] evalloopsbb4in ~> evalloopsbb5in [] evalloopsbb3in ~> evalloopsbb4in [A ~+> B,B ~+> B] evalloopsbb5in ~> evalloopsbb6in [A ~+> A,K ~+> A] evalloopsreturnin ~> evalloopsstop [] evalloopsreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,K ~+> 0.0] evalloopsbb6in ~> evalloopsbb1in [] evalloopsbb5in ~> evalloopsbb6in [A ~+> A,K ~+> A] evalloopsbb1in ~> evalloopsbb5in [huge ~=> B] evalloopsbb4in ~> evalloopsbb5in [] evalloopsbb3in ~> evalloopsbb4in [A ~+> B,B ~+> B] evalloopsbb4in ~> evalloopsbb3in [] evalloopsbb1in ~> evalloopsbb4in [K ~=> B] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0] evalloopsbb4in ~> evalloopsbb3in [] evalloopsbb3in ~> evalloopsbb4in [A ~+> B,B ~+> B] + Applied Processor: LareProcessor + Details: evalloopsstart ~> exitus616 [K ~=> B ,huge ~=> B ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,K ~^> B] evalloopsstart ~> evalloopsstop [K ~=> B ,huge ~=> B ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,K ~^> B] + evalloopsbb6in> [K ~=> B ,huge ~=> B ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,K ~^> B] + evalloopsbb4in> [A ~+> B ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> B ,B ~*> B] YES(?,POLY)