Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalcousot9start
      0: evalcousot9start -> evalcousot9entryin : [], cost: 1
      1: evalcousot9entryin -> evalcousot9bb3in : A'=free, B'=C, [], cost: 1
      2: evalcousot9bb3in -> evalcousot9bbin : [ B>=1 ], cost: 1
      3: evalcousot9bb3in -> evalcousot9returnin : [ 0>=B ], cost: 1
      4: evalcousot9bbin -> evalcousot9bb1in : [ A>=1 ], cost: 1
      5: evalcousot9bbin -> evalcousot9bb2in : [ 0>=A ], cost: 1
      8: evalcousot9returnin -> evalcousot9stop : [], cost: 1
      6: evalcousot9bb1in -> evalcousot9bb3in : A'=-1+A, [], cost: 1
      7: evalcousot9bb2in -> evalcousot9bb3in : A'=C, B'=-1+B, [], cost: 1


Simplified the transitions:
  Start location: evalcousot9start
      0: evalcousot9start -> evalcousot9entryin : [], cost: 1
      1: evalcousot9entryin -> evalcousot9bb3in : A'=free, B'=C, [], cost: 1
      2: evalcousot9bb3in -> evalcousot9bbin : [ B>=1 ], cost: 1
      4: evalcousot9bbin -> evalcousot9bb1in : [ A>=1 ], cost: 1
      5: evalcousot9bbin -> evalcousot9bb2in : [ 0>=A ], cost: 1
      6: evalcousot9bb1in -> evalcousot9bb3in : A'=-1+A, [], cost: 1
      7: evalcousot9bb2in -> evalcousot9bb3in : A'=C, B'=-1+B, [], cost: 1


Applied simple chaining:
  Start location: evalcousot9start
      0: evalcousot9start -> evalcousot9bb3in : A'=free, B'=C, [], cost: 2
      2: evalcousot9bb3in -> evalcousot9bbin : [ B>=1 ], cost: 1
      4: evalcousot9bbin -> evalcousot9bb3in : A'=-1+A, [ A>=1 ], cost: 2
      5: evalcousot9bbin -> evalcousot9bb3in : A'=C, B'=-1+B, [ 0>=A ], cost: 2


Applied chaining over branches and pruning:
  Start location: evalcousot9start
      0: evalcousot9start -> evalcousot9bb3in : A'=free, B'=C, [], cost: 2
      9: evalcousot9bb3in -> evalcousot9bb3in : A'=-1+A, [ B>=1 && A>=1 ], cost: 3
     10: evalcousot9bb3in -> evalcousot9bb3in : A'=C, B'=-1+B, [ B>=1 && 0>=A ], cost: 3

Eliminating 2 self-loops for location evalcousot9bb3in
  Self-Loop 9 has the metering function: A, resulting in the new transition 11.
  Found this metering function when nesting loops: -1+B,
  and nested parallel self-loops 12 (outer loop) and 11 (inner loop), obtaining the new transitions: 13, 14.
  Found this metering function when nesting loops: -1+A,
  Removing the self-loops: 9 10 12.
Adding an epsilon transition (to model nonexecution of the loops): 15.

Removed all Self-loops using metering functions (where possible):
  Start location: evalcousot9start
      0: evalcousot9start -> evalcousot9bb3in : A'=free, B'=C, [], cost: 2
     11: evalcousot9bb3in -> [8] : A'=0, [ B>=1 && A>=1 ], cost: 3*A
     13: evalcousot9bb3in -> [8] : A'=0, B'=1, [ B>=1 && 0>=A && -1+B>=1 && C>=1 ], cost: -3+3*B+3*C*(-1+B)
     14: evalcousot9bb3in -> [8] : A'=0, B'=1, [ B>=1 && A>=1 && B>=1 && 0>=0 && -1+B>=1 && C>=1 ], cost: -3+3*B+3*C*(-1+B)+3*A
     15: evalcousot9bb3in -> [8] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: evalcousot9start
     16: evalcousot9start -> [8] : A'=0, B'=C, [ C>=1 && free>=1 ], cost: 2+3*free
     17: evalcousot9start -> [8] : A'=0, B'=1, [ C>=1 && 0>=free && -1+C>=1 && C>=1 ], cost: -1+3*(-1+C)*C+3*C
     18: evalcousot9start -> [8] : A'=0, B'=1, [ C>=1 && free>=1 && C>=1 && 0>=0 && -1+C>=1 && C>=1 ], cost: -1+3*free+3*(-1+C)*C+3*C


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalcousot9start
     16: evalcousot9start -> [8] : A'=0, B'=C, [ C>=1 && free>=1 ], cost: 2+3*free
     17: evalcousot9start -> [8] : A'=0, B'=1, [ C>=1 && 0>=free && -1+C>=1 && C>=1 ], cost: -1+3*(-1+C)*C+3*C
     18: evalcousot9start -> [8] : A'=0, B'=1, [ C>=1 && free>=1 && C>=1 && 0>=0 && -1+C>=1 && C>=1 ], cost: -1+3*free+3*(-1+C)*C+3*C


Computing complexity for remaining 3 transitions.

  Found configuration with infinitely models for cost: 2+3*free
  and guard: C>=1 && free>=1:
  free: Pos, C: Pos

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: C>=1 && free>=1
  Final Cost:  2+3*free

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: INF
  Complexity value: INF

WORST_CASE(INF,?)