Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f129 -> f130 : [ 0>=1+A ], cost: 1
      1: f129 -> f130 : [ A>=1 ], cost: 1
     44: f129 -> f141 : A'=0, U'=1, [ A==0 ], cost: 1
      2: f130 -> f131 : [ 0>=1+B ], cost: 1
      3: f130 -> f131 : [ B>=1 ], cost: 1
     43: f130 -> f141 : B'=0, U'=1, [ B==0 ], cost: 1
      4: f131 -> f132 : [ 0>=1+C ], cost: 1
      5: f131 -> f132 : [ C>=1 ], cost: 1
     42: f131 -> f141 : C'=0, U'=1, [ C==0 ], cost: 1
     39: f132 -> f141 : U'=0, [ 0>=1+G ], cost: 1
     40: f132 -> f141 : U'=0, [ G>=1 ], cost: 1
     41: f132 -> f141 : G'=0, U'=1, [ G==0 ], cost: 1
      6: f0 -> f25 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [], cost: 1
      7: f25 -> f25 : M'=1+M, [ E>=1+M ], cost: 1
     66: f25 -> f31 : M'=0, [ M>=E ], cost: 1
     13: f31 -> f31 : A'=0, M'=1+M, N'=0, [ E>=1+M && A==0 ], cost: 1
      8: f31 -> f34 : [ E>=1+M && 0>=1+A ], cost: 1
      9: f31 -> f34 : [ E>=1+M && A>=1 ], cost: 1
     65: f31 -> f44 : M'=0, [ M>=E ], cost: 1
     10: f34 -> f31 : A'=1, M'=1+M, N'=1, [ free_3>=1 ], cost: 1
     11: f34 -> f31 : A'=0, M'=1+M, N'=0, [ free_4>=1 ], cost: 1
     12: f34 -> f31 : A'=0, M'=1+M, N'=0, [ 0>=free_5 ], cost: 1
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     64: f44 -> f60 : M'=0, [ M>=E ], cost: 1
     63: f47 -> f44 : M'=1+M, [ O>=E ], cost: 1
     20: f47 -> f47 : B'=0, O'=1+O, P'=0, [ E>=1+O && B==0 ], cost: 1
     15: f47 -> f50 : [ E>=1+O && 0>=1+B ], cost: 1
     16: f47 -> f50 : [ E>=1+O && B>=1 ], cost: 1
     17: f50 -> f47 : B'=1, O'=1+O, P'=1, [ free_7>=1+free_6 ], cost: 1
     18: f50 -> f47 : B'=1, O'=1+O, P'=1, [], cost: 1
     19: f50 -> f47 : B'=0, O'=1+O, P'=0, [], cost: 1
     21: f60 -> f60 : H'=H+free_8, M'=1+M, [ D>=1+M ], cost: 1
     60: f60 -> f66 : [ M>=D && 0>=1+C ], cost: 1
     61: f60 -> f66 : [ M>=D && C>=1 ], cost: 1
     62: f60 -> f72 : C'=0, M'=0, Q_1'=0, [ M>=D && C==0 ], cost: 1
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     25: f72 -> f72 : Q'=free_9+Q, M'=1+M, [ D>=1+M ], cost: 1
     57: f72 -> f78 : [ M>=D && 0>=1+C ], cost: 1
     58: f72 -> f78 : [ M>=D && C>=1 ], cost: 1
     59: f72 -> f84 : C'=0, M'=0, R'=0, [ M>=D && C==0 ], cost: 1
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     29: f84 -> f88 : J'=0, O'=0, [ D>=1+M ], cost: 1
     56: f84 -> f102 : O'=0, [ M>=D ], cost: 1
     55: f88 -> f84 : C'=0, M'=1+M, S'=0, [ O>=D && C==0 ], cost: 1
     30: f88 -> f88 : J'=free_10+J, O'=1+O, [ D>=1+O ], cost: 1
     53: f88 -> f94 : [ O>=D && 0>=1+C ], cost: 1
     54: f88 -> f94 : [ O>=D && C>=1 ], cost: 1
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     48: f102 -> f129 : G'=1, V'=1, [ free_18>=1+free_13 && free_15>=1+free_17 && free_12>=1+free_14 && O>=D && free_16>=1+free_19 ], cost: 1
     49: f102 -> f129 : G'=0, V'=0, [ free_25>=1+free_21 && free_23>=1+free_24 && O>=D && free_20>=1+free_22 ], cost: 1
     50: f102 -> f129 : G'=0, V'=0, [ free_29>=1+free_26 && O>=D && free_27>=1+free_28 ], cost: 1
     51: f102 -> f129 : G'=0, V'=0, [ O>=D && free_31>=1+free_30 ], cost: 1
     52: f102 -> f129 : G'=0, V'=0, [ O>=D ], cost: 1
     34: f102 -> f106 : K'=0, M'=0, [ D>=1+O ], cost: 1
     47: f106 -> f102 : C'=0, O'=1+O, T'=0, [ M>=D && C==0 ], cost: 1
     35: f106 -> f106 : K'=K+free_11, M'=1+M, [ D>=1+M ], cost: 1
     45: f106 -> f112 : [ M>=D && 0>=1+C ], cost: 1
     46: f106 -> f112 : [ M>=D && C>=1 ], cost: 1
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1

