YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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 MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (1,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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 MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (1,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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 MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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 MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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: [7] | `- p:[3,5,6] c: [6] | `- p:[3,5] c: [5] * Step 6: SizeAbstraction MAYBE + 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) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,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: [7] | `- p:[3,5,6] c: [6] | `- p:[3,5] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,0.0,0.0.0,0.0.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 <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + 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 <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] + Loop: [0.0.0 <= K + A + B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] + Loop: [0.0.0.0 <= K + A + B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.0.0,0.0.0.0] evalrandom1dstart ~> evalrandom1dentryin [] evalrandom1dentryin ~> evalrandom1dbb5in [K ~=> B] evalrandom1dentryin ~> evalrandom1dreturnin [] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb5in ~> evalrandom1dreturnin [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dreturnin ~> evalrandom1dstop [] evalrandom1dreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] + Loop: [A ~+> 0.0.0.0,B ~+> 0.0.0.0,K ~+> 0.0.0.0] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] + Applied Processor: LareProcessor + Details: evalrandom1dstart ~> exitus616 [K ~=> B ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> tick ,K ~^> B ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> tick] evalrandom1dstart ~> evalrandom1dstop [K ~=> B ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> tick ,K ~^> B ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> tick] + evalrandom1dbb5in> [A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> 0.0.0 ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> 0.0.0 ,A ~^> 0.0.0.0 ,A ~^> tick ,B ~^> B ,B ~^> 0.0.0 ,B ~^> 0.0.0.0 ,B ~^> tick ,K ~^> B ,K ~^> 0.0.0 ,K ~^> 0.0.0.0 ,K ~^> tick] + evalrandom1dbb5in> [A ~+> B ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> 0.0.0.0 ,A ~*> tick ,B ~*> B ,B ~*> 0.0.0.0 ,B ~*> tick ,K ~*> B ,K ~*> 0.0.0.0 ,K ~*> tick ,A ~^> B ,B ~^> B ,K ~^> B] + evalrandom1dbb5in> [A ~+> B ,A ~+> 0.0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,PRIMREC)