YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Flow Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6} ,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. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (1,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (1,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (1,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (1,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Flow Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6} ,11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7),(5,8),(9,4),(10,5)] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (1,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (1,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (1,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (1,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (1,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Flow Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{8},5->{7},6->{11},7->{9},8->{10},9->{5,6},10->{4,6},11->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) 12. evalwisereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2) ;(exitus616,2)} Flow Graph: [0->{1,2,3},1->{11,12},2->{11,12},3->{4,5,6},4->{7,8},5->{7,8},6->{11,12},7->{9},8->{10},9->{4,5,6},10->{4 ,5,6},11->{},12->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7),(5,8),(9,4),(10,5)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) 12. evalwisereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2) ;(exitus616,2)} Flow Graph: [0->{1,2,3},1->{11,12},2->{11,12},3->{4,5,6},4->{8},5->{7},6->{11,12},7->{9},8->{10},9->{5,6},10->{4,6} ,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:[5,9,7] c: [9] | `- p:[4,10,8] c: [10] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) 12. evalwisereturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2) ;(exitus616,2)} Flow Graph: [0->{1,2,3},1->{11,12},2->{11,12},3->{4,5,6},4->{8},5->{7},6->{11,12},7->{9},8->{10},9->{5,6},10->{4,6} ,11->{},12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[5,9,7] c: [9] | `- p:[4,10,8] c: [10]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.1] evalwisestart ~> evalwiseentryin [A <= A, B <= B] evalwiseentryin ~> evalwisereturnin [A <= A, B <= B] evalwiseentryin ~> evalwisereturnin [A <= A, B <= B] evalwiseentryin ~> evalwisebb6in [A <= B, B <= A] evalwisebb6in ~> evalwisebb3in [A <= A, B <= B] evalwisebb6in ~> evalwisebb3in [A <= A, B <= B] evalwisebb6in ~> evalwisereturnin [A <= A, B <= B] evalwisebb3in ~> evalwisebb4in [A <= A, B <= B] evalwisebb3in ~> evalwisebb5in [A <= A, B <= B] evalwisebb4in ~> evalwisebb6in [A <= A, B <= A] evalwisebb5in ~> evalwisebb6in [A <= A + B, B <= B] evalwisereturnin ~> evalwisestop [A <= A, B <= B] evalwisereturnin ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= A + B] evalwisebb6in ~> evalwisebb3in [A <= A, B <= B] evalwisebb4in ~> evalwisebb6in [A <= A, B <= A] evalwisebb3in ~> evalwisebb4in [A <= A, B <= B] + Loop: [0.1 <= K + A + B] evalwisebb6in ~> evalwisebb3in [A <= A, B <= B] evalwisebb5in ~> evalwisebb6in [A <= A + B, B <= B] evalwisebb3in ~> evalwisebb5in [A <= 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] evalwisestart ~> evalwiseentryin [] evalwiseentryin ~> evalwisereturnin [] evalwiseentryin ~> evalwisereturnin [] evalwiseentryin ~> evalwisebb6in [A ~=> B,B ~=> A] evalwisebb6in ~> evalwisebb3in [] evalwisebb6in ~> evalwisebb3in [] evalwisebb6in ~> evalwisereturnin [] evalwisebb3in ~> evalwisebb4in [] evalwisebb3in ~> evalwisebb5in [] evalwisebb4in ~> evalwisebb6in [A ~=> B] evalwisebb5in ~> evalwisebb6in [A ~+> A,B ~+> A] evalwisereturnin ~> evalwisestop [] evalwisereturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] evalwisebb6in ~> evalwisebb3in [] evalwisebb4in ~> evalwisebb6in [A ~=> B] evalwisebb3in ~> evalwisebb4in [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~+> 0.1] evalwisebb6in ~> evalwisebb3in [] evalwisebb5in ~> evalwisebb6in [A ~+> A,B ~+> A] evalwisebb3in ~> evalwisebb5in [] + Applied Processor: LareProcessor + Details: evalwisestart ~> evalwisebb3in [A ~=> B ,B ~=> A ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> B ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> 0.0 ,A ~*> 0.1 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> 0.0 ,B ~*> 0.1 ,B ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] evalwisestart ~> evalwisestop [A ~=> B ,B ~=> A ,A ~+> A ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,B ~*> A ,K ~*> A] evalwisestart ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> A ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,B ~*> A ,K ~*> A] + evalwisebb3in> [A ~=> B,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick] evalwisebb6in> [A ~=> B,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick] + evalwisebb3in> [A ~+> A ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,B ~*> A ,K ~*> A] evalwisebb6in> [A ~+> A ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,B ~*> A ,K ~*> A] YES(?,POLY)