Removing duplicate transition: 11.
Removing duplicate transition: 17.

Simplified the transitions:
  Start location: f0
      6: f0 -> f25 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [], cost: 1
      7: f25 -> f25 : M'=1+M, [ E>=1+M ], cost: 1
     66: f25 -> f31 : M'=0, [ M>=E ], cost: 1
     13: f31 -> f31 : A'=0, M'=1+M, N'=0, [ E>=1+M && A==0 ], cost: 1
      8: f31 -> f34 : [ E>=1+M && 0>=1+A ], cost: 1
      9: f31 -> f34 : [ E>=1+M && A>=1 ], cost: 1
     65: f31 -> f44 : M'=0, [ M>=E ], cost: 1
     10: f34 -> f31 : A'=1, M'=1+M, N'=1, [], cost: 1
     12: f34 -> f31 : A'=0, M'=1+M, N'=0, [], cost: 1
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     64: f44 -> f60 : M'=0, [ M>=E ], cost: 1
     63: f47 -> f44 : M'=1+M, [ O>=E ], cost: 1
     20: f47 -> f47 : B'=0, O'=1+O, P'=0, [ E>=1+O && B==0 ], cost: 1
     15: f47 -> f50 : [ E>=1+O && 0>=1+B ], cost: 1
     16: f47 -> f50 : [ E>=1+O && B>=1 ], cost: 1
     18: f50 -> f47 : B'=1, O'=1+O, P'=1, [], cost: 1
     19: f50 -> f47 : B'=0, O'=1+O, P'=0, [], cost: 1
     21: f60 -> f60 : H'=H+free_8, M'=1+M, [ D>=1+M ], cost: 1
     60: f60 -> f66 : [ M>=D && 0>=1+C ], cost: 1
     61: f60 -> f66 : [ M>=D && C>=1 ], cost: 1
     62: f60 -> f72 : C'=0, M'=0, Q_1'=0, [ M>=D && C==0 ], cost: 1
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     25: f72 -> f72 : Q'=free_9+Q, M'=1+M, [ D>=1+M ], cost: 1
     57: f72 -> f78 : [ M>=D && 0>=1+C ], cost: 1
     58: f72 -> f78 : [ M>=D && C>=1 ], cost: 1
     59: f72 -> f84 : C'=0, M'=0, R'=0, [ M>=D && C==0 ], cost: 1
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     29: f84 -> f88 : J'=0, O'=0, [ D>=1+M ], cost: 1
     56: f84 -> f102 : O'=0, [ M>=D ], cost: 1
     55: f88 -> f84 : C'=0, M'=1+M, S'=0, [ O>=D && C==0 ], cost: 1
     30: f88 -> f88 : J'=free_10+J, O'=1+O, [ D>=1+O ], cost: 1
     53: f88 -> f94 : [ O>=D && 0>=1+C ], cost: 1
     54: f88 -> f94 : [ O>=D && C>=1 ], cost: 1
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     34: f102 -> f106 : K'=0, M'=0, [ D>=1+O ], cost: 1
     47: f106 -> f102 : C'=0, O'=1+O, T'=0, [ M>=D && C==0 ], cost: 1
     35: f106 -> f106 : K'=K+free_11, M'=1+M, [ D>=1+M ], cost: 1
     45: f106 -> f112 : [ M>=D && 0>=1+C ], cost: 1
     46: f106 -> f112 : [ M>=D && C>=1 ], cost: 1
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1

Eliminating 1 self-loops for location f25
  Self-Loop 7 has the metering function: E-M, resulting in the new transition 67.
  Removing the self-loops: 7.
Eliminating 1 self-loops for location f31
  Self-Loop 13 has the metering function: E-M, resulting in the new transition 68.
  Removing the self-loops: 13.
Eliminating 1 self-loops for location f47
  Self-Loop 20 has the metering function: E-O, resulting in the new transition 69.
  Removing the self-loops: 20.
