Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f1 : C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 ], cost: 1 1: f1 -> f1 : B'=1+B, [ C+A>=1+2*B ], cost: 1 2: f1 -> f1 : B'=-1+B, [ 2*B>=2+C+A ], cost: 1 Eliminating 2 self-loops for location f1 Self-Loop 1 has the metering function: meter, resulting in the new transition 3. Self-Loop 2 has the metering function: meter_1, resulting in the new transition 4. Removing the self-loops: 1 2. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f1 : C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 ], cost: 1 3: f1 -> [2] : B'=B+meter, [ C+A>=1+2*B && 2*meter==-2*B+C+A ], cost: meter 4: f1 -> [2] : B'=B-meter_1, [ 2*B>=2+C+A && 2*meter_1==-1+2*B-C-A ], cost: meter_1 Applied chaining over branches and pruning: Start location: f0 5: f0 -> [2] : B'=B+meter, C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 && 2+A>=1+2*B && 2*meter==2-2*B+A ], cost: 1+meter 6: f0 -> [2] : B'=B-meter_1, C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 && 2*B>=4+A && 2*meter_1==-3+2*B-A ], cost: 1+meter_1 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 5: f0 -> [2] : B'=B+meter, C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 && 2+A>=1+2*B && 2*meter==2-2*B+A ], cost: 1+meter 6: f0 -> [2] : B'=B-meter_1, C'=2, [ A>=0 && 3>=A && 3>=B && B>=0 && 2*B>=4+A && 2*meter_1==-3+2*B-A ], cost: 1+meter_1 Computing complexity for remaining 2 transitions. Found configuration with infinitely models for cost: 1+meter and guard: A>=0 && 3>=A && 3>=B && B>=0 && 2+A>=1+2*B && 2*meter==2-2*B+A: B: Const, meter: Const, A: Both Found new complexity const, because: Found infinity configuration. Found configuration with infinitely models for cost: 1+meter_1 and guard: A>=0 && 3>=A && 3>=B && B>=0 && 2*B>=4+A && 2*meter_1==-3+2*B-A: B: Const, meter_1: Const, A: Both The final runtime is determined by this resulting transition: Final Guard: A>=0 && 3>=A && 3>=B && B>=0 && 2+A>=1+2*B && 2*meter==2-2*B+A Final Cost: 2 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)