Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f12 : A'=free, B'=free, C'=free, D'=0, [], cost: 1 1: f12 -> f12 : D'=1+D, E'=free_1, [ C>=1+D ], cost: 1 11: f12 -> f27 : [ D>=C ], cost: 1 2: f27 -> f27 : F'=free_2, [ 0>=1+free_3 ], cost: 1 3: f27 -> f27 : F'=free_4, [], cost: 1 10: f27 -> f42 : [], cost: 1 4: f42 -> f42 : [ free_6>=1+free_5 ], cost: 1 5: f42 -> f42 : [], cost: 1 9: f42 -> f55 : [], cost: 1 6: f55 -> f55 : [ free_8>=1+free_7 ], cost: 1 7: f55 -> f55 : [], cost: 1 8: f55 -> f66 : [], cost: 1 Removing duplicate transition: 4. Removing duplicate transition: 6. Simplified the transitions: Start location: f0 0: f0 -> f12 : A'=free, B'=free, C'=free, D'=0, [], cost: 1 1: f12 -> f12 : D'=1+D, E'=free_1, [ C>=1+D ], cost: 1 11: f12 -> f27 : [ D>=C ], cost: 1 2: f27 -> f27 : F'=free_2, [], cost: 1 3: f27 -> f27 : F'=free_4, [], cost: 1 10: f27 -> f42 : [], cost: 1 5: f42 -> f42 : [], cost: 1 9: f42 -> f55 : [], cost: 1 7: f55 -> f55 : [], cost: 1 Eliminating 1 self-loops for location f12 Self-Loop 1 has the metering function: C-D, resulting in the new transition 12. Removing the self-loops: 1. Eliminating 2 self-loops for location f27 Self-Loop 2 has unbounded runtime, resulting in the new transition 13. Self-Loop 3 has unbounded runtime, resulting in the new transition 14. Removing the self-loops: 2 3. Removing duplicate transition: 13. Eliminating 1 self-loops for location f42 Self-Loop 5 has unbounded runtime, resulting in the new transition 15. Removing the self-loops: 5. Eliminating 1 self-loops for location f55 Self-Loop 7 has unbounded runtime, resulting in the new transition 16. Removing the self-loops: 7. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f12 : A'=free, B'=free, C'=free, D'=0, [], cost: 1 12: f12 -> [6] : D'=C, E'=free_1, [ C>=1+D ], cost: C-D 14: f27 -> [7] : [], cost: INF 15: f42 -> [8] : [], cost: INF 16: f55 -> [9] : [], cost: INF 11: [6] -> f27 : [ D>=C ], cost: 1 10: [7] -> f42 : [], cost: 1 9: [8] -> f55 : [], cost: 1 Applied simple chaining: Start location: f0 0: f0 -> [9] : A'=free, B'=free, C'=free, D'=free, E'=free_1, [ free>=1 && free>=free ], cost: INF Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 0: f0 -> [9] : A'=free, B'=free, C'=free, D'=free, E'=free_1, [ free>=1 && free>=free ], 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: free>=1 && free>=free 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,?)