Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
      1: f16 -> f25 : E'=1+E, Q'=0, [ H>=1 && 0>=E && 0>=D ], cost: 1
      2: f16 -> f25 : Q'=free_4, [ H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 ], cost: 1
      3: f16 -> f25 : B'=1+B, Q'=1, [ H>=1 && 0>=D && 0>=B && E==1 ], cost: 1
      4: f16 -> f25 : B'=0, C'=-1+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 ], cost: 1
      5: f16 -> f25 : A'=1+A, B'=0, C'=1+A, D'=free_5, E'=0, Q'=free_6, [ H>=1 && 0>=D && free_6>=0 && 1>=free_6 && B>=2 && free_5>=0 && E==1 ], cost: 1
      6: f16 -> f25 : A'=1+A, B'=0, C'=1+A, D'=free_7, E'=0, Q'=free_8, [ H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && E==1 && B==1 ], cost: 1
      7: f16 -> f25 : D'=-1+D, Q'=free_9, [ H>=1 && D>=1 && 1>=free_9 && free_9>=0 ], cost: 1
     19: f16 -> f74 : [ 0>=H ], cost: 1
     15: f25 -> f16 : [ 1+F>=A && 0>=Q ], cost: 1
      8: f25 -> f50 : E'=1+E, J'=0, [ Q>=1 && 0>=E && 0>=D ], cost: 1
      9: f25 -> f50 : J'=free_10, [ Q>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 ], cost: 1
     10: f25 -> f50 : B'=1+B, J'=1, [ Q>=1 && 0>=D && 0>=B && E==1 ], cost: 1
     11: f25 -> f50 : B'=0, C'=-1+C, J'=0, [ Q>=1 && 0>=D && C>=1 && E==1 && B==1 ], cost: 1
     12: f25 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_11, E'=0, J'=free_12, [ Q>=1 && 0>=D && free_12>=0 && 1>=free_12 && B>=2 && free_11>=0 && E==1 ], cost: 1
     13: f25 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, J'=free_14, [ Q>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && E==1 && B==1 ], cost: 1
     14: f25 -> f50 : D'=-1+D, J'=free_15, [ Q>=1 && D>=1 && 1>=free_15 && free_15>=0 ], cost: 1
     16: f50 -> f16 : [ J>=1 && 1+F>=A && H>=G ], cost: 1
     17: f50 -> f16 : H'=1+H, [ J>=1 && 1+F>=A && G>=1+H ], cost: 1
     18: f50 -> f16 : H'=-1+H, [ 1+F>=A && 0>=J ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
      1: f16 -> f25 : E'=1+E, Q'=0, [ H>=1 && 0>=E && 0>=D ], cost: 1
      2: f16 -> f25 : Q'=free_4, [ H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 ], cost: 1
      3: f16 -> f25 : B'=1+B, Q'=1, [ H>=1 && 0>=D && 0>=B && E==1 ], cost: 1
      4: f16 -> f25 : B'=0, C'=-1+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 ], cost: 1
      5: f16 -> f25 : A'=1+A, B'=0, C'=1+A, D'=free_5, E'=0, Q'=free_6, [ H>=1 && 0>=D && free_6>=0 && 1>=free_6 && B>=2 && free_5>=0 && E==1 ], cost: 1
      6: f16 -> f25 : A'=1+A, B'=0, C'=1+A, D'=free_7, E'=0, Q'=free_8, [ H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && E==1 && B==1 ], cost: 1
      7: f16 -> f25 : D'=-1+D, Q'=free_9, [ H>=1 && D>=1 && 1>=free_9 && free_9>=0 ], cost: 1
     15: f25 -> f16 : [ 1+F>=A && 0>=Q ], cost: 1
      8: f25 -> f50 : E'=1+E, J'=0, [ Q>=1 && 0>=E && 0>=D ], cost: 1
      9: f25 -> f50 : J'=free_10, [ Q>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 ], cost: 1
     10: f25 -> f50 : B'=1+B, J'=1, [ Q>=1 && 0>=D && 0>=B && E==1 ], cost: 1
     11: f25 -> f50 : B'=0, C'=-1+C, J'=0, [ Q>=1 && 0>=D && C>=1 && E==1 && B==1 ], cost: 1
     12: f25 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_11, E'=0, J'=free_12, [ Q>=1 && 0>=D && free_12>=0 && 1>=free_12 && B>=2 && free_11>=0 && E==1 ], cost: 1
     13: f25 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, J'=free_14, [ Q>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && E==1 && B==1 ], cost: 1
     14: f25 -> f50 : D'=-1+D, J'=free_15, [ Q>=1 && D>=1 && 1>=free_15 && free_15>=0 ], cost: 1
     16: f50 -> f16 : [ J>=1 && 1+F>=A && H>=G ], cost: 1
     17: f50 -> f16 : H'=1+H, [ J>=1 && 1+F>=A && G>=1+H ], cost: 1
     18: f50 -> f16 : H'=-1+H, [ 1+F>=A && 0>=J ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     20: f16 -> f16 : E'=1+E, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A && 0>=0 ], cost: 2
     21: f16 -> f16 : Q'=free_4, [ H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && 1+F>=A && 0>=free_4 ], cost: 2
     26: f16 -> f16 : B'=0, C'=-1+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A && 0>=0 ], cost: 2
     27: f16 -> f16 : A'=1+A, B'=0, C'=1+A, D'=free_5, E'=0, Q'=free_6, [ H>=1 && 0>=D && free_6>=0 && 1>=free_6 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && 0>=free_6 ], cost: 2
     33: f16 -> f16 : D'=-1+D, Q'=free_9, [ H>=1 && D>=1 && 1>=free_9 && free_9>=0 && 1+F>=A && 0>=free_9 ], cost: 2
     22: f16 -> f50 : Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 ], cost: 2
     23: f16 -> f50 : B'=2+B, Q'=1, J'=1, [ H>=1 && 0>=D && 0>=B && E==1 && 1>=1 && 0>=D && 0>=1+B && E==1 ], cost: 2
     25: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=free_14, [ H>=1 && 0>=D && 0>=B && E==1 && 1>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && E==1 && 1+B==1 ], cost: 2
     32: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=-1+free_7, E'=0, Q'=free_8, J'=free_15, [ H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && E==1 && B==1 && free_8>=1 && free_7>=1 && 1>=free_15 && free_15>=0 ], cost: 2
     34: f16 -> f50 : D'=-1+D, E'=1+E, Q'=free_9, J'=0, [ H>=1 && D>=1 && 1>=free_9 && free_9>=0 && free_9>=1 && 0>=E && 0>=-1+D ], cost: 2
     16: f50 -> f16 : [ J>=1 && 1+F>=A && H>=G ], cost: 1
     17: f50 -> f16 : H'=1+H, [ J>=1 && 1+F>=A && G>=1+H ], cost: 1
     18: f50 -> f16 : H'=-1+H, [ 1+F>=A && 0>=J ], cost: 1

