Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f2
      0: f4 -> f14 : [ 0>=A ], cost: 1
      7: f4 -> f33 : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 ], cost: 1
      8: f4 -> f33 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 ], cost: 1
      1: f13 -> f4 : [], cost: 1
      2: f13 -> f400 : [ B>=1+A ], cost: 1
      3: f2 -> f23 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 ], cost: 1
      4: f2 -> f23 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 ], cost: 1
      5: f23 -> f4 : [ E>=C ], cost: 1
      6: f23 -> f4 : F'=1, [ C>=1+E ], cost: 1
      9: f33 -> f6 : [ E>=C ], cost: 1
     10: f33 -> f6 : F'=1, [ C>=1+E ], cost: 1
     11: f6 -> f43 : C'=free_12, D'=free_13, E'=C, [ free_12>=C && 0>=C && 0>=B ], cost: 1
     12: f6 -> f43 : C'=free_14, D'=free_15, E'=C, F'=0, [ free_14>=C && 0>=C && B>=1 ], cost: 1
     15: f6 -> f53 : C'=free_16, D'=free_17, E'=-1+C, [ 1+free_16>=C && C>=1 && 0>=B ], cost: 1
     16: f6 -> f53 : C'=free_18, D'=free_19, E'=-1+C, F'=0, [ 1+free_18>=C && C>=1 && B>=1 ], cost: 1
     13: f43 -> f6 : E'=C, [ C==E ], cost: 1
     14: f43 -> f6 : F'=1, [ C>=1+E ], cost: 1
     17: f53 -> f61 : B'=A, E'=C, [ E>=C ], cost: 1
     18: f53 -> f61 : B'=A, E'=C, F'=1, [ C>=1+E ], cost: 1
     19: f61 -> f63 : C'=free_20, D'=free_21, [ 0>=B && free_20>=E ], cost: 1
     20: f61 -> f63 : C'=free_22, D'=free_23, F'=0, [ B>=1 && free_22>=E ], cost: 1
     21: f63 -> f71 : D'=1+D, E'=C, [ E>=C ], cost: 1
     22: f63 -> f71 : D'=1+D, E'=C, F'=1, [ C>=1+E ], cost: 1
     23: f71 -> f73 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E ], cost: 1
     24: f71 -> f73 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E ], cost: 1
     25: f73 -> f13 : [ E>=C ], cost: 1
     26: f73 -> f13 : F'=1, [ C>=1+E ], cost: 1


