Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: f2 -> f8 : C'=0, D'=B, [ A>=1+B ], cost: 1
     21: f2 -> f1 : [ B>=A ], cost: 1
      1: f8 -> f8 : E'=1+E, F'=free_1, G'=free, [ A>=E && free>=free_1 ], cost: 1
      2: f8 -> f8 : C'=free_4, D'=E, E'=1+E, F'=free_3, G'=free_2, [ A>=E && free_3>=1+free_2 ], cost: 1
     19: f8 -> f19 : [ B>=1+D && E>=1+A ], cost: 1
     20: f8 -> f19 : [ D>=1+B && E>=1+A ], cost: 1
     18: f8 -> f34 : D'=B, [ E>=1+A && B==D ], cost: 1
      3: f19 -> f19 : E'=1+E, H'=free_5, [ A>=E ], cost: 1
     17: f19 -> f27 : [ E>=1+A ], cost: 1
      4: f27 -> f27 : E'=1+E, H'=free_6, [ A>=E ], cost: 1
     16: f27 -> f34 : [ E>=1+A ], cost: 1
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
      5: f34 -> f36 : [ 0>=1+C ], cost: 1
      6: f34 -> f36 : [ C>=1 ], cost: 1
     15: f36 -> f2 : B'=1+B, [ D>=1+A ], cost: 1
     11: f36 -> f36 : D'=1+D, H'=0, [ A>=D ], cost: 1
      7: f36 -> f43 : H'=free_7, [ A>=D && 0>=1+free_8 ], cost: 1
      8: f36 -> f43 : H'=free_9, [ A>=D && free_10>=1 ], cost: 1
      9: f43 -> f43 : E'=1+E, [ A>=E ], cost: 1
     14: f43 -> f49 : [ E>=1+A ], cost: 1
     13: f49 -> f36 : D'=1+D, [ E>=1+A ], cost: 1
     10: f49 -> f49 : E'=1+E, [ A>=E ], cost: 1
     22: start -> f2 : [], cost: 1


Simplified the transitions:
  Start location: start
      0: f2 -> f8 : C'=0, D'=B, [ A>=1+B ], cost: 1
      1: f8 -> f8 : E'=1+E, F'=free_1, G'=free, [ A>=E && free>=free_1 ], cost: 1
      2: f8 -> f8 : C'=free_4, D'=E, E'=1+E, F'=free_3, G'=free_2, [ A>=E && free_3>=1+free_2 ], cost: 1
     19: f8 -> f19 : [ B>=1+D && E>=1+A ], cost: 1
     20: f8 -> f19 : [ D>=1+B && E>=1+A ], cost: 1
     18: f8 -> f34 : D'=B, [ E>=1+A && B==D ], cost: 1
      3: f19 -> f19 : E'=1+E, H'=free_5, [ A>=E ], cost: 1
     17: f19 -> f27 : [ E>=1+A ], cost: 1
      4: f27 -> f27 : E'=1+E, H'=free_6, [ A>=E ], cost: 1
     16: f27 -> f34 : [ E>=1+A ], cost: 1
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
      5: f34 -> f36 : [ 0>=1+C ], cost: 1
      6: f34 -> f36 : [ C>=1 ], cost: 1
     15: f36 -> f2 : B'=1+B, [ D>=1+A ], cost: 1
     11: f36 -> f36 : D'=1+D, H'=0, [ A>=D ], cost: 1
      7: f36 -> f43 : H'=free_7, [ A>=D ], cost: 1
      8: f36 -> f43 : H'=free_9, [ A>=D ], cost: 1
      9: f43 -> f43 : E'=1+E, [ A>=E ], cost: 1
     14: f43 -> f49 : [ E>=1+A ], cost: 1
     13: f49 -> f36 : D'=1+D, [ E>=1+A ], cost: 1
     10: f49 -> f49 : E'=1+E, [ A>=E ], cost: 1
     22: start -> f2 : [], cost: 1

Eliminating 2 self-loops for location f8
  Self-Loop 1 has the metering function: 1-E+A, resulting in the new transition 23.
  Self-Loop 2 has the metering function: 1-E+A, resulting in the new transition 24.
  Removing the self-loops: 1 2.
Eliminating 1 self-loops for location f19
  Self-Loop 3 has the metering function: 1-E+A, resulting in the new transition 25.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f27
  Self-Loop 4 has the metering function: 1-E+A, resulting in the new transition 26.
  Removing the self-loops: 4.
