YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalEx1start(A,B,C,D) -> evalEx1entryin(A,B,C,D) True (1,1) 1. evalEx1entryin(A,B,C,D) -> evalEx1bb6in(0,A,C,D) True (?,1) 2. evalEx1bb6in(A,B,C,D) -> evalEx1bbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalEx1bb6in(A,B,C,D) -> evalEx1returnin(A,B,C,D) [A >= B] (?,1) 4. evalEx1bbin(A,B,C,D) -> evalEx1bb4in(A,B,1 + A,B) True (?,1) 5. evalEx1bb4in(A,B,C,D) -> evalEx1bb1in(A,B,C,D) [D >= 1 + C] (?,1) 6. evalEx1bb4in(A,B,C,D) -> evalEx1bb5in(A,B,C,D) [C >= D] (?,1) 7. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1) 8. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E && E >= 1] (?,1) 9. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1] (?,1) 10. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,D) [0 >= 1] (?,1) 11. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,D) [0 >= 1] (?,1) 12. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1] (?,1) 13. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1] (?,1) 14. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,D) True (?,1) 15. evalEx1bb5in(A,B,C,D) -> evalEx1bb6in(1 + A,D,C,D) True (?,1) 16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D) True (?,1) Signature: {(evalEx1bb1in,4) ;(evalEx1bb4in,4) ;(evalEx1bb5in,4) ;(evalEx1bb6in,4) ;(evalEx1bbin,4) ;(evalEx1entryin,4) ;(evalEx1returnin,4) ;(evalEx1start,4) ;(evalEx1stop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,8,9,10,11,12,13,14},6->{15},7->{5,6},8->{5,6},9->{5,6} ,10->{5,6},11->{5,6},12->{5,6},13->{5,6},14->{5,6},15->{2,3},16->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. evalEx1start(A,B,C,D) -> evalEx1entryin(A,B,C,D) True (1,1) 1. evalEx1entryin(A,B,C,D) -> evalEx1bb6in(0,A,C,D) True (1,1) 2. evalEx1bb6in(A,B,C,D) -> evalEx1bbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalEx1bb6in(A,B,C,D) -> evalEx1returnin(A,B,C,D) [A >= B] (1,1) 4. evalEx1bbin(A,B,C,D) -> evalEx1bb4in(A,B,1 + A,B) True (?,1) 5. evalEx1bb4in(A,B,C,D) -> evalEx1bb1in(A,B,C,D) [D >= 1 + C] (?,1) 6. evalEx1bb4in(A,B,C,D) -> evalEx1bb5in(A,B,C,D) [C >= D] (?,1) 7. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1) 8. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E && E >= 1] (?,1) 9. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1] (?,1) 10. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,D) [0 >= 1] (?,1) 11. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,D) [0 >= 1] (?,1) 12. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1] (?,1) 13. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1] (?,1) 14. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,D) True (?,1) 15. evalEx1bb5in(A,B,C,D) -> evalEx1bb6in(1 + A,D,C,D) True (?,1) 16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D) True (1,1) Signature: {(evalEx1bb1in,4) ;(evalEx1bb4in,4) ;(evalEx1bb5in,4) ;(evalEx1bb6in,4) ;(evalEx1bbin,4) ;(evalEx1entryin,4) ;(evalEx1returnin,4) ;(evalEx1start,4) ;(evalEx1stop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,8,9,10,11,12,13,14},6->{15},7->{5,6},8->{5,6},9->{5,6} ,10->{5,6},11->{5,6},12->{5,6},13->{5,6},14->{5,6},15->{2,3},16->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [8,10,11,12,13] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. evalEx1start(A,B,C,D) -> evalEx1entryin(A,B,C,D) True (1,1) 1. evalEx1entryin(A,B,C,D) -> evalEx1bb6in(0,A,C,D) True (1,1) 2. evalEx1bb6in(A,B,C,D) -> evalEx1bbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalEx1bb6in(A,B,C,D) -> evalEx1returnin(A,B,C,D) [A >= B] (1,1) 4. evalEx1bbin(A,B,C,D) -> evalEx1bb4in(A,B,1 + A,B) True (?,1) 5. evalEx1bb4in(A,B,C,D) -> evalEx1bb1in(A,B,C,D) [D >= 1 + C] (?,1) 6. evalEx1bb4in(A,B,C,D) -> evalEx1bb5in(A,B,C,D) [C >= D] (?,1) 7. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1) 9. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1] (?,1) 14. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,D) True (?,1) 15. evalEx1bb5in(A,B,C,D) -> evalEx1bb6in(1 + A,D,C,D) True (?,1) 16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D) True (1,1) Signature: {(evalEx1bb1in,4) ;(evalEx1bb4in,4) ;(evalEx1bb5in,4) ;(evalEx1bb6in,4) ;(evalEx1bbin,4) ;(evalEx1entryin,4) ;(evalEx1returnin,4) ;(evalEx1start,4) ;(evalEx1stop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3},16->{}] + Applied Processor: AddSinks + Details: () * Step 4: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. evalEx1start(A,B,C,D) -> evalEx1entryin(A,B,C,D) True (1,1) 1. evalEx1entryin(A,B,C,D) -> evalEx1bb6in(0,A,C,D) True (?,1) 2. evalEx1bb6in(A,B,C,D) -> evalEx1bbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalEx1bb6in(A,B,C,D) -> evalEx1returnin(A,B,C,D) [A >= B] (?,1) 4. evalEx1bbin(A,B,C,D) -> evalEx1bb4in(A,B,1 + A,B) True (?,1) 5. evalEx1bb4in(A,B,C,D) -> evalEx1bb1in(A,B,C,D) [D >= 1 + C] (?,1) 6. evalEx1bb4in(A,B,C,D) -> evalEx1bb5in(A,B,C,D) [C >= D] (?,1) 7. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1) 9. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1] (?,1) 14. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,D) True (?,1) 15. evalEx1bb5in(A,B,C,D) -> evalEx1bb6in(1 + A,D,C,D) True (?,1) 16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D) True (?,1) 17. evalEx1returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalEx1bb1in,4) ;(evalEx1bb4in,4) ;(evalEx1bb5in,4) ;(evalEx1bb6in,4) ;(evalEx1bbin,4) ;(evalEx1entryin,4) ;(evalEx1returnin,4) ;(evalEx1start,4) ;(evalEx1stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{16,17},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3} ,16->{},17->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,9,14,15,16,17] | `- p:[2,15,6,4,7,5,9,14] c: [2] | `- p:[5,7,9,14] c: [5] * Step 5: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. evalEx1start(A,B,C,D) -> evalEx1entryin(A,B,C,D) True (1,1) 1. evalEx1entryin(A,B,C,D) -> evalEx1bb6in(0,A,C,D) True (?,1) 2. evalEx1bb6in(A,B,C,D) -> evalEx1bbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalEx1bb6in(A,B,C,D) -> evalEx1returnin(A,B,C,D) [A >= B] (?,1) 4. evalEx1bbin(A,B,C,D) -> evalEx1bb4in(A,B,1 + A,B) True (?,1) 5. evalEx1bb4in(A,B,C,D) -> evalEx1bb1in(A,B,C,D) [D >= 1 + C] (?,1) 6. evalEx1bb4in(A,B,C,D) -> evalEx1bb5in(A,B,C,D) [C >= D] (?,1) 7. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1) 9. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1] (?,1) 14. evalEx1bb1in(A,B,C,D) -> evalEx1bb4in(A,B,1 + C,D) True (?,1) 15. evalEx1bb5in(A,B,C,D) -> evalEx1bb6in(1 + A,D,C,D) True (?,1) 16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D) True (?,1) 17. evalEx1returnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalEx1bb1in,4) ;(evalEx1bb4in,4) ;(evalEx1bb5in,4) ;(evalEx1bb6in,4) ;(evalEx1bbin,4) ;(evalEx1entryin,4) ;(evalEx1returnin,4) ;(evalEx1start,4) ;(evalEx1stop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{16,17},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3} ,16->{},17->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,9,14,15,16,17] | `- p:[2,15,6,4,7,5,9,14] c: [2] | `- p:[5,7,9,14] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 6: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalEx1start ~> evalEx1entryin [A <= A, B <= B, C <= C, D <= D] evalEx1entryin ~> evalEx1bb6in [A <= 0*K, B <= A, C <= C, D <= D] evalEx1bb6in ~> evalEx1bbin [A <= A, B <= B, C <= C, D <= D] evalEx1bb6in ~> evalEx1returnin [A <= A, B <= B, C <= C, D <= D] evalEx1bbin ~> evalEx1bb4in [A <= A, B <= B, C <= K + A, D <= B] evalEx1bb4in ~> evalEx1bb1in [A <= A, B <= B, C <= C, D <= D] evalEx1bb4in ~> evalEx1bb5in [A <= A, B <= B, C <= C, D <= D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= K + C, D <= D] evalEx1bb5in ~> evalEx1bb6in [A <= K + A, B <= D, C <= C, D <= D] evalEx1returnin ~> evalEx1stop [A <= A, B <= B, C <= C, D <= D] evalEx1returnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 2*K + A + B + D] evalEx1bb6in ~> evalEx1bbin [A <= A, B <= B, C <= C, D <= D] evalEx1bb5in ~> evalEx1bb6in [A <= K + A, B <= D, C <= C, D <= D] evalEx1bb4in ~> evalEx1bb5in [A <= A, B <= B, C <= C, D <= D] evalEx1bbin ~> evalEx1bb4in [A <= A, B <= B, C <= K + A, D <= B] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb4in ~> evalEx1bb1in [A <= A, B <= B, C <= C, D <= D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= K + C, D <= D] + Loop: [0.0.0 <= 2*K + C + D] evalEx1bb4in ~> evalEx1bb1in [A <= A, B <= B, C <= C, D <= D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= C, D <= K + D] evalEx1bb1in ~> evalEx1bb4in [A <= A, B <= B, C <= K + C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 7: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalEx1start ~> evalEx1entryin [] evalEx1entryin ~> evalEx1bb6in [A ~=> B,K ~=> A] evalEx1bb6in ~> evalEx1bbin [] evalEx1bb6in ~> evalEx1returnin [] evalEx1bbin ~> evalEx1bb4in [B ~=> D,A ~+> C,K ~+> C] evalEx1bb4in ~> evalEx1bb1in [] evalEx1bb4in ~> evalEx1bb5in [] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb1in ~> evalEx1bb4in [C ~+> C,K ~+> C] evalEx1bb5in ~> evalEx1bb6in [D ~=> B,A ~+> A,K ~+> A] evalEx1returnin ~> evalEx1stop [] evalEx1returnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,D ~+> 0.0,K ~*> 0.0] evalEx1bb6in ~> evalEx1bbin [] evalEx1bb5in ~> evalEx1bb6in [D ~=> B,A ~+> A,K ~+> A] evalEx1bb4in ~> evalEx1bb5in [] evalEx1bbin ~> evalEx1bb4in [B ~=> D,A ~+> C,K ~+> C] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb4in ~> evalEx1bb1in [] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb1in ~> evalEx1bb4in [C ~+> C,K ~+> C] + Loop: [C ~+> 0.0.0,D ~+> 0.0.0,K ~*> 0.0.0] evalEx1bb4in ~> evalEx1bb1in [] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb1in ~> evalEx1bb4in [D ~+> D,K ~+> D] evalEx1bb1in ~> evalEx1bb4in [C ~+> C,K ~+> C] + Applied Processor: LareProcessor + Details: evalEx1start ~> exitus616 [A ~=> B ,A ~=> D ,K ~=> A ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,D ~*> A ,D ~*> B ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> C ,D ~^> D ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> C ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] evalEx1start ~> evalEx1stop [A ~=> B ,A ~=> D ,K ~=> A ,A ~+> B ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,D ~*> A ,D ~*> B ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,D ~^> B ,D ~^> C ,D ~^> D ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> C ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalEx1bb6in> [B ~=> D ,A ~+> A ,A ~+> C ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,D ~+> 0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> C ,B ~*> D ,B ~*> 0.0.0 ,B ~*> tick ,D ~*> A ,D ~*> B ,D ~*> C ,D ~*> D ,D ~*> 0.0.0 ,D ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,A ~^> B ,A ~^> C ,A ~^> D ,A ~^> 0.0.0 ,A ~^> tick ,B ~^> B ,B ~^> C ,B ~^> D ,B ~^> 0.0.0 ,B ~^> tick ,D ~^> B ,D ~^> C ,D ~^> D ,D ~^> 0.0.0 ,D ~^> tick ,K ~^> B ,K ~^> C ,K ~^> D ,K ~^> 0.0.0 ,K ~^> tick] + evalEx1bb4in> [C ~+> C ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> 0.0.0 ,D ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,C ~*> C ,C ~*> D ,D ~*> C ,D ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)