YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1) 1. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1) 2. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1) 3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [-1 + A >= 0 && 100 >= B] (?,1) 4. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) [-1 + A >= 0] (?,1) 5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] (?,1) 6. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [-1 + A >= 0 && B >= 101] (?,1) 7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] (?,1) 8. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] (?,1) 9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] (?,1) 10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] (?,1) 11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] (?,1) 12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] 13. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4)} Flow Graph: [0->{1,2},1->{3,6},2->{4},3->{5},4->{},5->{3,6},6->{7,8},7->{4},8->{9,10,11},9->{7,8},10->{12,13},11->{12 ,13},12->{7,8},13->{7,8}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,6),(9,8),(11,13),(12,7)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True (1,1) 1. evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] (?,1) 2. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (?,1) 3. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [-1 + A >= 0 && 100 >= B] (?,1) 4. evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) [-1 + A >= 0] (?,1) 5. evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] (?,1) 6. evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [-1 + A >= 0 && B >= 101] (?,1) 7. evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] (?,1) 8. evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] (?,1) 9. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] (?,1) 10. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] (?,1) 11. evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] (?,1) 12. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] 13. evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [-1 + A + -1*D >= 0 (?,1) && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{5},4->{},5->{3,6},6->{7,8},7->{4},8->{9,10,11},9->{7},10->{12,13},11->{12} ,12->{8},13->{7,8}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [-1 + A >= 0 && 100 >= B] evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) [-1 + A >= 0] evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5},4->{},5->{3,6},6->{7,8},7->{4},8->{9,10,11},9->{7},10->{12,13},11->{12} ,12->{8},13->{7,8}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalsipma91start(A,B,C,D) -> evalsipma91entryin(A,B,C,D) True evalsipma91entryin(A,B,C,D) -> evalsipma91bb3in(1,A,C,D) [100 >= A] evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] evalsipma91bb3in(A,B,C,D) -> evalsipma91bb2in(A,B,C,D) [-1 + A >= 0 && 100 >= B] evalsipma91returnin(A,B,C,D) -> evalsipma91stop(A,B,C,D) [-1 + A >= 0] evalsipma91bb2in(A,B,C,D) -> evalsipma91bb3in(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb3in(A,B,C,D) -> evalsipma91bb11in(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb11in(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] evalsipma91bb11in(A,B,C,D) -> evalsipma91bb5in(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb11in(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in(A,B,C,D) -> evalsipma91bb8in(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] evalsipma91bb8in(A,B,C,D) -> evalsipma91bb11in(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] evalsipma91stop(A,B,C,D) -> exitus616(A,B,C,D) True evalsipma91stop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4) ;(exitus616,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5},4->{14,15},5->{3,6},6->{7,8},7->{4},8->{9,10,11},9->{7},10->{12,13} ,11->{12},12->{8},13->{7,8}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalsipma91start.0(A,B,C,D) -> evalsipma91entryin.1(A,B,C,D) True evalsipma91start.0(A,B,C,D) -> evalsipma91entryin.2(A,B,C,D) True evalsipma91entryin.1(A,B,C,D) -> evalsipma91bb3in.3(1,A,C,D) [100 >= A] evalsipma91entryin.2(A,B,C,D) -> evalsipma91returnin.4(A,B,C,D) [A >= 101] evalsipma91bb3in.3(A,B,C,D) -> evalsipma91bb2in.5(A,B,C,D) [-1 + A >= 0 && 100 >= B] evalsipma91returnin.4(A,B,C,D) -> evalsipma91stop.14(A,B,C,D) [-1 + A >= 0] evalsipma91returnin.4(A,B,C,D) -> evalsipma91stop.15(A,B,C,D) [-1 + A >= 0] evalsipma91bb2in.5(A,B,C,D) -> evalsipma91bb3in.3(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb2in.5(A,B,C,D) -> evalsipma91bb3in.6(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb3in.6(A,B,C,D) -> evalsipma91bb11in.7(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb3in.6(A,B,C,D) -> evalsipma91bb11in.8(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb11in.7(A,B,C,D) -> evalsipma91returnin.4(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.9(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.10(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.11(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb5in.9(A,B,C,D) -> evalsipma91bb11in.7(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] evalsipma91bb5in.10(A,B,C,D) -> evalsipma91bb8in.12(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in.10(A,B,C,D) -> evalsipma91bb8in.13(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in.11(A,B,C,D) -> evalsipma91bb8in.12(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] evalsipma91bb8in.12(A,B,C,D) -> evalsipma91bb11in.8(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] evalsipma91bb8in.13(A,B,C,D) -> evalsipma91bb11in.7(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] evalsipma91bb8in.13(A,B,C,D) -> evalsipma91bb11in.8(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] evalsipma91stop.14(A,B,C,D) -> exitus616.16(A,B,C,D) True evalsipma91stop.15(A,B,C,D) -> exitus616.16(A,B,C,D) True Signature: {(evalsipma91bb11in.7,4) ;(evalsipma91bb11in.8,4) ;(evalsipma91bb2in.5,4) ;(evalsipma91bb3in.3,4) ;(evalsipma91bb3in.6,4) ;(evalsipma91bb5in.10,4) ;(evalsipma91bb5in.11,4) ;(evalsipma91bb5in.9,4) ;(evalsipma91bb8in.12,4) ;(evalsipma91bb8in.13,4) ;(evalsipma91entryin.1,4) ;(evalsipma91entryin.2,4) ;(evalsipma91returnin.4,4) ;(evalsipma91start.0,4) ;(evalsipma91stop.14,4) ;(evalsipma91stop.15,4) ;(exitus616.16,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5,6},4->{7,8},5->{22},6->{23},7->{4},8->{9,10},9->{11},10->{12,13,14},11->{5,6} ,12->{15},13->{16,17},14->{18},15->{11},16->{19},17->{20,21},18->{19},19->{12,13,14},20->{11},21->{12,13,14} ,22->{},23->{}] + 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,19,20,21,22,23] | +- p:[4,7] c: [4,7] | `- p:[13,19,16,18,14,21,17] c: [13,14,16,17,18,19,21] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalsipma91start.0(A,B,C,D) -> evalsipma91entryin.1(A,B,C,D) True evalsipma91start.0(A,B,C,D) -> evalsipma91entryin.2(A,B,C,D) True evalsipma91entryin.1(A,B,C,D) -> evalsipma91bb3in.3(1,A,C,D) [100 >= A] evalsipma91entryin.2(A,B,C,D) -> evalsipma91returnin.4(A,B,C,D) [A >= 101] evalsipma91bb3in.3(A,B,C,D) -> evalsipma91bb2in.5(A,B,C,D) [-1 + A >= 0 && 100 >= B] evalsipma91returnin.4(A,B,C,D) -> evalsipma91stop.14(A,B,C,D) [-1 + A >= 0] evalsipma91returnin.4(A,B,C,D) -> evalsipma91stop.15(A,B,C,D) [-1 + A >= 0] evalsipma91bb2in.5(A,B,C,D) -> evalsipma91bb3in.3(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb2in.5(A,B,C,D) -> evalsipma91bb3in.6(1 + A,11 + B,C,D) [100 + -1*B >= 0 && 99 + A + -1*B >= 0 && -1 + A >= 0] evalsipma91bb3in.6(A,B,C,D) -> evalsipma91bb11in.7(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb3in.6(A,B,C,D) -> evalsipma91bb11in.8(A,B,C,D) [-1 + A >= 0 && B >= 101] evalsipma91bb11in.7(A,B,C,D) -> evalsipma91returnin.4(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && 1 >= A] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.9(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.10(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb11in.8(A,B,C,D) -> evalsipma91bb5in.11(A,B,C,D) [-101 + B >= 0 && -102 + A + B >= 0 && -1 + A >= 0 && A >= 2] evalsipma91bb5in.9(A,B,C,D) -> evalsipma91bb11in.7(-1 + A,-10 + B,C,D) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && B >= 111 && A = 2] evalsipma91bb5in.10(A,B,C,D) -> evalsipma91bb8in.12(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in.10(A,B,C,D) -> evalsipma91bb8in.13(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && A >= 3] evalsipma91bb5in.11(A,B,C,D) -> evalsipma91bb8in.12(A,B,-10 + B,-1 + A) [-101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 110 >= B] evalsipma91bb8in.12(A,B,C,D) -> evalsipma91bb11in.8(1 + D,11 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && 100 >= C] evalsipma91bb8in.13(A,B,C,D) -> evalsipma91bb11in.7(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] evalsipma91bb8in.13(A,B,C,D) -> evalsipma91bb11in.8(D,1 + C,C,D) [-1 + A + -1*D >= 0 && -1 + D >= 0 && -92 + C + D >= 0 && -102 + B + D >= 0 && -3 + A + D >= 0 && 1 + -1*A + D >= 0 && -10 + B + -1*C >= 0 && -91 + C >= 0 && -192 + B + C >= 0 && 10 + -1*B + C >= 0 && -93 + A + C >= 0 && -101 + B >= 0 && -103 + A + B >= 0 && -2 + A >= 0 && C >= 101] evalsipma91stop.14(A,B,C,D) -> exitus616.16(A,B,C,D) True evalsipma91stop.15(A,B,C,D) -> exitus616.16(A,B,C,D) True Signature: {(evalsipma91bb11in.7,4) ;(evalsipma91bb11in.8,4) ;(evalsipma91bb2in.5,4) ;(evalsipma91bb3in.3,4) ;(evalsipma91bb3in.6,4) ;(evalsipma91bb5in.10,4) ;(evalsipma91bb5in.11,4) ;(evalsipma91bb5in.9,4) ;(evalsipma91bb8in.12,4) ;(evalsipma91bb8in.13,4) ;(evalsipma91entryin.1,4) ;(evalsipma91entryin.2,4) ;(evalsipma91returnin.4,4) ;(evalsipma91start.0,4) ;(evalsipma91stop.14,4) ;(evalsipma91stop.15,4) ;(exitus616.16,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5,6},4->{7,8},5->{22},6->{23},7->{4},8->{9,10},9->{11},10->{12,13,14},11->{5,6} ,12->{15},13->{16,17},14->{18},15->{11},16->{19},17->{20,21},18->{19},19->{12,13,14},20->{11},21->{12,13,14} ,22->{},23->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | +- p:[4,7] c: [4,7] | `- p:[13,19,16,18,14,21,17] c: [13,14,16,17,18,19,21]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.1] evalsipma91start.0 ~> evalsipma91entryin.1 [A <= A, B <= B, C <= C, D <= D] evalsipma91start.0 ~> evalsipma91entryin.2 [A <= A, B <= B, C <= C, D <= D] evalsipma91entryin.1 ~> evalsipma91bb3in.3 [A <= K, B <= A, C <= C, D <= D] evalsipma91entryin.2 ~> evalsipma91returnin.4 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb3in.3 ~> evalsipma91bb2in.5 [A <= A, B <= B, C <= C, D <= D] evalsipma91returnin.4 ~> evalsipma91stop.14 [A <= A, B <= B, C <= C, D <= D] evalsipma91returnin.4 ~> evalsipma91stop.15 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb2in.5 ~> evalsipma91bb3in.3 [A <= K + A, B <= 10*K + A + B, C <= C, D <= D] evalsipma91bb2in.5 ~> evalsipma91bb3in.6 [A <= K + A, B <= 10*K + A + B, C <= C, D <= D] evalsipma91bb3in.6 ~> evalsipma91bb11in.7 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb3in.6 ~> evalsipma91bb11in.8 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in.7 ~> evalsipma91returnin.4 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in.8 ~> evalsipma91bb5in.9 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in.8 ~> evalsipma91bb5in.10 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in.8 ~> evalsipma91bb5in.11 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb5in.9 ~> evalsipma91bb11in.7 [A <= K, B <= B, C <= C, D <= D] evalsipma91bb5in.10 ~> evalsipma91bb8in.12 [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in.10 ~> evalsipma91bb8in.13 [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in.11 ~> evalsipma91bb8in.12 [A <= A, B <= B, C <= 100*K, D <= A] evalsipma91bb8in.12 ~> evalsipma91bb11in.8 [A <= A, B <= 111*K, C <= C, D <= D] evalsipma91bb8in.13 ~> evalsipma91bb11in.7 [A <= D, B <= B, C <= C, D <= D] evalsipma91bb8in.13 ~> evalsipma91bb11in.8 [A <= D, B <= B, C <= C, D <= D] evalsipma91stop.14 ~> exitus616.16 [A <= A, B <= B, C <= C, D <= D] evalsipma91stop.15 ~> exitus616.16 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 100*K + B] evalsipma91bb3in.3 ~> evalsipma91bb2in.5 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb2in.5 ~> evalsipma91bb3in.3 [A <= K + A, B <= 10*K + A + B, C <= C, D <= D] + Loop: [0.1 <= 92*K + 9*A + B] evalsipma91bb11in.8 ~> evalsipma91bb5in.10 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb8in.12 ~> evalsipma91bb11in.8 [A <= A, B <= 111*K, C <= C, D <= D] evalsipma91bb5in.10 ~> evalsipma91bb8in.12 [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in.11 ~> evalsipma91bb8in.12 [A <= A, B <= B, C <= 100*K, D <= A] evalsipma91bb11in.8 ~> evalsipma91bb5in.11 [A <= A, B <= B, C <= C, D <= D] evalsipma91bb8in.13 ~> evalsipma91bb11in.8 [A <= D, B <= B, C <= C, D <= D] evalsipma91bb5in.10 ~> evalsipma91bb8in.13 [A <= A, B <= B, C <= B, D <= A] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.1] evalsipma91start.0 ~> evalsipma91entryin.1 [] evalsipma91start.0 ~> evalsipma91entryin.2 [] evalsipma91entryin.1 ~> evalsipma91bb3in.3 [A ~=> B,K ~=> A] evalsipma91entryin.2 ~> evalsipma91returnin.4 [] evalsipma91bb3in.3 ~> evalsipma91bb2in.5 [] evalsipma91returnin.4 ~> evalsipma91stop.14 [] evalsipma91returnin.4 ~> evalsipma91stop.15 [] evalsipma91bb2in.5 ~> evalsipma91bb3in.3 [A ~+> A,A ~+> B,B ~+> B,K ~+> A,K ~*> B] evalsipma91bb2in.5 ~> evalsipma91bb3in.6 [A ~+> A,A ~+> B,B ~+> B,K ~+> A,K ~*> B] evalsipma91bb3in.6 ~> evalsipma91bb11in.7 [] evalsipma91bb3in.6 ~> evalsipma91bb11in.8 [] evalsipma91bb11in.7 ~> evalsipma91returnin.4 [] evalsipma91bb11in.8 ~> evalsipma91bb5in.9 [] evalsipma91bb11in.8 ~> evalsipma91bb5in.10 [] evalsipma91bb11in.8 ~> evalsipma91bb5in.11 [] evalsipma91bb5in.9 ~> evalsipma91bb11in.7 [K ~=> A] evalsipma91bb5in.10 ~> evalsipma91bb8in.12 [A ~=> D,B ~=> C] evalsipma91bb5in.10 ~> evalsipma91bb8in.13 [A ~=> D,B ~=> C] evalsipma91bb5in.11 ~> evalsipma91bb8in.12 [A ~=> D,K ~=> C] evalsipma91bb8in.12 ~> evalsipma91bb11in.8 [K ~=> B] evalsipma91bb8in.13 ~> evalsipma91bb11in.7 [D ~=> A] evalsipma91bb8in.13 ~> evalsipma91bb11in.8 [D ~=> A] evalsipma91stop.14 ~> exitus616.16 [] evalsipma91stop.15 ~> exitus616.16 [] + Loop: [B ~+> 0.0,K ~*> 0.0] evalsipma91bb3in.3 ~> evalsipma91bb2in.5 [] evalsipma91bb2in.5 ~> evalsipma91bb3in.3 [A ~+> A,A ~+> B,B ~+> B,K ~+> A,K ~*> B] + Loop: [B ~+> 0.1,A ~*> 0.1,K ~*> 0.1] evalsipma91bb11in.8 ~> evalsipma91bb5in.10 [] evalsipma91bb8in.12 ~> evalsipma91bb11in.8 [K ~=> B] evalsipma91bb5in.10 ~> evalsipma91bb8in.12 [A ~=> D,B ~=> C] evalsipma91bb5in.11 ~> evalsipma91bb8in.12 [A ~=> D,K ~=> C] evalsipma91bb11in.8 ~> evalsipma91bb5in.11 [] evalsipma91bb8in.13 ~> evalsipma91bb11in.8 [D ~=> A] evalsipma91bb5in.10 ~> evalsipma91bb8in.13 [A ~=> D,B ~=> C] + Applied Processor: Lare + Details: evalsipma91start.0 ~> exitus616.16 [D ~=> A ,K ~=> A ,K ~=> B ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.1 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] + evalsipma91bb2in.5> [A ~+> A ,A ~+> B ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,A ~*> B ,B ~*> A ,B ~*> B ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> tick] + evalsipma91bb11in.8> [A ~=> D ,B ~=> C ,K ~=> B ,K ~=> C ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,A ~*> 0.1 ,A ~*> tick ,K ~*> 0.1 ,K ~*> tick] evalsipma91bb8in.13> [A ~=> D ,B ~=> C ,K ~=> B ,K ~=> C ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,A ~*> 0.1 ,A ~*> tick ,K ~*> 0.1 ,K ~*> tick] YES(?,POLY)