Eliminating 5 self-loops for location f16
  Self-Loop 20 has the metering function: 1-E, resulting in the new transition 41.
  Self-Loop 21 has unbounded runtime, resulting in the new transition 42.
  Self-Loop 26 has the metering function: -1+B, resulting in the new transition 43.
  Self-Loop 27 has the metering function: -1+E, resulting in the new transition 44.
  Self-Loop 33 has the metering function: D, resulting in the new transition 45.
  Found this metering function when nesting loops: -1+D,
  Found this metering function when nesting loops: meter,
  Found this metering function when nesting loops: meter_1,
  Found this metering function when nesting loops: -1+E,
  Found this metering function when nesting loops: -1+E,
  Found this metering function when nesting loops: -1+E,
  and nested parallel self-loops 27 (outer loop) and 45 (inner loop), obtaining the new transitions: 46.
  Found this metering function when nesting loops: -1+E,
  and nested parallel self-loops 27 (outer loop) and 45 (inner loop), obtaining the new transitions: 47, 48.
  Found this metering function when nesting loops: -1+E,
  Found this metering function when nesting loops: -1+E,
  Found this metering function when nesting loops: meter_2,
  Found this metering function when nesting loops: -1+E,
  Removing the self-loops: 20 21 26 27 33.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     41: f16 -> [5] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     42: f16 -> [5] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     43: f16 -> [5] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     44: f16 -> [5] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     45: f16 -> [5] : D'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A ], cost: 2*D
     46: f16 -> [5] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     47: f16 -> [5] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     48: f16 -> [5] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     16: f50 -> f16 : [ J>=1 && 1+F>=A && H>=G ], cost: 1
     17: f50 -> f16 : H'=1+H, [ J>=1 && 1+F>=A && G>=1+H ], cost: 1
     18: f50 -> f16 : H'=-1+H, [ 1+F>=A && 0>=J ], cost: 1
     22: [5] -> f50 : Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 ], cost: 2
     23: [5] -> f50 : B'=2+B, Q'=1, J'=1, [ H>=1 && 0>=D && 0>=B && E==1 && 1>=1 && 0>=D && 0>=1+B && E==1 ], cost: 2
     25: [5] -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=free_14, [ H>=1 && 0>=D && 0>=B && E==1 && 1>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && E==1 && 1+B==1 ], cost: 2
     32: [5] -> f50 : A'=1+A, B'=0, C'=1+A, D'=-1+free_7, E'=0, Q'=free_8, J'=free_15, [ H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && E==1 && B==1 && free_8>=1 && free_7>=1 && 1>=free_15 && free_15>=0 ], cost: 2
     34: [5] -> f50 : D'=-1+D, E'=1+E, Q'=free_9, J'=0, [ H>=1 && D>=1 && 1>=free_9 && free_9>=0 && free_9>=1 && 0>=E && 0>=-1+D ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     51: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=free_14, [ H>=1 && 0>=E && 0>=D && 1+F>=A && H>=1 && 0>=D && 0>=B && 1==1 && 1>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && 1==1 && 1+B==1 ], cost: 4-2*E
     52: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=-1+free_7, E'=0, Q'=free_8, J'=free_15, [ H>=1 && 0>=E && 0>=D && 1+F>=A && H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && 1==1 && B==1 && free_8>=1 && free_7>=1 && 1>=free_15 && free_15>=0 ], cost: 4-2*E
     54: f16 -> f50 : Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 ], cost: INF
     71: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=free_14, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && 0>=B && E==1 && 1>=1 && 0>=0 && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && E==1 && 1+B==1 ], cost: 2+2*D
     72: f16 -> f50 : A'=1+A, B'=0, C'=1+A, D'=-1+free_7, E'=0, Q'=free_8, J'=free_15, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && E==1 && B==1 && free_8>=1 && free_7>=1 && 1>=free_15 && free_15>=0 ], cost: 2+2*D
     49: f16 -> [6] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     53: f16 -> [7] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     55: f16 -> [8] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     56: f16 -> [9] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     57: f16 -> [10] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     58: f16 -> [11] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     59: f16 -> [12] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     60: f16 -> [13] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     61: f16 -> [14] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     62: f16 -> [15] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     63: f16 -> [16] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     64: f16 -> [17] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     65: f16 -> [18] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     66: f16 -> [19] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     67: f16 -> [20] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     73: f16 -> [21] : D'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A ], cost: 2*D
     74: f16 -> [22] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     75: f16 -> [23] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     76: f16 -> [24] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     77: f16 -> [25] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     79: f16 -> [26] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     80: f16 -> [27] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     81: f16 -> [28] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     82: f16 -> [29] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     83: f16 -> [30] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     84: f16 -> [31] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     85: f16 -> [32] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     86: f16 -> [33] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     87: f16 -> [34] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     88: f16 -> [35] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     16: f50 -> f16 : [ J>=1 && 1+F>=A && H>=G ], cost: 1
     17: f50 -> f16 : H'=1+H, [ J>=1 && 1+F>=A && G>=1+H ], cost: 1
     18: f50 -> f16 : H'=-1+H, [ 1+F>=A && 0>=J ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     89: f16 -> f16 : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=free_14, [ H>=1 && 0>=E && 0>=D && 1+F>=A && H>=1 && 0>=D && 0>=B && 1==1 && 1>=1 && 0>=D && 0>=C && free_14>=0 && 1>=free_14 && free_13>=0 && 1==1 && 1+B==1 && free_14>=1 && 1+F>=1+A && H>=G ], cost: 5-2*E
     92: f16 -> f16 : A'=1+A, B'=0, C'=1+A, D'=-1+free_7, E'=0, Q'=free_8, J'=free_15, [ H>=1 && 0>=E && 0>=D && 1+F>=A && H>=1 && 0>=D && 0>=C && free_8>=0 && 1>=free_8 && free_7>=0 && 1==1 && B==1 && free_8>=1 && free_7>=1 && 1>=free_15 && free_15>=0 && free_15>=1 && 1+F>=1+A && H>=G ], cost: 5-2*E
     95: f16 -> f16 : Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && free_10>=1 && 1+F>=A && H>=G ], cost: INF
     96: f16 -> f16 : H'=1+H, Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && free_10>=1 && 1+F>=A && G>=1+H ], cost: INF
     97: f16 -> f16 : H'=-1+H, Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && 1+F>=A && 0>=free_10 ], cost: INF
     49: f16 -> [6] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     53: f16 -> [7] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     55: f16 -> [8] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     56: f16 -> [9] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     57: f16 -> [10] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     58: f16 -> [11] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     59: f16 -> [12] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     60: f16 -> [13] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     61: f16 -> [14] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     62: f16 -> [15] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     63: f16 -> [16] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     64: f16 -> [17] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     65: f16 -> [18] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     66: f16 -> [19] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     67: f16 -> [20] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     73: f16 -> [21] : D'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A ], cost: 2*D
     74: f16 -> [22] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     75: f16 -> [23] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     76: f16 -> [24] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     77: f16 -> [25] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     79: f16 -> [26] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     80: f16 -> [27] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     81: f16 -> [28] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     82: f16 -> [29] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     83: f16 -> [30] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     84: f16 -> [31] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     85: f16 -> [32] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     86: f16 -> [33] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     87: f16 -> [34] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     88: f16 -> [35] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D

