YES(?,POLY) * Step 1: 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) 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 2: FromIts 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},2->{11},3->{5,6},4->{11},5->{7},6->{10},7->{9},8->{10},9->{7,8},10->{3,4},11->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalloopsstart(A,B) -> evalloopsentryin(A,B) True evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2)} Rule 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: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalloopsstart(A,B) -> evalloopsentryin(A,B) True evalloopsentryin(A,B) -> evalloopsbb6in(A,B) [A >= 0] evalloopsentryin(A,B) -> evalloopsreturnin(A,B) [0 >= 1 + A] evalloopsbb6in(A,B) -> evalloopsbb1in(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in(A,B) -> evalloopsreturnin(A,B) [1 + A >= 0 && 0 >= 1 + A] evalloopsbb1in(A,B) -> evalloopsbb4in(A,1) [A >= 0 && A >= 2] evalloopsbb1in(A,B) -> evalloopsbb5in(A,C) [A >= 0 && 1 >= A] evalloopsbb4in(A,B) -> evalloopsbb3in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] evalloopsbb4in(A,B) -> evalloopsbb5in(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] evalloopsbb3in(A,B) -> evalloopsbb4in(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb5in(A,B) -> evalloopsbb6in(-1 + A,B) [A >= 0] evalloopsreturnin(A,B) -> evalloopsstop(A,B) [-1 + -1*A >= 0] evalloopsstop(A,B) -> exitus616(A,B) True evalloopsstop(A,B) -> exitus616(A,B) True Signature: {(evalloopsbb1in,2) ;(evalloopsbb3in,2) ;(evalloopsbb4in,2) ;(evalloopsbb5in,2) ;(evalloopsbb6in,2) ;(evalloopsentryin,2) ;(evalloopsreturnin,2) ;(evalloopsstart,2) ;(evalloopsstop,2) ;(exitus616,2)} Rule 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->{12,13}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalloopsstart.0(A,B) -> evalloopsentryin.1(A,B) True evalloopsstart.0(A,B) -> evalloopsentryin.2(A,B) True evalloopsentryin.1(A,B) -> evalloopsbb6in.3(A,B) [A >= 0] evalloopsentryin.2(A,B) -> evalloopsreturnin.11(A,B) [0 >= 1 + A] evalloopsbb6in.3(A,B) -> evalloopsbb1in.5(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in.3(A,B) -> evalloopsbb1in.6(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in.4(A,B) -> evalloopsreturnin.11(A,B) [1 + A >= 0 && 0 >= 1 + A] evalloopsbb1in.5(A,B) -> evalloopsbb4in.7(A,1) [A >= 0 && A >= 2] evalloopsbb1in.6(A,B) -> evalloopsbb5in.10(A,C) [A >= 0 && 1 >= A] evalloopsbb4in.7(A,B) -> evalloopsbb3in.9(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] evalloopsbb4in.8(A,B) -> evalloopsbb5in.10(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] evalloopsbb3in.9(A,B) -> evalloopsbb4in.7(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb3in.9(A,B) -> evalloopsbb4in.8(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb5in.10(A,B) -> evalloopsbb6in.3(-1 + A,B) [A >= 0] evalloopsbb5in.10(A,B) -> evalloopsbb6in.4(-1 + A,B) [A >= 0] evalloopsreturnin.11(A,B) -> evalloopsstop.12(A,B) [-1 + -1*A >= 0] evalloopsreturnin.11(A,B) -> evalloopsstop.13(A,B) [-1 + -1*A >= 0] evalloopsstop.12(A,B) -> exitus616.14(A,B) True evalloopsstop.13(A,B) -> exitus616.14(A,B) True Signature: {(evalloopsbb1in.5,2) ;(evalloopsbb1in.6,2) ;(evalloopsbb3in.9,2) ;(evalloopsbb4in.7,2) ;(evalloopsbb4in.8,2) ;(evalloopsbb5in.10,2) ;(evalloopsbb6in.3,2) ;(evalloopsbb6in.4,2) ;(evalloopsentryin.1,2) ;(evalloopsentryin.2,2) ;(evalloopsreturnin.11,2) ;(evalloopsstart.0,2) ;(evalloopsstop.12,2) ;(evalloopsstop.13,2) ;(exitus616.14,2)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{15,16},4->{7},5->{8},6->{15,16},7->{9},8->{13,14},9->{11,12},10->{13,14} ,11->{9},12->{10},13->{4,5},14->{6},15->{17},16->{18},17->{},18->{}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | `- p:[4,13,8,5,10,12,9,7,11] c: [4,5,7,8,10,12,13] | `- p:[9,11] c: [9,11] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalloopsstart.0(A,B) -> evalloopsentryin.1(A,B) True evalloopsstart.0(A,B) -> evalloopsentryin.2(A,B) True evalloopsentryin.1(A,B) -> evalloopsbb6in.3(A,B) [A >= 0] evalloopsentryin.2(A,B) -> evalloopsreturnin.11(A,B) [0 >= 1 + A] evalloopsbb6in.3(A,B) -> evalloopsbb1in.5(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in.3(A,B) -> evalloopsbb1in.6(A,B) [1 + A >= 0 && A >= 0] evalloopsbb6in.4(A,B) -> evalloopsreturnin.11(A,B) [1 + A >= 0 && 0 >= 1 + A] evalloopsbb1in.5(A,B) -> evalloopsbb4in.7(A,1) [A >= 0 && A >= 2] evalloopsbb1in.6(A,B) -> evalloopsbb5in.10(A,C) [A >= 0 && 1 >= A] evalloopsbb4in.7(A,B) -> evalloopsbb3in.9(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B] evalloopsbb4in.8(A,B) -> evalloopsbb5in.10(A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && B >= A] evalloopsbb3in.9(A,B) -> evalloopsbb4in.7(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb3in.9(A,B) -> evalloopsbb4in.8(A,2*B) [-1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalloopsbb5in.10(A,B) -> evalloopsbb6in.3(-1 + A,B) [A >= 0] evalloopsbb5in.10(A,B) -> evalloopsbb6in.4(-1 + A,B) [A >= 0] evalloopsreturnin.11(A,B) -> evalloopsstop.12(A,B) [-1 + -1*A >= 0] evalloopsreturnin.11(A,B) -> evalloopsstop.13(A,B) [-1 + -1*A >= 0] evalloopsstop.12(A,B) -> exitus616.14(A,B) True evalloopsstop.13(A,B) -> exitus616.14(A,B) True Signature: {(evalloopsbb1in.5,2) ;(evalloopsbb1in.6,2) ;(evalloopsbb3in.9,2) ;(evalloopsbb4in.7,2) ;(evalloopsbb4in.8,2) ;(evalloopsbb5in.10,2) ;(evalloopsbb6in.3,2) ;(evalloopsbb6in.4,2) ;(evalloopsentryin.1,2) ;(evalloopsentryin.2,2) ;(evalloopsreturnin.11,2) ;(evalloopsstart.0,2) ;(evalloopsstop.12,2) ;(evalloopsstop.13,2) ;(exitus616.14,2)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{15,16},4->{7},5->{8},6->{15,16},7->{9},8->{13,14},9->{11,12},10->{13,14} ,11->{9},12->{10},13->{4,5},14->{6},15->{17},16->{18},17->{},18->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | `- p:[4,13,8,5,10,12,9,7,11] c: [4,5,7,8,10,12,13] | `- p:[9,11] c: [9,11]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.0.0] evalloopsstart.0 ~> evalloopsentryin.1 [A <= A, B <= B] evalloopsstart.0 ~> evalloopsentryin.2 [A <= A, B <= B] evalloopsentryin.1 ~> evalloopsbb6in.3 [A <= A, B <= B] evalloopsentryin.2 ~> evalloopsreturnin.11 [A <= A, B <= B] evalloopsbb6in.3 ~> evalloopsbb1in.5 [A <= A, B <= B] evalloopsbb6in.3 ~> evalloopsbb1in.6 [A <= A, B <= B] evalloopsbb6in.4 ~> evalloopsreturnin.11 [A <= A, B <= B] evalloopsbb1in.5 ~> evalloopsbb4in.7 [A <= A, B <= K] evalloopsbb1in.6 ~> evalloopsbb5in.10 [A <= A, B <= unknown] evalloopsbb4in.7 ~> evalloopsbb3in.9 [A <= A, B <= B] evalloopsbb4in.8 ~> evalloopsbb5in.10 [A <= A, B <= B] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A <= A, B <= A + B] evalloopsbb3in.9 ~> evalloopsbb4in.8 [A <= A, B <= A + B] evalloopsbb5in.10 ~> evalloopsbb6in.3 [A <= K + A, B <= B] evalloopsbb5in.10 ~> evalloopsbb6in.4 [A <= K + A, B <= B] evalloopsreturnin.11 ~> evalloopsstop.12 [A <= A, B <= B] evalloopsreturnin.11 ~> evalloopsstop.13 [A <= A, B <= B] evalloopsstop.12 ~> exitus616.14 [A <= A, B <= B] evalloopsstop.13 ~> exitus616.14 [A <= A, B <= B] + Loop: [0.0 <= A] evalloopsbb6in.3 ~> evalloopsbb1in.5 [A <= A, B <= B] evalloopsbb5in.10 ~> evalloopsbb6in.3 [A <= K + A, B <= B] evalloopsbb1in.6 ~> evalloopsbb5in.10 [A <= A, B <= unknown] evalloopsbb6in.3 ~> evalloopsbb1in.6 [A <= A, B <= B] evalloopsbb4in.8 ~> evalloopsbb5in.10 [A <= A, B <= B] evalloopsbb3in.9 ~> evalloopsbb4in.8 [A <= A, B <= A + B] evalloopsbb4in.7 ~> evalloopsbb3in.9 [A <= A, B <= B] evalloopsbb1in.5 ~> evalloopsbb4in.7 [A <= A, B <= K] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A <= A, B <= A + B] + Loop: [0.0.0 <= K + A + B] evalloopsbb4in.7 ~> evalloopsbb3in.9 [A <= A, B <= B] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A <= A, B <= A + B] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.0.0] evalloopsstart.0 ~> evalloopsentryin.1 [] evalloopsstart.0 ~> evalloopsentryin.2 [] evalloopsentryin.1 ~> evalloopsbb6in.3 [] evalloopsentryin.2 ~> evalloopsreturnin.11 [] evalloopsbb6in.3 ~> evalloopsbb1in.5 [] evalloopsbb6in.3 ~> evalloopsbb1in.6 [] evalloopsbb6in.4 ~> evalloopsreturnin.11 [] evalloopsbb1in.5 ~> evalloopsbb4in.7 [K ~=> B] evalloopsbb1in.6 ~> evalloopsbb5in.10 [huge ~=> B] evalloopsbb4in.7 ~> evalloopsbb3in.9 [] evalloopsbb4in.8 ~> evalloopsbb5in.10 [] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A ~+> B,B ~+> B] evalloopsbb3in.9 ~> evalloopsbb4in.8 [A ~+> B,B ~+> B] evalloopsbb5in.10 ~> evalloopsbb6in.3 [A ~+> A,K ~+> A] evalloopsbb5in.10 ~> evalloopsbb6in.4 [A ~+> A,K ~+> A] evalloopsreturnin.11 ~> evalloopsstop.12 [] evalloopsreturnin.11 ~> evalloopsstop.13 [] evalloopsstop.12 ~> exitus616.14 [] evalloopsstop.13 ~> exitus616.14 [] + Loop: [A ~=> 0.0] evalloopsbb6in.3 ~> evalloopsbb1in.5 [] evalloopsbb5in.10 ~> evalloopsbb6in.3 [A ~+> A,K ~+> A] evalloopsbb1in.6 ~> evalloopsbb5in.10 [huge ~=> B] evalloopsbb6in.3 ~> evalloopsbb1in.6 [] evalloopsbb4in.8 ~> evalloopsbb5in.10 [] evalloopsbb3in.9 ~> evalloopsbb4in.8 [A ~+> B,B ~+> B] evalloopsbb4in.7 ~> evalloopsbb3in.9 [] evalloopsbb1in.5 ~> evalloopsbb4in.7 [K ~=> B] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A ~+> B,B ~+> B] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] evalloopsbb4in.7 ~> evalloopsbb3in.9 [] evalloopsbb3in.9 ~> evalloopsbb4in.7 [A ~+> B,B ~+> B] + Applied Processor: Lare + Details: evalloopsstart.0 ~> exitus616.14 [A ~=> 0.0 ,huge ~=> B ,A ~+> A ,A ~+> B ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,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] + evalloopsbb5in.10> [A ~=> 0.0 ,huge ~=> B ,A ~+> A ,A ~+> B ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,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] + evalloopsbb3in.9> [A ~+> B ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,POLY)