Eliminating 1 self-loops for location f36
  Self-Loop 11 has the metering function: 1-D+A, resulting in the new transition 27.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location f43
  Self-Loop 9 has the metering function: 1-E+A, resulting in the new transition 28.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f49
  Self-Loop 10 has the metering function: 1-E+A, resulting in the new transition 29.
  Removing the self-loops: 10.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      0: f2 -> f8 : C'=0, D'=B, [ A>=1+B ], cost: 1
     23: f8 -> [10] : E'=1+A, F'=free_1, G'=free, [ A>=E && free>=free_1 ], cost: 1-E+A
     24: f8 -> [10] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=E && free_3>=1+free_2 ], cost: 1-E+A
     25: f19 -> [11] : E'=1+A, H'=free_5, [ A>=E ], cost: 1-E+A
     26: f27 -> [12] : E'=1+A, H'=free_6, [ A>=E ], cost: 1-E+A
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
      5: f34 -> f36 : [ 0>=1+C ], cost: 1
      6: f34 -> f36 : [ C>=1 ], cost: 1
     27: f36 -> [13] : D'=1+A, H'=0, [ A>=D ], cost: 1-D+A
     28: f43 -> [14] : E'=1+A, [ A>=E ], cost: 1-E+A
     29: f49 -> [15] : E'=1+A, [ A>=E ], cost: 1-E+A
     22: start -> f2 : [], cost: 1
     19: [10] -> f19 : [ B>=1+D && E>=1+A ], cost: 1
     20: [10] -> f19 : [ D>=1+B && E>=1+A ], cost: 1
     18: [10] -> f34 : D'=B, [ E>=1+A && B==D ], cost: 1
     17: [11] -> f27 : [ E>=1+A ], cost: 1
     16: [12] -> f34 : [ E>=1+A ], cost: 1
     15: [13] -> f2 : B'=1+B, [ D>=1+A ], cost: 1
      7: [13] -> f43 : H'=free_7, [ A>=D ], cost: 1
      8: [13] -> f43 : H'=free_9, [ A>=D ], cost: 1
     14: [14] -> f49 : [ E>=1+A ], cost: 1
     13: [15] -> f36 : D'=1+D, [ E>=1+A ], cost: 1


Applied simple chaining:
  Start location: start
      0: f2 -> f8 : C'=0, D'=B, [ A>=1+B ], cost: 1
     23: f8 -> [10] : E'=1+A, F'=free_1, G'=free, [ A>=E && free>=free_1 ], cost: 1-E+A
     24: f8 -> [10] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=E && free_3>=1+free_2 ], cost: 1-E+A
     25: f19 -> f27 : E'=1+A, H'=free_5, [ A>=E && 1+A>=1+A ], cost: 2-E+A
     26: f27 -> f34 : E'=1+A, H'=free_6, [ A>=E && 1+A>=1+A ], cost: 2-E+A
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
      5: f34 -> f36 : [ 0>=1+C ], cost: 1
      6: f34 -> f36 : [ C>=1 ], cost: 1
     27: f36 -> [13] : D'=1+A, H'=0, [ A>=D ], cost: 1-D+A
     28: f43 -> f49 : E'=1+A, [ A>=E && 1+A>=1+A ], cost: 2-E+A
     29: f49 -> f36 : D'=1+D, E'=1+A, [ A>=E && 1+A>=1+A ], cost: 2-E+A
     22: start -> f2 : [], cost: 1
     19: [10] -> f19 : [ B>=1+D && E>=1+A ], cost: 1
     20: [10] -> f19 : [ D>=1+B && E>=1+A ], cost: 1
     18: [10] -> f34 : D'=B, [ E>=1+A && B==D ], cost: 1
     15: [13] -> f2 : B'=1+B, [ D>=1+A ], cost: 1
      7: [13] -> f43 : H'=free_7, [ A>=D ], cost: 1
      8: [13] -> f43 : H'=free_9, [ A>=D ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     30: f2 -> [10] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 2-E+A
     31: f2 -> [10] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 2-E+A
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
      5: f34 -> f36 : [ 0>=1+C ], cost: 1
      6: f34 -> f36 : [ C>=1 ], cost: 1
     32: f36 -> f2 : B'=1+B, D'=1+A, H'=0, [ A>=D && 1+A>=1+A ], cost: 2-D+A
     33: f36 -> [16] : D'=1+A, H'=0, [ A>=D ], cost: 1-D+A
     34: f36 -> [17] : D'=1+A, H'=0, [ A>=D ], cost: 1-D+A
     22: start -> f2 : [], cost: 1
     18: [10] -> f34 : D'=B, [ E>=1+A && B==D ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     35: f2 -> f34 : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     36: f2 -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 2-E+A
     12: f34 -> f2 : B'=1+B, C'=0, [ C==0 ], cost: 1
     37: f34 -> f2 : B'=1+B, D'=1+A, H'=0, [ 0>=1+C && A>=D && 1+A>=1+A ], cost: 3-D+A
     40: f34 -> f2 : B'=1+B, D'=1+A, H'=0, [ C>=1 && A>=D && 1+A>=1+A ], cost: 3-D+A
     38: f34 -> [16] : D'=1+A, H'=0, [ 0>=1+C && A>=D ], cost: 2-D+A
     41: f34 -> [16] : D'=1+A, H'=0, [ C>=1 && A>=D ], cost: 2-D+A
     39: f34 -> [17] : D'=1+A, H'=0, [ 0>=1+C && A>=D ], cost: 2-D+A
     42: f34 -> [17] : D'=1+A, H'=0, [ C>=1 && A>=D ], cost: 2-D+A
     22: start -> f2 : [], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     43: f2 -> f2 : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B && 0==0 ], cost: 4-E+A
     36: f2 -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 2-E+A
     44: f2 -> [19] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     45: f2 -> [20] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     46: f2 -> [21] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     47: f2 -> [22] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     48: f2 -> [23] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     49: f2 -> [24] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     22: start -> f2 : [], cost: 1