Eliminating 5 self-loops for location f16
  Self-Loop 92 has the metering function: -1+B, resulting in the new transition 105.
  Found this metering function when nesting loops: -1+B,
  Removing the self-loops: 89 92 95 96 97.
Adding an epsilon transition (to model nonexecution of the loops): 109.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f16 : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
    104: f16 -> [36] : A'=1+A, B'=0, C'=1+A, D'=free_13, E'=0, Q'=1, J'=1, [ H>=1 && 0>=E && 0>=D && 0>=C && free_13>=0 && 1+B==1 && 1+F>=1+A && H>=G ], cost: 5-2*E
    105: f16 -> [36] : A'=-1+B+A, B'=0, C'=-1+B+A, D'=-1+free_7, E'=0, Q'=1, J'=1, [ H>=1 && 0>=E && 0>=D && 0>=C && B==1 && free_7>=1 && 1+F>=1+A && H>=G ], cost: -5+5*B
    106: f16 -> [36] : Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && free_10>=1 && 1+F>=A && H>=G ], cost: INF
    107: f16 -> [36] : H'=1+H, Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && free_10>=1 && 1+F>=A && G>=1+H ], cost: INF
    108: f16 -> [36] : H'=-1+H, Q'=free_4, J'=free_10, [ H>=1 && E>=2 && 0>=D && 1+F>=A && H>=1 && E>=2 && 0>=D && 1>=free_4 && free_4>=0 && free_4>=1 && E>=2 && 0>=D && 1>=free_10 && free_10>=0 && 1+F>=A && 0>=free_10 ], cost: INF
    109: f16 -> [36] : [], cost: 0
     49: [36] -> [6] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     53: [36] -> [7] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     55: [36] -> [8] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     56: [36] -> [9] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     57: [36] -> [10] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     58: [36] -> [11] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     59: [36] -> [12] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     60: [36] -> [13] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     61: [36] -> [14] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     62: [36] -> [15] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     63: [36] -> [16] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     64: [36] -> [17] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     65: [36] -> [18] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     66: [36] -> [19] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     67: [36] -> [20] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     73: [36] -> [21] : D'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A ], cost: 2*D
     74: [36] -> [22] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     75: [36] -> [23] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     76: [36] -> [24] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     77: [36] -> [25] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     79: [36] -> [26] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     80: [36] -> [27] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     81: [36] -> [28] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     82: [36] -> [29] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     83: [36] -> [30] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     84: [36] -> [31] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     85: [36] -> [32] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     86: [36] -> [33] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     87: [36] -> [34] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     88: [36] -> [35] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D