Simplified the transitions:
  Start location: f2
      7: f4 -> f33 : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 ], cost: 1
      8: f4 -> f33 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 ], cost: 1
      1: f13 -> f4 : [], cost: 1
      3: f2 -> f23 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 ], cost: 1
      4: f2 -> f23 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 ], cost: 1
      5: f23 -> f4 : [ E>=C ], cost: 1
      6: f23 -> f4 : F'=1, [ C>=1+E ], cost: 1
      9: f33 -> f6 : [ E>=C ], cost: 1
     10: f33 -> f6 : F'=1, [ C>=1+E ], cost: 1
     11: f6 -> f43 : C'=free_12, D'=free_13, E'=C, [ free_12>=C && 0>=C && 0>=B ], cost: 1
     12: f6 -> f43 : C'=free_14, D'=free_15, E'=C, F'=0, [ free_14>=C && 0>=C && B>=1 ], cost: 1
     15: f6 -> f53 : C'=free_16, D'=free_17, E'=-1+C, [ 1+free_16>=C && C>=1 && 0>=B ], cost: 1
     16: f6 -> f53 : C'=free_18, D'=free_19, E'=-1+C, F'=0, [ 1+free_18>=C && C>=1 && B>=1 ], cost: 1
     13: f43 -> f6 : E'=C, [ C==E ], cost: 1
     14: f43 -> f6 : F'=1, [ C>=1+E ], cost: 1
     17: f53 -> f61 : B'=A, E'=C, [ E>=C ], cost: 1
     18: f53 -> f61 : B'=A, E'=C, F'=1, [ C>=1+E ], cost: 1
     19: f61 -> f63 : C'=free_20, D'=free_21, [ 0>=B && free_20>=E ], cost: 1
     20: f61 -> f63 : C'=free_22, D'=free_23, F'=0, [ B>=1 && free_22>=E ], cost: 1
     21: f63 -> f71 : D'=1+D, E'=C, [ E>=C ], cost: 1
     22: f63 -> f71 : D'=1+D, E'=C, F'=1, [ C>=1+E ], cost: 1
     23: f71 -> f73 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E ], cost: 1
     24: f71 -> f73 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E ], cost: 1
     25: f73 -> f13 : [ E>=C ], cost: 1
     26: f73 -> f13 : F'=1, [ C>=1+E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
     31: f4 -> f6 : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 ], cost: 2
     32: f4 -> f6 : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C ], cost: 2
     33: f4 -> f6 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 ], cost: 2
     34: f4 -> f6 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C ], cost: 2
      1: f13 -> f4 : [], cost: 1
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     35: f6 -> f6 : C'=free_12, D'=free_13, E'=free_12, [ free_12>=C && 0>=C && 0>=B && free_12==C ], cost: 2
     36: f6 -> f6 : C'=free_12, D'=free_13, E'=C, F'=1, [ free_12>=C && 0>=C && 0>=B && free_12>=1+C ], cost: 2
     37: f6 -> f6 : C'=free_14, D'=free_15, E'=free_14, F'=0, [ free_14>=C && 0>=C && B>=1 && free_14==C ], cost: 2
     38: f6 -> f6 : C'=free_14, D'=free_15, E'=C, F'=1, [ free_14>=C && 0>=C && B>=1 && free_14>=1+C ], cost: 2
     39: f6 -> f61 : B'=A, C'=free_16, D'=free_17, E'=free_16, [ 1+free_16>=C && C>=1 && 0>=B && -1+C>=free_16 ], cost: 2
     40: f6 -> f61 : B'=A, C'=free_16, D'=free_17, E'=free_16, F'=1, [ 1+free_16>=C && C>=1 && 0>=B && free_16>=C ], cost: 2
     41: f6 -> f61 : B'=A, C'=free_18, D'=free_19, E'=free_18, F'=0, [ 1+free_18>=C && C>=1 && B>=1 && -1+C>=free_18 ], cost: 2
     42: f6 -> f61 : B'=A, C'=free_18, D'=free_19, E'=free_18, F'=1, [ 1+free_18>=C && C>=1 && B>=1 && free_18>=C ], cost: 2
     43: f61 -> f71 : C'=free_20, D'=1+free_21, E'=free_20, [ 0>=B && free_20>=E && E>=free_20 ], cost: 2
     44: f61 -> f71 : C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ 0>=B && free_20>=E && free_20>=1+E ], cost: 2
     45: f61 -> f71 : C'=free_22, D'=1+free_23, E'=free_22, F'=0, [ B>=1 && free_22>=E && E>=free_22 ], cost: 2
     46: f61 -> f71 : C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ B>=1 && free_22>=E && free_22>=1+E ], cost: 2
     47: f71 -> f13 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E && E>=free_24 ], cost: 2
     48: f71 -> f13 : C'=free_24, D'=free_25, F'=1, [ 0>=B && free_24>=E && free_24>=1+E ], cost: 2
     49: f71 -> f13 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E && E>=free_26 ], cost: 2
     50: f71 -> f13 : C'=free_26, D'=free_27, F'=1, [ B>=1 && free_26>=E && free_26>=1+E ], cost: 2