Eliminating 1 self-loops for location f2
  Removing the self-loops: 43.
Adding an epsilon transition (to model nonexecution of the loops): 51.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     50: f2 -> [25] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 4-E+A
     51: f2 -> [25] : [], cost: 0
     22: start -> f2 : [], cost: 1
     36: [25] -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 2-E+A
     44: [25] -> [19] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     45: [25] -> [20] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     46: [25] -> [21] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     47: [25] -> [22] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     48: [25] -> [23] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     49: [25] -> [24] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A


Applied chaining over branches and pruning:
  Start location: start
     52: start -> [25] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     53: start -> [25] : [], cost: 1
     36: [25] -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 2-E+A
     44: [25] -> [19] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     45: [25] -> [20] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     46: [25] -> [21] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     47: [25] -> [22] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     48: [25] -> [23] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A
     49: [25] -> [24] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 3-E+A


Applied chaining over branches and pruning:
  Start location: start
     61: start -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 3-E+A
     62: start -> [19] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     63: start -> [20] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     64: start -> [21] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     65: start -> [22] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     66: start -> [23] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     67: start -> [24] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     54: start -> [26] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     55: start -> [27] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     56: start -> [28] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     57: start -> [29] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     58: start -> [30] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     59: start -> [31] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     60: start -> [32] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start
     61: start -> [18] : C'=free_4, D'=A, E'=1+A, F'=free_3, G'=free_2, [ A>=1+B && A>=E && free_3>=1+free_2 ], cost: 3-E+A
     62: start -> [19] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     63: start -> [20] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     64: start -> [21] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     65: start -> [22] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     66: start -> [23] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     67: start -> [24] : C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 && 1+A>=1+A && B==B ], cost: 4-E+A
     54: start -> [26] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     55: start -> [27] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     56: start -> [28] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     57: start -> [29] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     58: start -> [30] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     59: start -> [31] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A
     60: start -> [32] : B'=1+B, C'=0, D'=B, E'=1+A, F'=free_1, G'=free, [ A>=1+B && A>=E && free>=free_1 ], cost: 5-E+A


Computing complexity for remaining 14 transitions.

  Found configuration with infinitely models for cost: 3-E+A
  and guard: A>=1+B && A>=E && free_3>=1+free_2:
  free_2: Pos, E: Pos, B: Pos, free_3: Pos, A: Pos, where: free_3 > free_2 A > E A > B

Found new complexity n^1, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: A>=1+B && A>=E && free_3>=1+free_2
  Final Cost:  3-E+A

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

WORST_CASE(Omega(n^1),?)