Applied chaining over branches and pruning:
  Start location: f0
    110: f0 -> [36] : A'=1, B'=0, C'=1, D'=free_1, E'=0, F'=free_3, G'=free_2, H'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     49: [36] -> [6] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     53: [36] -> [7] : E'=1, Q'=0, [ H>=1 && 0>=E && 0>=D && 1+F>=A ], cost: 2-2*E
     55: [36] -> [8] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     56: [36] -> [9] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     57: [36] -> [10] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     58: [36] -> [11] : [ H>=1 && E>=2 && 0>=D && 1+F>=A ], cost: INF
     59: [36] -> [12] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     60: [36] -> [13] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     61: [36] -> [14] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     62: [36] -> [15] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     63: [36] -> [16] : B'=0, C'=1-B+C, Q'=0, [ H>=1 && 0>=D && C>=1 && E==1 && B==1 && 1+F>=A ], cost: -2+2*B
     64: [36] -> [17] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     65: [36] -> [18] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     66: [36] -> [19] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     67: [36] -> [20] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E
     73: [36] -> [21] : D'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A ], cost: 2*D
     74: [36] -> [22] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     75: [36] -> [23] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     76: [36] -> [24] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     77: [36] -> [25] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=free_5, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     79: [36] -> [26] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     80: [36] -> [27] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     81: [36] -> [28] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     82: [36] -> [29] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     83: [36] -> [30] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && 0>=D && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5
     84: [36] -> [31] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     85: [36] -> [32] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     86: [36] -> [33] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     87: [36] -> [34] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D
     88: [36] -> [35] : A'=-1+E+A, B'=0, C'=-1+E+A, D'=0, E'=0, Q'=0, [ H>=1 && D>=1 && 1+F>=A && H>=1 && 0>=0 && B>=2 && free_5>=0 && E==1 && 1+F>=1+A && H>=1 && free_5>=1 && 1+F>=1+A ], cost: -2+2*E+2*(-1+E)*free_5+2*D


Applied chaining over branches and pruning:
  Start location: f0
    113: f0 -> [21] : A'=1, B'=0, C'=1, D'=0, E'=0, F'=free_3, G'=free_2, H'=free, Q'=0, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=1 && 1+free_3>=1 ], cost: 1+2*free_1


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    113: f0 -> [21] : A'=1, B'=0, C'=1, D'=0, E'=0, F'=free_3, G'=free_2, H'=free, Q'=0, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=1 && 1+free_3>=1 ], cost: 1+2*free_1


Computing complexity for remaining 1 transitions.

  Found configuration with infinitely models for cost: 1+2*free_1
  and guard: free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=1 && 1+free_3>=1:
  free_2: Pos, free_3: Pos, free: Pos, free_1: Pos, where: free_2 > free free_3 > free_2

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=1 && 1+free_3>=1
  Final Cost:  1+2*free_1

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

WORST_CASE(INF,?)