Eliminating 1 self-loops for location f60
  Self-Loop 21 has the metering function: -M+D, resulting in the new transition 70.
  Removing the self-loops: 21.
Eliminating 1 self-loops for location f72
  Self-Loop 25 has the metering function: -M+D, resulting in the new transition 71.
  Removing the self-loops: 25.
Eliminating 1 self-loops for location f88
  Self-Loop 30 has the metering function: -O+D, resulting in the new transition 72.
  Removing the self-loops: 30.
Eliminating 1 self-loops for location f106
  Self-Loop 35 has the metering function: -M+D, resulting in the new transition 73.
  Removing the self-loops: 35.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      6: f0 -> f25 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [], cost: 1
     67: f25 -> [22] : M'=E, [ E>=1+M ], cost: E-M
     68: f31 -> [23] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     10: f34 -> f31 : A'=1, M'=1+M, N'=1, [], cost: 1
     12: f34 -> f31 : A'=0, M'=1+M, N'=0, [], cost: 1
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     64: f44 -> f60 : M'=0, [ M>=E ], cost: 1
     69: f47 -> [24] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     18: f50 -> f47 : B'=1, O'=1+O, P'=1, [], cost: 1
     19: f50 -> f47 : B'=0, O'=1+O, P'=0, [], cost: 1
     70: f60 -> [25] : H'=H-free_8*(M-D), M'=D, [ D>=1+M ], cost: -M+D
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     71: f72 -> [26] : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M ], cost: -M+D
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     29: f84 -> f88 : J'=0, O'=0, [ D>=1+M ], cost: 1
     56: f84 -> f102 : O'=0, [ M>=D ], cost: 1
     72: f88 -> [27] : J'=J-free_10*(O-D), O'=D, [ D>=1+O ], cost: -O+D
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     34: f102 -> f106 : K'=0, M'=0, [ D>=1+O ], cost: 1
     73: f106 -> [28] : K'=K-free_11*(M-D), M'=D, [ D>=1+M ], cost: -M+D
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1
     66: [22] -> f31 : M'=0, [ M>=E ], cost: 1
      8: [23] -> f34 : [ E>=1+M && 0>=1+A ], cost: 1
      9: [23] -> f34 : [ E>=1+M && A>=1 ], cost: 1
     65: [23] -> f44 : M'=0, [ M>=E ], cost: 1
     63: [24] -> f44 : M'=1+M, [ O>=E ], cost: 1
     15: [24] -> f50 : [ E>=1+O && 0>=1+B ], cost: 1
     16: [24] -> f50 : [ E>=1+O && B>=1 ], cost: 1
     60: [25] -> f66 : [ M>=D && 0>=1+C ], cost: 1
     61: [25] -> f66 : [ M>=D && C>=1 ], cost: 1
     62: [25] -> f72 : C'=0, M'=0, Q_1'=0, [ M>=D && C==0 ], cost: 1
     57: [26] -> f78 : [ M>=D && 0>=1+C ], cost: 1
     58: [26] -> f78 : [ M>=D && C>=1 ], cost: 1
     59: [26] -> f84 : C'=0, M'=0, R'=0, [ M>=D && C==0 ], cost: 1
     55: [27] -> f84 : C'=0, M'=1+M, S'=0, [ O>=D && C==0 ], cost: 1
     53: [27] -> f94 : [ O>=D && 0>=1+C ], cost: 1
     54: [27] -> f94 : [ O>=D && C>=1 ], cost: 1
     47: [28] -> f102 : C'=0, O'=1+O, T'=0, [ M>=D && C==0 ], cost: 1
     45: [28] -> f112 : [ M>=D && 0>=1+C ], cost: 1
     46: [28] -> f112 : [ M>=D && C>=1 ], cost: 1


