Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f3 : [], cost: 1 5: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=A, H'=B, [], cost: 1 6: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=free_1, H'=free, Q'=free_1, J'=free, [], cost: 1 9: f0 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [], cost: 1 11: f0 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [], cost: 1 1: f0 -> f4 : [], cost: 1 2: f0 -> f8 : [], cost: 1 7: f0 -> f8 : A'=free_3, B'=free_5, C'=D, D'=free_4, E'=F, F'=free_2, G'=A, H'=B, Q'=free_4, J'=free_2, K'=free_3, L'=free_5, [], cost: 1 3: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ A>=1+B ], cost: 1 4: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 8: f3 -> f8 : A'=free_7, B'=free_9, C'=D, D'=free_8, E'=F, F'=free_6, G'=A, H'=A, Q'=free_8, J'=free_6, K'=free_7, L'=free_9, [ A==B ], cost: 1 10: f4 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 12: f4 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [ A>=B ], cost: 1 Simplified the transitions: Start location: f0 0: f0 -> f3 : [], cost: 1 5: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=A, H'=B, [], cost: 1 6: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=free_1, H'=free, Q'=free_1, J'=free, [], cost: 1 9: f0 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [], cost: 1 11: f0 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [], cost: 1 1: f0 -> f4 : [], cost: 1 3: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ A>=1+B ], cost: 1 4: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 10: f4 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 12: f4 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [ A>=B ], cost: 1 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 0: f0 -> f3 : [], cost: 1 5: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=A, H'=B, [], cost: 1 6: f0 -> f3 : A'=F, B'=D, C'=D, E'=F, G'=free_1, H'=free, Q'=free_1, J'=free, [], cost: 1 9: f0 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [], cost: 1 11: f0 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [], cost: 1 1: f0 -> f4 : [], cost: 1 3: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ A>=1+B ], cost: 1 4: f3 -> f4 : C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 10: f4 -> f3 : A'=1+A, C'=D, E'=F, G'=A, H'=B, [ B>=1+A ], cost: 1 12: f4 -> f3 : B'=1+B, C'=D, E'=F, G'=A, H'=B, [ A>=B ], cost: 1 This is only a partial result (probably due to a timeout), trying to find max complexity Removed transitions with const cost Start location: f0 The final runtime is determined by this resulting transition: Final Guard: Final Cost: 1 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)