YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3},2->{4,10},3->{},4->{5,6},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3},11->{5,6}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (1,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (1,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (1,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (1,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3},2->{4,10},3->{},4->{5,6},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3},11->{5,6}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10),(4,6)] * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (1,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (1,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (1,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (1,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3},11->{5,6}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 12. evalrealheapsortstep1returnin(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3) ;(exitus616,3)} Flow Graph: [0->{1,2},1->{3,12},2->{4,10},3->{},4->{5,6},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3,12},11->{5,6} ,12->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10),(4,6)] * Step 5: LooptreeTransformer WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 12. evalrealheapsortstep1returnin(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3) ;(exitus616,3)} Flow Graph: [0->{1,2},1->{3,12},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3,12},11->{5,6} ,12->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[4,9,6,11,8,5,7] c: [9] | `- p:[5,11,8] c: [11] * Step 6: SizeAbstraction WORST_CASE(?,POLY) + Considered Problem: (Rules: 0. evalrealheapsortstep1start(A,B,C) -> evalrealheapsortstep1entryin(A,B,C) True (1,1) 1. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [2 >= A] (?,1) 2. evalrealheapsortstep1entryin(A,B,C) -> evalrealheapsortstep1bb6in(A,1,C) [A >= 3] (?,1) 3. evalrealheapsortstep1returnin(A,B,C) -> evalrealheapsortstep1stop(A,B,C) True (?,1) 4. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,B) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb4in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortstep1bb3in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb5in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 8. evalrealheapsortstep1bb4in(A,B,C) -> evalrealheapsortstep1bb2in(A,B,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && D >= 0 && 1 + C >= 2*D && 2*D >= C] 9. evalrealheapsortstep1bb5in(A,B,C) -> evalrealheapsortstep1bb6in(A,1 + B,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortstep1bb6in(A,B,C) -> evalrealheapsortstep1returnin(A,B,C) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortstep1bb2in(A,B,C) -> evalrealheapsortstep1bb3in(A,B,-1 + D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C && F >= 0 && 1 + C >= 2*F && 2*F >= C && D >= 0 && 1 + C >= 2*D && 2*D >= C] 12. evalrealheapsortstep1returnin(A,B,C) -> exitus616(A,B,C) True (?,1) Signature: {(evalrealheapsortstep1bb2in,3) ;(evalrealheapsortstep1bb3in,3) ;(evalrealheapsortstep1bb4in,3) ;(evalrealheapsortstep1bb5in,3) ;(evalrealheapsortstep1bb6in,3) ;(evalrealheapsortstep1entryin,3) ;(evalrealheapsortstep1returnin,3) ;(evalrealheapsortstep1start,3) ;(evalrealheapsortstep1stop,3) ;(exitus616,3)} Flow Graph: [0->{1,2},1->{3,12},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{3,12},11->{5,6} ,12->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | `- p:[4,9,6,11,8,5,7] c: [9] | `- p:[5,11,8] c: [11]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,0.0,0.0.0] evalrealheapsortstep1start ~> evalrealheapsortstep1entryin [A <= A, B <= B, C <= C] evalrealheapsortstep1entryin ~> evalrealheapsortstep1returnin [A <= A, B <= B, C <= C] evalrealheapsortstep1entryin ~> evalrealheapsortstep1bb6in [A <= A, B <= K, C <= C] evalrealheapsortstep1returnin ~> evalrealheapsortstep1stop [A <= A, B <= B, C <= C] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1bb3in [A <= A, B <= B, C <= B] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb5in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb5in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb5in ~> evalrealheapsortstep1bb6in [A <= A, B <= A, C <= C] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1returnin [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A <= A, B <= B, C <= A] evalrealheapsortstep1returnin ~> exitus616 [A <= A, B <= B, C <= C] + Loop: [0.0 <= K + A + B] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1bb3in [A <= A, B <= B, C <= B] evalrealheapsortstep1bb5in ~> evalrealheapsortstep1bb6in [A <= A, B <= A, C <= C] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb5in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A <= A, B <= B, C <= A] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb5in [A <= A, B <= B, C <= C] + Loop: [0.0.0 <= K + 2*C] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [A <= A, B <= B, C <= C] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A <= A, B <= B, C <= A] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [A <= A, B <= B, C <= C] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,0.0,0.0.0] evalrealheapsortstep1start ~> evalrealheapsortstep1entryin [] evalrealheapsortstep1entryin ~> evalrealheapsortstep1returnin [] evalrealheapsortstep1entryin ~> evalrealheapsortstep1bb6in [K ~=> B] evalrealheapsortstep1returnin ~> evalrealheapsortstep1stop [] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1bb3in [B ~=> C] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb5in [] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb5in [] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [] evalrealheapsortstep1bb5in ~> evalrealheapsortstep1bb6in [A ~=> B] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1returnin [] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A ~=> C] evalrealheapsortstep1returnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrealheapsortstep1bb6in ~> evalrealheapsortstep1bb3in [B ~=> C] evalrealheapsortstep1bb5in ~> evalrealheapsortstep1bb6in [A ~=> B] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb5in [] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A ~=> C] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb5in [] + Loop: [K ~+> 0.0.0,C ~*> 0.0.0] evalrealheapsortstep1bb3in ~> evalrealheapsortstep1bb4in [] evalrealheapsortstep1bb2in ~> evalrealheapsortstep1bb3in [A ~=> C] evalrealheapsortstep1bb4in ~> evalrealheapsortstep1bb2in [] + Applied Processor: LareProcessor + Details: evalrealheapsortstep1start ~> exitus616 [A ~=> B ,A ~=> C ,K ~=> B ,K ~=> C ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] evalrealheapsortstep1start ~> evalrealheapsortstep1stop [A ~=> B ,A ~=> C ,K ~=> B ,K ~=> C ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalrealheapsortstep1bb6in> [A ~=> B ,A ~=> C ,B ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> tick] + evalrealheapsortstep1bb4in> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] evalrealheapsortstep1bb3in> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] YES(?,POLY)