Trying to load file: main.koat

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


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


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

Eliminating 5 self-loops for location f16
  Self-Loop 20 has the metering function: 1-F, 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+C, resulting in the new transition 43.
  Self-Loop 27 has the metering function: -1+F, resulting in the new transition 44.
  Self-Loop 33 has the metering function: E, resulting in the new transition 45.
  Found this metering function when nesting loops: -1+E,
  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+F,
  Found this metering function when nesting loops: -1+F,
  Found this metering function when nesting loops: -1+F,
  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+F,
  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+F,
  Found this metering function when nesting loops: -1+F,
  Found this metering function when nesting loops: meter_2,
  Found this metering function when nesting loops: -1+F,
  Removing the self-loops: 20 21 26 27 33.

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


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


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

Eliminating 5 self-loops for location f16
  Self-Loop 92 has the metering function: -1+C, resulting in the new transition 105.
  Found this metering function when nesting loops: -1+C,
  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
    104: f16 -> [36] : A'=1, B'=1+B, C'=0, D'=1+B, E'=free_13, F'=0, J'=1, [ Q>=1 && 0>=F && 0>=E && 0>=D && free_13>=0 && 1+C==1 && Q>=H ], cost: 5-2*F
    105: f16 -> [36] : A'=1, B'=-1+B+C, C'=0, D'=-1+B+C, E'=-1+free_7, F'=0, J'=1, [ Q>=1 && 0>=F && 0>=E && 0>=D && C==1 && free_7>=1 && Q>=H ], cost: -5+5*C
    106: f16 -> [36] : A'=free_4, J'=free_10, [ Q>=1 && F>=2 && 0>=E && Q>=1 && F>=2 && 0>=E && 1>=free_4 && free_4>=0 && free_4>=1 && F>=2 && 0>=E && 1>=free_10 && free_10>=0 && Q>=H && free_10>=1 ], cost: INF
    107: f16 -> [36] : A'=free_4, Q'=1+Q, J'=free_10, [ Q>=1 && F>=2 && 0>=E && Q>=1 && F>=2 && 0>=E && 1>=free_4 && free_4>=0 && free_4>=1 && F>=2 && 0>=E && 1>=free_10 && free_10>=0 && H>=1+Q && free_10>=1 ], cost: INF
    108: f16 -> [36] : A'=free_4, Q'=-1+Q, J'=free_10, [ Q>=1 && F>=2 && 0>=E && Q>=1 && F>=2 && 0>=E && 1>=free_4 && free_4>=0 && free_4>=1 && F>=2 && 0>=E && 1>=free_10 && free_10>=0 && 0>=free_10 ], cost: INF
    109: f16 -> [36] : [], cost: 0
      1: f0 -> f16 : B'=1, C'=0, D'=1, E'=free_1, F'=0, G'=free_3, H'=free_2, Q'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 ], cost: 1
     49: [36] -> [6] : A'=0, F'=1, [ Q>=1 && 0>=F && 0>=E ], cost: 2-2*F
     53: [36] -> [7] : A'=0, F'=1, [ Q>=1 && 0>=F && 0>=E ], cost: 2-2*F
     55: [36] -> [8] : [ Q>=1 && F>=2 && 0>=E ], cost: INF
     56: [36] -> [9] : [ Q>=1 && F>=2 && 0>=E ], cost: INF
     57: [36] -> [10] : [ Q>=1 && F>=2 && 0>=E ], cost: INF
     58: [36] -> [11] : [ Q>=1 && F>=2 && 0>=E ], cost: INF
     59: [36] -> [12] : A'=0, C'=0, D'=1-C+D, [ Q>=1 && 0>=E && D>=1 && F==1 && C==1 ], cost: -2+2*C
     60: [36] -> [13] : A'=0, C'=0, D'=1-C+D, [ Q>=1 && 0>=E && D>=1 && F==1 && C==1 ], cost: -2+2*C
     61: [36] -> [14] : A'=0, C'=0, D'=1-C+D, [ Q>=1 && 0>=E && D>=1 && F==1 && C==1 ], cost: -2+2*C
     62: [36] -> [15] : A'=0, C'=0, D'=1-C+D, [ Q>=1 && 0>=E && D>=1 && F==1 && C==1 ], cost: -2+2*C
     63: [36] -> [16] : A'=0, C'=0, D'=1-C+D, [ Q>=1 && 0>=E && D>=1 && F==1 && C==1 ], cost: -2+2*C
     64: [36] -> [17] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 ], cost: -2+2*F
     65: [36] -> [18] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 ], cost: -2+2*F
     66: [36] -> [19] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 ], cost: -2+2*F
     67: [36] -> [20] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 ], cost: -2+2*F
     73: [36] -> [21] : A'=0, E'=0, [ Q>=1 && E>=1 ], cost: 2*E
     74: [36] -> [22] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 ], cost: -2+2*(-1+F)*free_5+2*F
     75: [36] -> [23] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 ], cost: -2+2*(-1+F)*free_5+2*F
     76: [36] -> [24] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 ], cost: -2+2*(-1+F)*free_5+2*F
     77: [36] -> [25] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=free_5, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 ], cost: -2+2*(-1+F)*free_5+2*F
     79: [36] -> [26] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*F
     80: [36] -> [27] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*F
     81: [36] -> [28] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*F
     82: [36] -> [29] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*F
     83: [36] -> [30] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && 0>=E && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*F
     84: [36] -> [31] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*E+2*F
     85: [36] -> [32] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*E+2*F
     86: [36] -> [33] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*E+2*F
     87: [36] -> [34] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*E+2*F
     88: [36] -> [35] : A'=0, B'=-1+B+F, C'=0, D'=-1+B+F, E'=0, F'=0, [ Q>=1 && E>=1 && Q>=1 && 0>=0 && C>=2 && free_5>=0 && F==1 && Q>=1 && free_5>=1 ], cost: -2+2*(-1+F)*free_5+2*E+2*F


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


Applied chaining over branches and pruning:
  Start location: f0
    113: f0 -> [21] : A'=0, B'=1, C'=0, D'=1, E'=0, F'=0, G'=free_3, H'=free_2, Q'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=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'=0, B'=1, C'=0, D'=1, E'=0, F'=0, G'=free_3, H'=free_2, Q'=free, [ free>=0 && free_2>=free && free_2>=0 && free_3>=free_2 && free_1>=0 && free_3>=0 && free>=1 && free_1>=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:
  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
  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,?)