YES * Step 1: TrivialSCCs YES + 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 YES + 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: Looptree YES + 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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | +- p:[3,5] c: [5] | `- p:[8,12,10,11,13] c: [13] | `- p:[8,12,10,11] c: [12] YES