Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f15 : A'=2, [], cost: 1 1: f15 -> f18 : B'=A, [ 10>=A ], cost: 1 4: f15 -> f28 : [ A>=11 ], cost: 1 3: f18 -> f15 : A'=1+A, [], cost: 1 2: f18 -> f18 : B'=-1+B, C'=free, [ free_2>=1+free_1 ], cost: 1 Simplified the transitions: Start location: f0 0: f0 -> f15 : A'=2, [], cost: 1 1: f15 -> f18 : B'=A, [ 10>=A ], cost: 1 3: f18 -> f15 : A'=1+A, [], cost: 1 2: f18 -> f18 : B'=-1+B, C'=free, [], cost: 1 Eliminating 1 self-loops for location f18 Self-Loop 2 has unbounded runtime, resulting in the new transition 5. Removing the self-loops: 2. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f15 : A'=2, [], cost: 1 1: f15 -> f18 : B'=A, [ 10>=A ], cost: 1 5: f18 -> [4] : [], cost: INF 3: [4] -> f15 : A'=1+A, [], cost: 1 Applied simple chaining: Start location: f0 0: f0 -> f15 : A'=2, [], cost: 1 1: f15 -> f15 : A'=1+A, B'=A, [ 10>=A ], cost: INF Eliminating 1 self-loops for location f15 Removing the self-loops: 1. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f15 : A'=2, [], cost: 1 6: f15 -> [5] : A'=1+A, B'=A, [ 10>=A ], cost: INF Applied simple chaining: Start location: f0 0: f0 -> [5] : A'=3, B'=2, [ 10>=2 ], cost: INF Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 0: f0 -> [5] : A'=3, B'=2, [ 10>=2 ], cost: INF Computing complexity for remaining 1 transitions. Found new complexity INF, because: INF sat. The final runtime is determined by this resulting transition: Final Guard: 10>=2 Final Cost: INF Obtained the following complexity w.r.t. the length of the input n: Complexity class: INF Complexity value: INF WORST_CASE(INF,?)