YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True (?,1) 2. evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] (?,1) 3. evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True (?,1) 5. evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] (?,1) 6. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] (?,1) 7. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] (?,1) 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True (?,1) 10. evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True (?,1) 11. evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True (?,1) 12. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1) Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True (1,1) 2. evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] (?,1) 3. evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] (1,1) 4. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True (?,1) 5. evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] (?,1) 6. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] (?,1) 7. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] (?,1) 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True (?,1) 10. evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True (?,1) 11. evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True (?,1) 12. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (1,1) Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{12},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{}] + Applied Processor: AddSinks + Details: () * Step 3: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True (?,1) 2. evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] (?,1) 3. evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True (?,1) 5. evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] (?,1) 6. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] (?,1) 7. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] (?,1) 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True (?,1) 10. evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True (?,1) 11. evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True (?,1) 12. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1) 13. evalfreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{12,13},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{},13->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,11,5,4,10,7,6,8,9] c: [2] | `- p:[6,10,7,8] c: [6] * Step 4: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb5in(B,B,C,D) True (?,1) 2. evalfbb5in(A,B,C,D) -> evalfbbin(A,B,C,D) [B >= 2] (?,1) 3. evalfbb5in(A,B,C,D) -> evalfreturnin(A,B,C,D) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D) -> evalfbb2in(A,B,-1 + B,-1 + A + B) True (?,1) 5. evalfbb2in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C >= 1 + D] (?,1) 6. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,D) [D >= C] (?,1) 7. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [0 >= 1 + E] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb1in(A,B,C,D) [E >= 1] (?,1) 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) True (?,1) 10. evalfbb1in(A,B,C,D) -> evalfbb2in(A,B,C,-1 + D) True (?,1) 11. evalfbb4in(A,B,C,D) -> evalfbb5in(1 + -1*C + D,-1 + C,C,D) True (?,1) 12. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,1) 13. evalfreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalfbb1in,4) ;(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbbin,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{12,13},4->{5,6},5->{11},6->{7,8,9},7->{10},8->{10},9->{11},10->{5,6},11->{2,3} ,12->{},13->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[2,11,5,4,10,7,6,8,9] c: [2] | `- p:[6,10,7,8] c: [6]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalfstart ~> evalfentryin [A <= A, B <= B, C <= C, D <= D] evalfentryin ~> evalfbb5in [A <= B, B <= B, C <= C, D <= D] evalfbb5in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D] evalfbb5in ~> evalfreturnin [A <= A, B <= B, C <= C, D <= D] evalfbbin ~> evalfbb2in [A <= A, B <= B, C <= K + B, D <= K + A + B] evalfbb2in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb4in ~> evalfbb5in [A <= K + C + D, B <= K + C, C <= C, D <= D] evalfreturnin ~> evalfstop [A <= A, B <= B, C <= C, D <= D] evalfreturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 2*K + B + C] evalfbb5in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D] evalfbb4in ~> evalfbb5in [A <= K + C + D, B <= K + C, C <= C, D <= D] evalfbb2in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] evalfbbin ~> evalfbb2in [A <= A, B <= B, C <= K + B, D <= K + A + B] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb4in [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= 2*K + C + D] evalfbb2in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D] evalfbb1in ~> evalfbb2in [A <= A, B <= B, C <= C, D <= K + D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] evalfbb3in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalfstart ~> evalfentryin [] evalfentryin ~> evalfbb5in [B ~=> A] evalfbb5in ~> evalfbbin [] evalfbb5in ~> evalfreturnin [] evalfbbin ~> evalfbb2in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb2in ~> evalfbb4in [] evalfbb2in ~> evalfbb3in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb4in [] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb4in ~> evalfbb5in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfreturnin ~> evalfstop [] evalfreturnin ~> exitus616 [] + Loop: [B ~+> 0.0,C ~+> 0.0,K ~*> 0.0] evalfbb5in ~> evalfbbin [] evalfbb4in ~> evalfbb5in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfbb2in ~> evalfbb4in [] evalfbbin ~> evalfbb2in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb3in ~> evalfbb1in [] evalfbb2in ~> evalfbb3in [] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb4in [] + Loop: [C ~+> 0.0.0,D ~+> 0.0.0,K ~*> 0.0.0] evalfbb2in ~> evalfbb3in [] evalfbb1in ~> evalfbb2in [D ~+> D,K ~+> D] evalfbb3in ~> evalfbb1in [] evalfbb3in ~> evalfbb1in [] + Applied Processor: LareProcessor + Details: evalfstart ~> exitus616 [B ~=> A ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> 0.0.0 ,C ~^> tick ,K ~^> A ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] evalfstart ~> evalfstop [B ~=> A ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> 0.0.0 ,C ~^> tick ,K ~^> A ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb5in> [A ~+> A ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> 0.0.0 ,C ~^> tick ,K ~^> A ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb3in> [C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,C ~*> D ,D ~*> D ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] evalfbb2in> [C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,C ~*> D ,D ~*> D ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)