YES(?,POLY) * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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,1) 2. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (1,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,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,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,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 3: AddSinks 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,1) 2. evalsipma91entryin(A,B,C,D) -> evalsipma91returnin(A,B,C,D) [A >= 101] (1,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,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,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,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: AddSinks + Details: () * Step 4: 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] 14. evalsipma91returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4) ;(exitus616,4)} Flow Graph: [0->{1,2},1->{3,6},2->{4,14},3->{5},4->{},5->{3,6},6->{7,8},7->{4,14},8->{9,10,11},9->{7,8},10->{12,13} ,11->{12,13},12->{7,8},13->{7,8},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,6),(9,8),(11,13),(12,7)] * Step 5: LooptreeTransformer 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] 14. evalsipma91returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4) ;(exitus616,4)} Flow Graph: [0->{1,2},1->{3},2->{4,14},3->{5},4->{},5->{3,6},6->{7,8},7->{4,14},8->{9,10,11},9->{7},10->{12,13} ,11->{12},12->{8},13->{7,8},14->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[3,5] c: [5] | `- p:[8,12,10,11,13] c: [13] | `- p:[8,12,10,11] c: [12] * Step 6: SizeAbstraction 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] 14. evalsipma91returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalsipma91bb11in,4) ;(evalsipma91bb2in,4) ;(evalsipma91bb3in,4) ;(evalsipma91bb5in,4) ;(evalsipma91bb8in,4) ;(evalsipma91entryin,4) ;(evalsipma91returnin,4) ;(evalsipma91start,4) ;(evalsipma91stop,4) ;(exitus616,4)} Flow Graph: [0->{1,2},1->{3},2->{4,14},3->{5},4->{},5->{3,6},6->{7,8},7->{4,14},8->{9,10,11},9->{7},10->{12,13} ,11->{12},12->{8},13->{7,8},14->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[3,5] c: [5] | `- p:[8,12,10,11,13] c: [13] | `- p:[8,12,10,11] c: [12]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.1,0.1.0] evalsipma91start ~> evalsipma91entryin [A <= A, B <= B, C <= C, D <= D] evalsipma91entryin ~> evalsipma91bb3in [A <= K, B <= A, C <= C, D <= D] evalsipma91entryin ~> evalsipma91returnin [A <= A, B <= B, C <= C, D <= D] evalsipma91bb3in ~> evalsipma91bb2in [A <= A, B <= B, C <= C, D <= D] evalsipma91returnin ~> evalsipma91stop [A <= A, B <= B, C <= C, D <= D] evalsipma91bb2in ~> evalsipma91bb3in [A <= K + A, B <= 10*K + A + B, C <= C, D <= D] evalsipma91bb3in ~> evalsipma91bb11in [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in ~> evalsipma91returnin [A <= A, B <= B, C <= C, D <= D] evalsipma91bb11in ~> evalsipma91bb5in [A <= A, B <= B, C <= C, D <= D] evalsipma91bb5in ~> evalsipma91bb11in [A <= K, B <= B, C <= C, D <= D] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= 100*K, D <= A] evalsipma91bb8in ~> evalsipma91bb11in [A <= A, B <= 111*K, C <= C, D <= D] evalsipma91bb8in ~> evalsipma91bb11in [A <= D, B <= B, C <= C, D <= D] evalsipma91returnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 101*K + B] evalsipma91bb3in ~> evalsipma91bb2in [A <= A, B <= B, C <= C, D <= D] evalsipma91bb2in ~> evalsipma91bb3in [A <= K + A, B <= 10*K + A + B, C <= C, D <= D] + Loop: [0.1 <= K + A + D] evalsipma91bb11in ~> evalsipma91bb5in [A <= A, B <= B, C <= C, D <= D] evalsipma91bb8in ~> evalsipma91bb11in [A <= A, B <= 111*K, C <= C, D <= D] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= 100*K, D <= A] evalsipma91bb8in ~> evalsipma91bb11in [A <= D, B <= B, C <= C, D <= D] + Loop: [0.1.0 <= 111*K + B + C] evalsipma91bb11in ~> evalsipma91bb5in [A <= A, B <= B, C <= C, D <= D] evalsipma91bb8in ~> evalsipma91bb11in [A <= A, B <= 111*K, C <= C, D <= D] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= B, D <= A] evalsipma91bb5in ~> evalsipma91bb8in [A <= A, B <= B, C <= 100*K, D <= A] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.1,0.1.0] evalsipma91start ~> evalsipma91entryin [] evalsipma91entryin ~> evalsipma91bb3in [A ~=> B,K ~=> A] evalsipma91entryin ~> evalsipma91returnin [] evalsipma91bb3in ~> evalsipma91bb2in [] evalsipma91returnin ~> evalsipma91stop [] evalsipma91bb2in ~> evalsipma91bb3in [A ~+> A,A ~+> B,B ~+> B,K ~+> A,K ~*> B] evalsipma91bb3in ~> evalsipma91bb11in [] evalsipma91bb11in ~> evalsipma91returnin [] evalsipma91bb11in ~> evalsipma91bb5in [] evalsipma91bb5in ~> evalsipma91bb11in [K ~=> A] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,B ~=> C] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,K ~=> C] evalsipma91bb8in ~> evalsipma91bb11in [K ~=> B] evalsipma91bb8in ~> evalsipma91bb11in [D ~=> A] evalsipma91returnin ~> exitus616 [] + Loop: [B ~+> 0.0,K ~*> 0.0] evalsipma91bb3in ~> evalsipma91bb2in [] evalsipma91bb2in ~> evalsipma91bb3in [A ~+> A,A ~+> B,B ~+> B,K ~+> A,K ~*> B] + Loop: [A ~+> 0.1,D ~+> 0.1,K ~+> 0.1] evalsipma91bb11in ~> evalsipma91bb5in [] evalsipma91bb8in ~> evalsipma91bb11in [K ~=> B] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,B ~=> C] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,K ~=> C] evalsipma91bb8in ~> evalsipma91bb11in [D ~=> A] + Loop: [B ~+> 0.1.0,C ~+> 0.1.0,K ~*> 0.1.0] evalsipma91bb11in ~> evalsipma91bb5in [] evalsipma91bb8in ~> evalsipma91bb11in [K ~=> B] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,B ~=> C] evalsipma91bb5in ~> evalsipma91bb8in [A ~=> D,K ~=> C] + Applied Processor: LareProcessor + Details: evalsipma91start ~> evalsipma91stop [A ~=> B ,A ~=> C ,D ~=> A ,K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,A ~+> B ,A ~+> C ,A ~+> 0.0 ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> tick ,C ~*> tick ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick] evalsipma91start ~> exitus616 [A ~=> B ,A ~=> C ,D ~=> A ,K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,A ~+> B ,A ~+> C ,A ~+> 0.0 ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.1 ,A ~*> 0.1.0 ,A ~*> tick ,C ~*> tick ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick] + evalsipma91bb3in> [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] + evalsipma91bb5in> [A ~=> D ,B ~=> C ,D ~=> A ,K ~=> B ,K ~=> C ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1.0 ,B ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.1.0 ,B ~*> tick ,C ~*> tick ,D ~*> tick ,K ~*> 0.1.0 ,K ~*> tick] evalsipma91bb11in> [A ~=> D ,B ~=> C ,D ~=> A ,K ~=> B ,K ~=> C ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1.0 ,B ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.1.0 ,B ~*> tick ,C ~*> tick ,D ~*> tick ,K ~*> 0.1.0 ,K ~*> tick] + evalsipma91bb8in> [A ~=> D ,B ~=> C ,K ~=> B ,K ~=> C ,B ~+> 0.1.0 ,B ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,K ~*> 0.1.0 ,K ~*> tick] evalsipma91bb5in> [A ~=> D ,B ~=> C ,K ~=> B ,K ~=> C ,B ~+> 0.1.0 ,B ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,K ~*> 0.1.0 ,K ~*> tick] evalsipma91bb11in> [A ~=> D ,B ~=> C ,K ~=> B ,K ~=> C ,B ~+> 0.1.0 ,B ~+> tick ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,K ~*> 0.1.0 ,K ~*> tick] YES(?,POLY)