Eliminating 4 self-loops for location f6
  Self-Loop 35 has unbounded runtime, resulting in the new transition 51.
  Self-Loop 36 has the metering function: 1-C, resulting in the new transition 52.
  Self-Loop 37 has unbounded runtime, resulting in the new transition 53.
  Self-Loop 38 has the metering function: 1-C, resulting in the new transition 54.
  Removing the self-loops: 35 36 37 38.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
     31: f4 -> f6 : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 ], cost: 2
     32: f4 -> f6 : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C ], cost: 2
     33: f4 -> f6 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 ], cost: 2
     34: f4 -> f6 : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C ], cost: 2
      1: f13 -> f4 : [], cost: 1
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     51: f6 -> [14] : [ 0>=C && 0>=B ], cost: INF
     52: f6 -> [14] : C'=1, D'=free_13, E'=0, F'=1, [ 0>=C && 0>=B && 1+C>=1+C ], cost: 2-2*C
     53: f6 -> [14] : [ 0>=C && B>=1 ], cost: INF
     54: f6 -> [14] : C'=1, D'=free_15, E'=0, F'=1, [ 0>=C && B>=1 && 1+C>=1+C ], cost: 2-2*C
     43: f61 -> f71 : C'=free_20, D'=1+free_21, E'=free_20, [ 0>=B && free_20>=E && E>=free_20 ], cost: 2
     44: f61 -> f71 : C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ 0>=B && free_20>=E && free_20>=1+E ], cost: 2
     45: f61 -> f71 : C'=free_22, D'=1+free_23, E'=free_22, F'=0, [ B>=1 && free_22>=E && E>=free_22 ], cost: 2
     46: f61 -> f71 : C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ B>=1 && free_22>=E && free_22>=1+E ], cost: 2
     47: f71 -> f13 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E && E>=free_24 ], cost: 2
     48: f71 -> f13 : C'=free_24, D'=free_25, F'=1, [ 0>=B && free_24>=E && free_24>=1+E ], cost: 2
     49: f71 -> f13 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E && E>=free_26 ], cost: 2
     50: f71 -> f13 : C'=free_26, D'=free_27, F'=1, [ B>=1 && free_26>=E && free_26>=1+E ], cost: 2
     39: [14] -> f61 : B'=A, C'=free_16, D'=free_17, E'=free_16, [ 1+free_16>=C && C>=1 && 0>=B && -1+C>=free_16 ], cost: 2
     40: [14] -> f61 : B'=A, C'=free_16, D'=free_17, E'=free_16, F'=1, [ 1+free_16>=C && C>=1 && 0>=B && free_16>=C ], cost: 2
     41: [14] -> f61 : B'=A, C'=free_18, D'=free_19, E'=free_18, F'=0, [ 1+free_18>=C && C>=1 && B>=1 && -1+C>=free_18 ], cost: 2
     42: [14] -> f61 : B'=A, C'=free_18, D'=free_19, E'=free_18, F'=1, [ 1+free_18>=C && C>=1 && B>=1 && free_18>=C ], cost: 2


Applied chaining over branches and pruning:
  Start location: f2
     55: f4 -> [14] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     56: f4 -> [14] : A'=-1+A, C'=1, D'=free_13, E'=0, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 ], cost: 4-2*free_8
     57: f4 -> [14] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     59: f4 -> [14] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
     61: f4 -> [14] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     79: f71 -> f4 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E && E>=free_24 ], cost: 3
     80: f71 -> f4 : C'=free_24, D'=free_25, F'=1, [ 0>=B && free_24>=E && free_24>=1+E ], cost: 3
     81: f71 -> f4 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E && E>=free_26 ], cost: 3
     82: f71 -> f4 : C'=free_26, D'=free_27, F'=1, [ B>=1 && free_26>=E && free_26>=1+E ], cost: 3
     63: [14] -> f71 : B'=A, C'=free_20, D'=1+free_21, E'=free_20, [ 1+free_16>=C && C>=1 && 0>=B && -1+C>=free_16 && 0>=A && free_20>=free_16 && free_16>=free_20 ], cost: 4
     64: [14] -> f71 : B'=A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ 1+free_16>=C && C>=1 && 0>=B && -1+C>=free_16 && 0>=A && free_20>=free_16 && free_20>=1+free_16 ], cost: 4
     66: [14] -> f71 : B'=A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ 1+free_16>=C && C>=1 && 0>=B && -1+C>=free_16 && A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 4
     70: [14] -> f71 : B'=A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ 1+free_16>=C && C>=1 && 0>=B && free_16>=C && A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 4
     72: [14] -> f71 : B'=A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ 1+free_18>=C && C>=1 && B>=1 && -1+C>=free_18 && 0>=A && free_20>=free_18 && free_20>=1+free_18 ], cost: 4


Applied chaining over branches and pruning:
  Start location: f2
     88: f4 -> f71 : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
     89: f4 -> f71 : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
     90: f4 -> f71 : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
     91: f4 -> f71 : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
     83: f4 -> [15] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     84: f4 -> [16] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     85: f4 -> [17] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     86: f4 -> [18] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     87: f4 -> [19] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     92: f4 -> [20] : A'=-1+A, C'=1, D'=free_13, E'=0, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 ], cost: 4-2*free_8
     93: f4 -> [21] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     94: f4 -> [22] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     95: f4 -> [23] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     96: f4 -> [24] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     97: f4 -> [25] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     98: f4 -> [26] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
     99: f4 -> [27] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    100: f4 -> [28] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    101: f4 -> [29] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    102: f4 -> [30] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    103: f4 -> [31] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    104: f4 -> [32] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    105: f4 -> [33] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    106: f4 -> [34] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    107: f4 -> [35] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     79: f71 -> f4 : C'=free_24, D'=free_25, [ 0>=B && free_24>=E && E>=free_24 ], cost: 3
     80: f71 -> f4 : C'=free_24, D'=free_25, F'=1, [ 0>=B && free_24>=E && free_24>=1+E ], cost: 3
     81: f71 -> f4 : C'=free_26, D'=free_27, F'=0, [ B>=1 && free_26>=E && E>=free_26 ], cost: 3
     82: f71 -> f4 : C'=free_26, D'=free_27, F'=1, [ B>=1 && free_26>=E && free_26>=1+E ], cost: 3