Applied simple chaining:
  Start location: f0
      6: f0 -> f31 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     68: f31 -> [23] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     10: f34 -> f31 : A'=1, M'=1+M, N'=1, [], cost: 1
     12: f34 -> f31 : A'=0, M'=1+M, N'=0, [], cost: 1
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     64: f44 -> [25] : H'=H+free_8*D, M'=D, [ M>=E && D>=1 ], cost: 1+D
     69: f47 -> [24] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     18: f50 -> f47 : B'=1, O'=1+O, P'=1, [], cost: 1
     19: f50 -> f47 : B'=0, O'=1+O, P'=0, [], cost: 1
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     71: f72 -> [26] : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M ], cost: -M+D
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     56: f84 -> f102 : O'=0, [ M>=D ], cost: 1
     29: f84 -> [27] : J'=free_10*D, O'=D, [ D>=1+M && D>=1 ], cost: 1+D
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     34: f102 -> [28] : K'=free_11*D, M'=D, [ D>=1+O && D>=1 ], cost: 1+D
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1
      8: [23] -> f34 : [ E>=1+M && 0>=1+A ], cost: 1
      9: [23] -> f34 : [ E>=1+M && A>=1 ], cost: 1
     65: [23] -> f44 : M'=0, [ M>=E ], cost: 1
     63: [24] -> f44 : M'=1+M, [ O>=E ], cost: 1
     15: [24] -> f50 : [ E>=1+O && 0>=1+B ], cost: 1
     16: [24] -> f50 : [ E>=1+O && B>=1 ], cost: 1
     60: [25] -> f66 : [ M>=D && 0>=1+C ], cost: 1
     61: [25] -> f66 : [ M>=D && C>=1 ], cost: 1
     62: [25] -> f72 : C'=0, M'=0, Q_1'=0, [ M>=D && C==0 ], cost: 1
     57: [26] -> f78 : [ M>=D && 0>=1+C ], cost: 1
     58: [26] -> f78 : [ M>=D && C>=1 ], cost: 1
     59: [26] -> f84 : C'=0, M'=0, R'=0, [ M>=D && C==0 ], cost: 1
     55: [27] -> f84 : C'=0, M'=1+M, S'=0, [ O>=D && C==0 ], cost: 1
     53: [27] -> f94 : [ O>=D && 0>=1+C ], cost: 1
     54: [27] -> f94 : [ O>=D && C>=1 ], cost: 1
     47: [28] -> f102 : C'=0, O'=1+O, T'=0, [ M>=D && C==0 ], cost: 1
     45: [28] -> f112 : [ M>=D && 0>=1+C ], cost: 1
     46: [28] -> f112 : [ M>=D && C>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      6: f0 -> f31 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     76: f31 -> f44 : A'=0, M'=0, N'=0, [ E>=1+M && A==0 && E>=E ], cost: 1+E-M
     74: f31 -> [29] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     75: f31 -> [30] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     77: f44 -> f66 : H'=H+free_8*D, M'=D, [ M>=E && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     78: f44 -> f66 : H'=H+free_8*D, M'=D, [ M>=E && D>=1 && D>=D && C>=1 ], cost: 2+D
     79: f44 -> f72 : C'=0, H'=H+free_8*D, M'=0, Q_1'=0, [ M>=E && D>=1 && D>=D && C==0 ], cost: 2+D
     80: f47 -> f44 : B'=0, M'=1+M, O'=E, P'=0, [ E>=1+O && B==0 && E>=E ], cost: 1+E-O
     81: f47 -> [31] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     82: f47 -> [32] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     83: f72 -> f78 : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M && D>=D && 0>=1+C ], cost: 1-M+D
     84: f72 -> f78 : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M && D>=D && C>=1 ], cost: 1-M+D
     85: f72 -> f84 : C'=0, Q'=Q-free_9*(M-D), M'=0, R'=0, [ D>=1+M && D>=D && C==0 ], cost: 1-M+D
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     86: f84 -> f84 : C'=0, J'=free_10*D, M'=1+M, O'=D, S'=0, [ D>=1+M && D>=1 && D>=D && C==0 ], cost: 2+D
     87: f84 -> f94 : J'=free_10*D, O'=D, [ D>=1+M && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     88: f84 -> f94 : J'=free_10*D, O'=D, [ D>=1+M && D>=1 && D>=D && C>=1 ], cost: 2+D
     56: f84 -> f102 : O'=0, [ M>=D ], cost: 1
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     89: f102 -> f102 : C'=0, K'=free_11*D, M'=D, O'=1+O, T'=0, [ D>=1+O && D>=1 && D>=D && C==0 ], cost: 2+D
     90: f102 -> f112 : K'=free_11*D, M'=D, [ D>=1+O && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     91: f102 -> f112 : K'=free_11*D, M'=D, [ D>=1+O && D>=1 && D>=D && C>=1 ], cost: 2+D
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1

Eliminating 1 self-loops for location f84
  Self-Loop 86 has the metering function: -M+D, resulting in the new transition 92.
  Removing the self-loops: 86.
Eliminating 1 self-loops for location f102
  Self-Loop 89 has the metering function: -O+D, resulting in the new transition 93.
  Removing the self-loops: 89.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      6: f0 -> f31 : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     76: f31 -> f44 : A'=0, M'=0, N'=0, [ E>=1+M && A==0 && E>=E ], cost: 1+E-M
     74: f31 -> [29] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     75: f31 -> [30] : A'=0, M'=E, N'=0, [ E>=1+M && A==0 ], cost: E-M
     14: f44 -> f47 : O'=1+M, [ E>=1+M ], cost: 1
     77: f44 -> f66 : H'=H+free_8*D, M'=D, [ M>=E && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     78: f44 -> f66 : H'=H+free_8*D, M'=D, [ M>=E && D>=1 && D>=D && C>=1 ], cost: 2+D
     79: f44 -> f72 : C'=0, H'=H+free_8*D, M'=0, Q_1'=0, [ M>=E && D>=1 && D>=D && C==0 ], cost: 2+D
     80: f47 -> f44 : B'=0, M'=1+M, O'=E, P'=0, [ E>=1+O && B==0 && E>=E ], cost: 1+E-O
     81: f47 -> [31] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     82: f47 -> [32] : B'=0, O'=E, P'=0, [ E>=1+O && B==0 ], cost: E-O
     22: f66 -> f72 : C'=1, H'=F, M'=0, Q_1'=1, [ F==H ], cost: 1
     23: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ F>=1+H ], cost: 1
     24: f66 -> f72 : C'=0, M'=0, Q_1'=0, [ H>=1+F ], cost: 1
     83: f72 -> f78 : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M && D>=D && 0>=1+C ], cost: 1-M+D
     84: f72 -> f78 : Q'=Q-free_9*(M-D), M'=D, [ D>=1+M && D>=D && C>=1 ], cost: 1-M+D
     85: f72 -> f84 : C'=0, Q'=Q-free_9*(M-D), M'=0, R'=0, [ D>=1+M && D>=D && C==0 ], cost: 1-M+D
     26: f78 -> f84 : C'=1, Q'=F, M'=0, R'=1, [ F==Q ], cost: 1
     27: f78 -> f84 : C'=0, M'=0, R'=0, [ F>=1+Q ], cost: 1
     28: f78 -> f84 : C'=0, M'=0, R'=0, [ Q>=1+F ], cost: 1
     92: f84 -> [33] : C'=0, J'=free_10*D, M'=D, O'=D, S'=0, [ D>=1+M && D>=1 && C==0 ], cost: -2*M-(M-D)*D+2*D
     31: f94 -> f84 : C'=1, J'=F, M'=1+M, S'=1, [ F==J ], cost: 1
     32: f94 -> f84 : C'=0, M'=1+M, S'=0, [ F>=1+J ], cost: 1
     33: f94 -> f84 : C'=0, M'=1+M, S'=0, [ J>=1+F ], cost: 1
     93: f102 -> [34] : C'=0, K'=free_11*D, M'=D, O'=D, T'=0, [ D>=1+O && D>=1 && C==0 ], cost: -D*(O-D)-2*O+2*D
     36: f112 -> f102 : C'=1, K'=F, O'=1+O, T'=1, [ F==K ], cost: 1
     37: f112 -> f102 : C'=0, O'=1+O, T'=0, [ F>=1+K ], cost: 1
     38: f112 -> f102 : C'=0, O'=1+O, T'=0, [ K>=1+F ], cost: 1
     87: [33] -> f94 : J'=free_10*D, O'=D, [ D>=1+M && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     88: [33] -> f94 : J'=free_10*D, O'=D, [ D>=1+M && D>=1 && D>=D && C>=1 ], cost: 2+D
     56: [33] -> f102 : O'=0, [ M>=D ], cost: 1
     90: [34] -> f112 : K'=free_11*D, M'=D, [ D>=1+O && D>=1 && D>=D && 0>=1+C ], cost: 2+D
     91: [34] -> f112 : K'=free_11*D, M'=D, [ D>=1+O && D>=1 && D>=D && C>=1 ], cost: 2+D


Applied chaining over branches and pruning:
  Start location: f0
     94: f0 -> [35] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     95: f0 -> [36] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     96: f0 -> [37] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     94: f0 -> [35] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     95: f0 -> [36] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2
     96: f0 -> [37] : A'=1, B'=1, C'=1, D'=4, E'=free_2, F'=free, G'=0, H'=0, Q'=0, J'=0, K'=0, L'=free_1, M'=0, [ free_2>=1 && free_2>=free_2 ], cost: 2+free_2


Computing complexity for remaining 3 transitions.

  Found configuration with infinitely models for cost: 2+free_2
  and guard: free_2>=1 && free_2>=free_2:
  free_2: Pos

Found new complexity INF, because: Found infinity configuration.


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

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

WORST_CASE(INF,?)