Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start0
      0: start -> stop : [ 0>=A && B==C && D==A ], cost: 1
      1: start -> lbl6 : [ A>=1 && 0>=C && B==C && D==A ], cost: 1
      2: start -> cut : [ A>=1 && D==A && B==A && C==A ], cost: 1
      3: start -> lbl101 : B'=B-D, [ A>=1 && C>=1+A && B==C && D==A ], cost: 1
      4: start -> lbl111 : D'=-B+D, [ A>=1+C && C>=1 && B==C && D==A ], cost: 1
      5: lbl6 -> stop : [ A>=1 && 0>=C && D==A && B==C ], cost: 1
     12: cut -> stop : [ A>=B && B>=1 && C>=B && D==B ], cost: 1
      6: lbl101 -> cut : [ A>=B && B>=1 && C>=2*B && D==B ], cost: 1
      7: lbl101 -> lbl101 : B'=B-D, [ B>=1+D && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
      8: lbl101 -> lbl111 : D'=-B+D, [ D>=1+B && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
      9: lbl111 -> cut : [ C>=B && B>=1 && A>=2*B && D==B ], cost: 1
     10: lbl111 -> lbl101 : B'=B-D, [ B>=1+D && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     11: lbl111 -> lbl111 : D'=-B+D, [ D>=1+B && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     13: start0 -> start : B'=C, D'=A, [], cost: 1


Simplified the transitions:
  Start location: start0
      3: start -> lbl101 : B'=B-D, [ A>=1 && C>=1+A && B==C && D==A ], cost: 1
      4: start -> lbl111 : D'=-B+D, [ A>=1+C && C>=1 && B==C && D==A ], cost: 1
      7: lbl101 -> lbl101 : B'=B-D, [ B>=1+D && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
      8: lbl101 -> lbl111 : D'=-B+D, [ D>=1+B && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
     10: lbl111 -> lbl101 : B'=B-D, [ B>=1+D && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     11: lbl111 -> lbl111 : D'=-B+D, [ D>=1+B && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     13: start0 -> start : B'=C, D'=A, [], cost: 1

Eliminating 1 self-loops for location lbl101
  Removing the self-loops: 7.
Adding an epsilon transition (to model nonexecution of the loops): 15.
Eliminating 1 self-loops for location lbl111
  Removing the self-loops: 11.
Adding an epsilon transition (to model nonexecution of the loops): 17.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      3: start -> lbl101 : B'=B-D, [ A>=1 && C>=1+A && B==C && D==A ], cost: 1
      4: start -> lbl111 : D'=-B+D, [ A>=1+C && C>=1 && B==C && D==A ], cost: 1
     14: lbl101 -> [7] : B'=B-D, [ B>=1+D && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
     15: lbl101 -> [7] : [], cost: 0
     16: lbl111 -> [8] : D'=-B+D, [ D>=1+B && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     17: lbl111 -> [8] : [], cost: 0
     13: start0 -> start : B'=C, D'=A, [], cost: 1
      8: [7] -> lbl111 : D'=-B+D, [ D>=1+B && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
     10: [8] -> lbl101 : B'=B-D, [ B>=1+D && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     20: lbl101 -> lbl111 : B'=B-D, D'=-B+2*D, [ B>=1+D && A>=D && B>=1 && D>=1 && C>=B+D && D>=1+B-D && A>=D && B-D>=1 && D>=1 && C>=B ], cost: 2
     21: lbl101 -> lbl111 : D'=-B+D, [ D>=1+B && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
     22: lbl111 -> lbl101 : B'=2*B-D, D'=-B+D, [ D>=1+B && C>=B && B>=1 && D>=1 && A>=B+D && B>=1-B+D && C>=B && B>=1 && -B+D>=1 && A>=D ], cost: 2
     23: lbl111 -> lbl101 : B'=B-D, [ B>=1+D && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     18: start0 -> lbl101 : B'=C-A, D'=A, [ A>=1 && C>=1+A && C==C && A==A ], cost: 2
     19: start0 -> lbl111 : B'=C, D'=-C+A, [ A>=1+C && C>=1 && C==C && A==A ], cost: 2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
     20: lbl101 -> lbl111 : B'=B-D, D'=-B+2*D, [ B>=1+D && A>=D && B>=1 && D>=1 && C>=B+D && D>=1+B-D && A>=D && B-D>=1 && D>=1 && C>=B ], cost: 2
     21: lbl101 -> lbl111 : D'=-B+D, [ D>=1+B && A>=D && B>=1 && D>=1 && C>=B+D ], cost: 1
     22: lbl111 -> lbl101 : B'=2*B-D, D'=-B+D, [ D>=1+B && C>=B && B>=1 && D>=1 && A>=B+D && B>=1-B+D && C>=B && B>=1 && -B+D>=1 && A>=D ], cost: 2
     23: lbl111 -> lbl101 : B'=B-D, [ B>=1+D && C>=B && B>=1 && D>=1 && A>=B+D ], cost: 1
     18: start0 -> lbl101 : B'=C-A, D'=A, [ A>=1 && C>=1+A && C==C && A==A ], cost: 2
     19: start0 -> lbl111 : B'=C, D'=-C+A, [ A>=1+C && C>=1 && C==C && A==A ], cost: 2

This is only a partial result (probably due to a timeout), trying to find max complexity

Removed transitions with const cost
  Start location: start0
    <empty>


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),?)