Applied chaining over branches and pruning:
  Start location: f2
    108: f4 -> f4 : A'=-1+A, B'=-1+A, C'=free_24, D'=free_25, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 && 0>=-1+A && free_24>=free_20 && free_20>=free_24 ], cost: 11-2*free_8
    109: f4 -> f4 : A'=-1+A, B'=-1+A, C'=free_24, D'=free_25, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 && 0>=-1+A && free_24>=free_20 && free_24>=1+free_20 ], cost: 11-2*free_8
    113: f4 -> f4 : A'=-1+A, B'=-1+A, C'=free_24, D'=free_25, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 && 0>=-1+A && free_24>=free_20 && free_24>=1+free_20 ], cost: 11-2*free_8
    118: f4 -> f4 : A'=-1+A, B'=-1+A, C'=free_26, D'=free_27, E'=free_22, F'=0, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 && -1+A>=1 && free_26>=free_22 && free_22>=free_26 ], cost: 11-2*free_8
    119: f4 -> f4 : A'=-1+A, B'=-1+A, C'=free_26, D'=free_27, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 && -1+A>=1 && free_26>=free_22 && free_26>=1+free_22 ], cost: 11-2*free_8
     83: f4 -> [15] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     84: f4 -> [16] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     85: f4 -> [17] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     86: f4 -> [18] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     87: f4 -> [19] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     92: f4 -> [20] : A'=-1+A, C'=1, D'=free_13, E'=0, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 ], cost: 4-2*free_8
     93: f4 -> [21] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     94: f4 -> [22] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     95: f4 -> [23] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     96: f4 -> [24] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     97: f4 -> [25] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     98: f4 -> [26] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
     99: f4 -> [27] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    100: f4 -> [28] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    101: f4 -> [29] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    102: f4 -> [30] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    103: f4 -> [31] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    104: f4 -> [32] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    105: f4 -> [33] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    106: f4 -> [34] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    107: f4 -> [35] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    110: f4 -> [36] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    111: f4 -> [37] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    114: f4 -> [38] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    115: f4 -> [39] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    116: f4 -> [40] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    117: f4 -> [41] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    120: f4 -> [42] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    121: f4 -> [43] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2

Eliminating 5 self-loops for location f4
  Self-Loop 108 has the metering function: A, resulting in the new transition 124.
  Self-Loop 109 has the metering function: -1+A, resulting in the new transition 125.
  Self-Loop 113 has the metering function: -1+A, resulting in the new transition 126.
  Removing the self-loops: 108 109 113 118 119.
Adding an epsilon transition (to model nonexecution of the loops): 129.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
    124: f4 -> [44] : A'=0, B'=0, C'=0, D'=free_25, E'=0, F'=1, [ 0>=B && 1-A==0 && 0>=C ], cost: 11*A
    125: f4 -> [44] : A'=1, B'=1, C'=free_24, D'=free_25, E'=0, F'=1, [ 0>=B && 1-A==0 && 0>=C && free_24>=1 ], cost: -11-2*free_24*(-1+A)+11*A
    126: f4 -> [44] : A'=1, B'=1, C'=free_24, D'=free_25, E'=free_20, F'=1, [ 0>=B && 1-A==0 && 0>=C && free_20>=1 && free_24>=1+free_20 ], cost: -11-2*free_24*(-1+A)+11*A
    127: f4 -> [44] : A'=-1+A, B'=-1+A, C'=free_22, D'=free_27, E'=free_22, F'=0, [ 0>=B && 0>=C && -1+A>=1 && free_22>=1 ], cost: 11-2*C
    128: f4 -> [44] : A'=-1+A, B'=-1+A, C'=free_26, D'=free_27, E'=free_22, F'=1, [ 0>=B && 0>=C && -1+A>=1 && free_22>=1 && free_26>=1+free_22 ], cost: 11-2*C
    129: f4 -> [44] : [], cost: 0
     27: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
     28: f2 -> f4 : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
     29: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
     30: f2 -> f4 : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     83: [44] -> [15] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     84: [44] -> [16] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     85: [44] -> [17] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     86: [44] -> [18] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     87: [44] -> [19] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     92: [44] -> [20] : A'=-1+A, C'=1, D'=free_13, E'=0, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 ], cost: 4-2*free_8
     93: [44] -> [21] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     94: [44] -> [22] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     95: [44] -> [23] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     96: [44] -> [24] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     97: [44] -> [25] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     98: [44] -> [26] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
     99: [44] -> [27] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    100: [44] -> [28] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    101: [44] -> [29] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    102: [44] -> [30] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    103: [44] -> [31] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    104: [44] -> [32] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    105: [44] -> [33] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    106: [44] -> [34] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    107: [44] -> [35] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    110: [44] -> [36] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    111: [44] -> [37] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    114: [44] -> [38] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    115: [44] -> [39] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    116: [44] -> [40] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    117: [44] -> [41] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    120: [44] -> [42] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    121: [44] -> [43] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8


