YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (?,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (?,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3)] * Step 2: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (?,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (?,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,O(1)) + Considered Problem: Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] evaleasy1stop(A,B) -> exitus616(A,B) True Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2) ;(exitus616,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{10}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: evaleasy1start.0(A,B) -> evaleasy1entryin.1(A,B) True evaleasy1entryin.1(A,B) -> evaleasy1bb3in.2(0,B) True evaleasy1bb3in.2(A,B) -> evaleasy1bbin.4(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.2(A,B) -> evaleasy1bbin.5(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.2(A,B) -> evaleasy1bbin.6(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.3(A,B) -> evaleasy1returnin.9(A,B) [A >= 0 && A >= 40] evaleasy1bbin.4(A,B) -> evaleasy1bb1in.7(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin.5(A,B) -> evaleasy1bb2in.8(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin.6(A,B) -> evaleasy1bb2in.8(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in.7(A,B) -> evaleasy1bb3in.2(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb1in.7(A,B) -> evaleasy1bb3in.3(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in.8(A,B) -> evaleasy1bb3in.2(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1bb2in.8(A,B) -> evaleasy1bb3in.3(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin.9(A,B) -> evaleasy1stop.10(A,B) [-40 + A >= 0] evaleasy1stop.10(A,B) -> exitus616.11(A,B) True Signature: {(evaleasy1bb1in.7,2) ;(evaleasy1bb2in.8,2) ;(evaleasy1bb3in.2,2) ;(evaleasy1bb3in.3,2) ;(evaleasy1bbin.4,2) ;(evaleasy1bbin.5,2) ;(evaleasy1bbin.6,2) ;(evaleasy1entryin.1,2) ;(evaleasy1returnin.9,2) ;(evaleasy1start.0,2) ;(evaleasy1stop.10,2) ;(exitus616.11,2)} Rule Graph: [0->{1},1->{2,3,4},2->{6},3->{7},4->{8},5->{13},6->{9,10},7->{11,12},8->{11,12},9->{2,3,4},10->{5},11->{2 ,3,4},12->{5},13->{14},14->{}] + 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] | `- p:[2,9,6,11,7,3,8,4] c: [2,3,4,6,7,8,9,11] * Step 6: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: evaleasy1start.0(A,B) -> evaleasy1entryin.1(A,B) True evaleasy1entryin.1(A,B) -> evaleasy1bb3in.2(0,B) True evaleasy1bb3in.2(A,B) -> evaleasy1bbin.4(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.2(A,B) -> evaleasy1bbin.5(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.2(A,B) -> evaleasy1bbin.6(A,B) [A >= 0 && 39 >= A] evaleasy1bb3in.3(A,B) -> evaleasy1returnin.9(A,B) [A >= 0 && A >= 40] evaleasy1bbin.4(A,B) -> evaleasy1bb1in.7(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] evaleasy1bbin.5(A,B) -> evaleasy1bb2in.8(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] evaleasy1bbin.6(A,B) -> evaleasy1bb2in.8(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] evaleasy1bb1in.7(A,B) -> evaleasy1bb3in.2(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb1in.7(A,B) -> evaleasy1bb3in.3(1 + A,B) [-1*B >= 0 && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb2in.8(A,B) -> evaleasy1bb3in.2(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1bb2in.8(A,B) -> evaleasy1bb3in.3(2 + A,B) [39 + -1*A >= 0 && A >= 0] evaleasy1returnin.9(A,B) -> evaleasy1stop.10(A,B) [-40 + A >= 0] evaleasy1stop.10(A,B) -> exitus616.11(A,B) True Signature: {(evaleasy1bb1in.7,2) ;(evaleasy1bb2in.8,2) ;(evaleasy1bb3in.2,2) ;(evaleasy1bb3in.3,2) ;(evaleasy1bbin.4,2) ;(evaleasy1bbin.5,2) ;(evaleasy1bbin.6,2) ;(evaleasy1entryin.1,2) ;(evaleasy1returnin.9,2) ;(evaleasy1start.0,2) ;(evaleasy1stop.10,2) ;(exitus616.11,2)} Rule Graph: [0->{1},1->{2,3,4},2->{6},3->{7},4->{8},5->{13},6->{9,10},7->{11,12},8->{11,12},9->{2,3,4},10->{5},11->{2 ,3,4},12->{5},13->{14},14->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | `- p:[2,9,6,11,7,3,8,4] c: [2,3,4,6,7,8,9,11]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,0.0] evaleasy1start.0 ~> evaleasy1entryin.1 [A <= A, B <= B] evaleasy1entryin.1 ~> evaleasy1bb3in.2 [A <= 0*K, B <= B] evaleasy1bb3in.2 ~> evaleasy1bbin.4 [A <= A, B <= B] evaleasy1bb3in.2 ~> evaleasy1bbin.5 [A <= A, B <= B] evaleasy1bb3in.2 ~> evaleasy1bbin.6 [A <= A, B <= B] evaleasy1bb3in.3 ~> evaleasy1returnin.9 [A <= A, B <= B] evaleasy1bbin.4 ~> evaleasy1bb1in.7 [A <= A, B <= B] evaleasy1bbin.5 ~> evaleasy1bb2in.8 [A <= A, B <= B] evaleasy1bbin.6 ~> evaleasy1bb2in.8 [A <= A, B <= B] evaleasy1bb1in.7 ~> evaleasy1bb3in.2 [A <= 40*K, B <= B] evaleasy1bb1in.7 ~> evaleasy1bb3in.3 [A <= 40*K, B <= B] evaleasy1bb2in.8 ~> evaleasy1bb3in.2 [A <= 41*K, B <= B] evaleasy1bb2in.8 ~> evaleasy1bb3in.3 [A <= 41*K, B <= B] evaleasy1returnin.9 ~> evaleasy1stop.10 [A <= A, B <= B] evaleasy1stop.10 ~> exitus616.11 [A <= A, B <= B] + Loop: [0.0 <= 821*K + 20*A] evaleasy1bb3in.2 ~> evaleasy1bbin.4 [A <= A, B <= B] evaleasy1bb1in.7 ~> evaleasy1bb3in.2 [A <= 40*K, B <= B] evaleasy1bbin.4 ~> evaleasy1bb1in.7 [A <= A, B <= B] evaleasy1bb2in.8 ~> evaleasy1bb3in.2 [A <= 41*K, B <= B] evaleasy1bbin.5 ~> evaleasy1bb2in.8 [A <= A, B <= B] evaleasy1bb3in.2 ~> evaleasy1bbin.5 [A <= A, B <= B] evaleasy1bbin.6 ~> evaleasy1bb2in.8 [A <= A, B <= B] evaleasy1bb3in.2 ~> evaleasy1bbin.6 [A <= A, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0] evaleasy1start.0 ~> evaleasy1entryin.1 [] evaleasy1entryin.1 ~> evaleasy1bb3in.2 [K ~=> A] evaleasy1bb3in.2 ~> evaleasy1bbin.4 [] evaleasy1bb3in.2 ~> evaleasy1bbin.5 [] evaleasy1bb3in.2 ~> evaleasy1bbin.6 [] evaleasy1bb3in.3 ~> evaleasy1returnin.9 [] evaleasy1bbin.4 ~> evaleasy1bb1in.7 [] evaleasy1bbin.5 ~> evaleasy1bb2in.8 [] evaleasy1bbin.6 ~> evaleasy1bb2in.8 [] evaleasy1bb1in.7 ~> evaleasy1bb3in.2 [K ~=> A] evaleasy1bb1in.7 ~> evaleasy1bb3in.3 [K ~=> A] evaleasy1bb2in.8 ~> evaleasy1bb3in.2 [K ~=> A] evaleasy1bb2in.8 ~> evaleasy1bb3in.3 [K ~=> A] evaleasy1returnin.9 ~> evaleasy1stop.10 [] evaleasy1stop.10 ~> exitus616.11 [] + Loop: [A ~*> 0.0,K ~*> 0.0] evaleasy1bb3in.2 ~> evaleasy1bbin.4 [] evaleasy1bb1in.7 ~> evaleasy1bb3in.2 [K ~=> A] evaleasy1bbin.4 ~> evaleasy1bb1in.7 [] evaleasy1bb2in.8 ~> evaleasy1bb3in.2 [K ~=> A] evaleasy1bbin.5 ~> evaleasy1bb2in.8 [] evaleasy1bb3in.2 ~> evaleasy1bbin.5 [] evaleasy1bbin.6 ~> evaleasy1bb2in.8 [] evaleasy1bb3in.2 ~> evaleasy1bbin.6 [] + Applied Processor: Lare + Details: evaleasy1start.0 ~> exitus616.11 [K ~=> A,tick ~+> tick,K ~*> 0.0,K ~*> tick] + evaleasy1bb1in.7> [K ~=> A ,tick ~+> tick ,A ~*> 0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> tick] evaleasy1bb2in.8> [K ~=> A,tick ~+> tick,A ~*> 0.0,A ~*> tick,K ~*> 0.0,K ~*> tick] YES(?,O(1))