YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Flow Graph: [0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (1,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (1,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (1,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (1,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Flow Graph: [0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4)] * Step 3: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (1,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (1,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (1,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (1,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Flow Graph: [0->{1,2},1->{3},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) 9. evalrandom1dreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3,4},2->{8,9},3->{5,6,7},4->{8,9},5->{3,4},6->{3,4},7->{3,4},8->{},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4)] * Step 5: LooptreeTransformer WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) 9. evalrandom1dreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3},2->{8,9},3->{5,6,7},4->{8,9},5->{3,4},6->{3,4},7->{3,4},8->{},9->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[3,5,6,7] c: [3] * Step 6: SizeAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) True (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) 9. evalrandom1dreturnin(A,B) -> exitus616(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2) ;(exitus616,2)} Flow Graph: [0->{1,2},1->{3},2->{8,9},3->{5,6,7},4->{8,9},5->{3,4},6->{3,4},7->{3,4},8->{},9->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[3,5,6,7] c: [3]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0] evalrandom1dstart ~> evalrandom1dentryin [A <= A, B <= B] evalrandom1dentryin ~> evalrandom1dbb5in [A <= A, B <= K] evalrandom1dentryin ~> evalrandom1dreturnin [A <= A, B <= B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb5in ~> evalrandom1dreturnin [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] evalrandom1dreturnin ~> evalrandom1dstop [A <= A, B <= B] evalrandom1dreturnin ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= K + A + B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= K + B] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0] evalrandom1dstart ~> evalrandom1dentryin [] evalrandom1dentryin ~> evalrandom1dbb5in [K ~=> B] evalrandom1dentryin ~> evalrandom1dreturnin [] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb5in ~> evalrandom1dreturnin [] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] evalrandom1dreturnin ~> evalrandom1dstop [] evalrandom1dreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [B ~+> B,K ~+> B] + Applied Processor: LareProcessor + Details: evalrandom1dstart ~> exitus616 [K ~=> B ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,K ~*> B ,K ~*> 0.0 ,K ~*> tick] evalrandom1dstart ~> evalrandom1dstop [K ~=> B ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,K ~*> B ,K ~*> 0.0 ,K ~*> tick] + evalrandom1dbb5in> [A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,O(n^1))