Applied chaining over branches and pruning:
  Start location: f2
    130: f2 -> [44] : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, [ free_3>=1 && free>=1 && 0>=free_1 && 1>=free ], cost: 2
    131: f2 -> [44] : A'=free_3, B'=free_1, C'=free, D'=free_2, E'=1, F'=1, [ free_3>=1 && free>=1 && 0>=free_1 && free>=2 ], cost: 2
    132: f2 -> [44] : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=0, [ free_7>=1 && free_4>=1 && free_5>=1 && 1>=free_4 ], cost: 2
    133: f2 -> [44] : A'=free_7, B'=free_5, C'=free_4, D'=free_6, E'=1, F'=1, [ free_7>=1 && free_4>=1 && free_5>=1 && free_4>=2 ], cost: 2
     83: [44] -> [15] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     84: [44] -> [16] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     85: [44] -> [17] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     86: [44] -> [18] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     87: [44] -> [19] : A'=-1+A, C'=free_8, D'=free_9, E'=C, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B ], cost: INF
     92: [44] -> [20] : A'=-1+A, C'=1, D'=free_13, E'=0, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 ], cost: 4-2*free_8
     93: [44] -> [21] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     94: [44] -> [22] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     95: [44] -> [23] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     96: [44] -> [24] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     97: [44] -> [25] : A'=-1+A, C'=free_8, D'=free_9, E'=C, F'=1, [ free_8>=C && 0>=B && A>=1 && free_8>=1+C && 0>=free_8 && 0>=B ], cost: INF
     98: [44] -> [26] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
     99: [44] -> [27] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    100: [44] -> [28] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    101: [44] -> [29] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    102: [44] -> [30] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=0, [ free_10>=C && B>=1 && A>=1 && C>=free_10 && 0>=free_10 && B>=1 ], cost: INF
    103: [44] -> [31] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    104: [44] -> [32] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    105: [44] -> [33] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    106: [44] -> [34] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    107: [44] -> [35] : A'=-1+A, C'=free_10, D'=free_11, E'=C, F'=1, [ free_10>=C && B>=1 && A>=1 && free_10>=1+C && 0>=free_10 && B>=1 ], cost: INF
    110: [44] -> [36] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    111: [44] -> [37] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_16>=free_20 ], cost: 8-2*free_8
    114: [44] -> [38] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    115: [44] -> [39] : A'=-1+A, B'=-1+A, C'=free_20, D'=1+free_21, E'=free_20, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && 0>=-1+A && free_20>=free_16 && free_20>=1+free_16 ], cost: 8-2*free_8
    116: [44] -> [40] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    117: [44] -> [41] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && 0>=free_16 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    120: [44] -> [42] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8
    121: [44] -> [43] : A'=-1+A, B'=-1+A, C'=free_22, D'=1+free_23, E'=free_22, F'=1, [ free_8>=C && 0>=B && A>=1 && C>=free_8 && 0>=free_8 && 0>=B && 1+free_8>=1+free_8 && 1+free_16>=1 && 1>=1 && 0>=B && free_16>=1 && -1+A>=1 && free_22>=free_16 && free_22>=1+free_16 ], cost: 8-2*free_8


Applied chaining over branches and pruning:
  Start location: f2
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f2
    <empty>


Computing complexity for remaining 0 transitions.


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