Trying to load file: main.koat

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


Simplified the transitions:
  Start location: start0
      2: start -> lbl121 : E'=B-D, [ A>=1 && C>=1+A && B==C && D==A && E==F ], cost: 1
      9: lbl121 -> lbl121 : E'=E-D, [ E>=1 && E>=A && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: 1
      8: lbl121 -> lbl111 : E'=-1+E, [ E>=1 && A>=1+E && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: 1
      6: lbl111 -> lbl121 : E'=E-D, [ E>=1 && E>=A && C>=1+E+A && A>=2+E && D==A && B==C ], cost: 1
      5: lbl111 -> lbl111 : E'=-1+E, [ E>=1 && C>=1+E+A && A>=2+E && D==A && B==C ], cost: 1
     11: start0 -> start : B'=C, D'=A, E'=F, [], cost: 1

Eliminating 1 self-loops for location lbl121
  Self-Loop 9 has the metering function: -D+A, resulting in the new transition 12.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location lbl111
  Self-Loop 5 has the metering function: E, resulting in the new transition 13.
  Removing the self-loops: 5.

Removed all Self-loops using metering functions (where possible):
  Start location: start0
      2: start -> lbl121 : E'=B-D, [ A>=1 && C>=1+A && B==C && D==A && E==F ], cost: 1
     12: lbl121 -> [7] : E'=E+(D-A)*D, [ E>=1 && E>=A && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: -D+A
     13: lbl111 -> [8] : E'=0, [ E>=1 && C>=1+E+A && A>=2+E && D==A && B==C ], cost: E
     11: start0 -> start : B'=C, D'=A, E'=F, [], cost: 1
      8: [7] -> lbl111 : E'=-1+E, [ E>=1 && A>=1+E && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: 1
      6: [8] -> lbl121 : E'=E-D, [ E>=1 && E>=A && C>=1+E+A && A>=2+E && D==A && B==C ], cost: 1


Applied simple chaining:
  Start location: start0
     12: lbl121 -> [7] : E'=E+(D-A)*D, [ E>=1 && E>=A && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: -D+A
     11: start0 -> lbl121 : B'=C, D'=A, E'=C-A, [ A>=1 && C>=1+A && C==C && A==A && F==F ], cost: 2
      8: [7] -> [8] : E'=0, [ E>=1 && A>=1+E && C>=1+A && A>=1 && C>=E+A && D==A && B==C && -1+E>=1 && C>=E+A && A>=1+E && D==A && B==C ], cost: E
      6: [8] -> lbl121 : E'=E-D, [ E>=1 && E>=A && C>=1+E+A && A>=2+E && D==A && B==C ], cost: 1


Applied chaining over branches and pruning:
  Start location: start0
     14: lbl121 -> [9] : E'=E+(D-A)*D, [ E>=1 && E>=A && C>=1+A && A>=1 && C>=E+A && D==A && B==C ], cost: -D+A
     11: start0 -> lbl121 : B'=C, D'=A, E'=C-A, [ A>=1 && C>=1+A && C==C && A==A && F==F ], cost: 2


Applied simple chaining:
  Start location: start0
     11: start0 -> [9] : B'=C, D'=A, E'=C-A, [ A>=1 && C>=1+A && C==C && A==A && F==F && C-A>=1 && C-A>=A && C>=1+A && A>=1 && C>=C && A==A && C==C ], cost: 2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start0
     11: start0 -> [9] : B'=C, D'=A, E'=C-A, [ A>=1 && C>=1+A && C==C && A==A && F==F && C-A>=1 && C-A>=A && C>=1+A && A>=1 && C>=C && A==A && C==C ], cost: 2


Computing complexity for remaining 1 transitions.

Found new complexity const, because: const cost.


The final runtime is determined by this resulting transition:
  Final Guard: A>=1 && C>=1+A && C==C && A==A && F==F && C-A>=1 && C-A>=A && C>=1+A && A>=1 && C>=C && A==A && C==C
  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),?)