Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: eval -> eval : A'=0, [ 2*free>=0 && 0>=2*free && A==1 ], cost: 1
      1: eval -> eval : A'=2*free_1, [ 2*free_1>=0 && 2+2*free_1>=0 && A==1+2*free_1 ], cost: 1
      2: eval -> eval : A'=free_2, [ 1>=2*free_5 && 2*free_5>=0 && 2*free_6>=1 && 1>=2*free_6 && 1>=2*free_3 && 3*free_3>=2 && free_2>=free_3 && 1>=2*free_4 && 3*free_4>=2 && free_4>=free_2 && A==1 ], cost: 1
      3: eval -> eval : A'=free_7, [ 2*free_11>=1 && 1+2*free_11>=0 && 2*free_11>=2*free_10 && 1+2*free_10>=2*free_11 && 2*free_11>=2*free_8 && 3*free_8>=1+2*free_11 && free_7>=free_8 && 2*free_11>=2*free_9 && 3*free_9>=1+2*free_11 && free_9>=free_7 && A==2*free_11 ], cost: 1
      4: start -> eval : [], cost: 1


Simplified the transitions:
  Start location: start
      0: eval -> eval : A'=0, [ -2*free==0 && A==1 ], cost: 1
      1: eval -> eval : A'=2*free_1, [ 2*free_1>=0 && A==1+2*free_1 ], cost: 1
      2: eval -> eval : A'=free_2, [ 1>=2*free_5 && 2*free_5>=0 && 1-2*free_6==0 && 1>=2*free_3 && 3*free_3>=2 && free_2>=free_3 && 1>=2*free_4 && 3*free_4>=2 && free_4>=free_2 && A==1 ], cost: 1
      3: eval -> eval : A'=free_7, [ 2*free_11>=1 && 2*free_11>=2*free_10 && 1+2*free_10>=2*free_11 && 2*free_11>=2*free_8 && 3*free_8>=1+2*free_11 && free_7>=free_8 && 2*free_11>=2*free_9 && 3*free_9>=1+2*free_11 && free_9>=free_7 && A==2*free_11 ], cost: 1
      4: start -> eval : [], cost: 1

Eliminating 4 self-loops for location eval
  Self-Loop 0 has the metering function: -1+A, resulting in the new transition 5.
  Removing the self-loops: 0 1 2 3.
Adding an epsilon transition (to model nonexecution of the loops): 9.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      5: eval -> [2] : A'=0, [ -2*free==0 && A==1 ], cost: -1+A
      6: eval -> [2] : A'=2*free_1, [ 2*free_1>=0 && A==1+2*free_1 ], cost: 1
      7: eval -> [2] : A'=free_2, [ 1-2*free_6==0 ], cost: 1
      8: eval -> [2] : A'=free_7, [ 2*free_11>=1 && 2*free_11>=2*free_10 && 1+2*free_10>=2*free_11 && 2*free_11>=2*free_8 && 3*free_8>=1+2*free_11 && free_7>=free_8 && 2*free_11>=2*free_9 && 3*free_9>=1+2*free_11 && free_9>=free_7 && A==2*free_11 ], cost: 1
      9: eval -> [2] : [], cost: 0
      4: start -> eval : [], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     10: start -> [2] : A'=0, [ -2*free==0 && A==1 ], cost: A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start
     10: start -> [2] : A'=0, [ -2*free==0 && A==1 ], cost: A


Computing complexity for remaining 1 transitions.

Found new complexity const, because: const cost.


The final runtime is determined by this resulting transition:
  Final Guard: -2*free==0 && A==1
  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),?)