Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f38 -> f11 : B'=A, [ A==B ], cost: 1
     12: f38 -> f11 : G'=-1+G, [ B>=1+A ], cost: 1
     13: f38 -> f11 : G'=-1+G, [ A>=1+B ], cost: 1
      2: f11 -> f34 : A'=0, B'=free_2, D'=1+D, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D ], cost: 1
      3: f11 -> f34 : A'=1, B'=free_3, D'=1+D, [ free_3>=0 && 1>=free_3 && G>=1 && 0>=C && D==1 ], cost: 1
      4: f11 -> f34 : A'=0, B'=free_4, D'=1+D, [ free_4>=0 && 1>=free_4 && G>=1 && 0>=C && D==2 ], cost: 1
      5: f11 -> f34 : A'=free_6, B'=free_7, C'=free_5, D'=0, E'=1+E, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && free_5>=0 && G>=1 && 0>=C && D>=3 ], cost: 1
      6: f11 -> f34 : A'=free_8, B'=free_9, C'=-1+C, [ free_9>=0 && 1>=free_9 && free_8>=0 && 1>=free_8 && C>=1 && G>=1 ], cost: 1
     14: f11 -> f53 : [ 0>=G ], cost: 1
      1: f0 -> f11 : A'=0, B'=0, C'=free, D'=0, E'=1, F'=free_1, G'=free_1, [ free>=0 && free_1>=1 ], cost: 1
      7: f34 -> f38 : D'=1+D, [ 0>=B && 0>=C && 0>=D ], cost: 1
      8: f34 -> f38 : D'=1+D, [ B>=1 && 0>=C && D==1 ], cost: 1
      9: f34 -> f38 : D'=1+D, [ 0>=B && 0>=C && D==2 ], cost: 1
     10: f34 -> f38 : C'=free_10, D'=0, E'=1+E, [ free_10>=0 && 0>=C && D>=3 ], cost: 1
     11: f34 -> f38 : C'=-1+C, [ C>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f38 -> f11 : B'=A, [ A==B ], cost: 1
     12: f38 -> f11 : G'=-1+G, [ B>=1+A ], cost: 1
     13: f38 -> f11 : G'=-1+G, [ A>=1+B ], cost: 1
      2: f11 -> f34 : A'=0, B'=free_2, D'=1+D, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D ], cost: 1
      3: f11 -> f34 : A'=1, B'=free_3, D'=1+D, [ free_3>=0 && 1>=free_3 && G>=1 && 0>=C && D==1 ], cost: 1
      4: f11 -> f34 : A'=0, B'=free_4, D'=1+D, [ free_4>=0 && 1>=free_4 && G>=1 && 0>=C && D==2 ], cost: 1
      5: f11 -> f34 : A'=free_6, B'=free_7, C'=free_5, D'=0, E'=1+E, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && free_5>=0 && G>=1 && 0>=C && D>=3 ], cost: 1
      6: f11 -> f34 : A'=free_8, B'=free_9, C'=-1+C, [ free_9>=0 && 1>=free_9 && free_8>=0 && 1>=free_8 && C>=1 && G>=1 ], cost: 1
      1: f0 -> f11 : A'=0, B'=0, C'=free, D'=0, E'=1, F'=free_1, G'=free_1, [ free>=0 && free_1>=1 ], cost: 1
      7: f34 -> f38 : D'=1+D, [ 0>=B && 0>=C && 0>=D ], cost: 1
      8: f34 -> f38 : D'=1+D, [ B>=1 && 0>=C && D==1 ], cost: 1
      9: f34 -> f38 : D'=1+D, [ 0>=B && 0>=C && D==2 ], cost: 1
     10: f34 -> f38 : C'=free_10, D'=0, E'=1+E, [ free_10>=0 && 0>=C && D>=3 ], cost: 1
     11: f34 -> f38 : C'=-1+C, [ C>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f38 -> f11 : B'=A, [ A==B ], cost: 1
     12: f38 -> f11 : G'=-1+G, [ B>=1+A ], cost: 1
     13: f38 -> f11 : G'=-1+G, [ A>=1+B ], cost: 1
     15: f11 -> f38 : A'=0, B'=free_2, D'=2+D, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D && 0>=free_2 && 0>=C && 0>=1+D ], cost: 2
     16: f11 -> f38 : A'=0, B'=free_2, D'=2+D, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D && free_2>=1 && 0>=C && 1+D==1 ], cost: 2
     18: f11 -> f38 : A'=0, B'=free_4, C'=free_10, D'=0, E'=1+E, [ free_4>=0 && 1>=free_4 && G>=1 && 0>=C && D==2 && free_10>=0 && 0>=C && 1+D>=3 ], cost: 2
     20: f11 -> f38 : A'=free_6, B'=free_7, C'=-1+free_5, D'=0, E'=1+E, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && free_5>=0 && G>=1 && 0>=C && D>=3 && free_5>=1 ], cost: 2
     21: f11 -> f38 : A'=free_8, B'=free_9, C'=-1+C, D'=1+D, [ free_9>=0 && 1>=free_9 && free_8>=0 && 1>=free_8 && C>=1 && G>=1 && 0>=free_9 && 0>=-1+C && 0>=D ], cost: 2
      1: f0 -> f11 : A'=0, B'=0, C'=free, D'=0, E'=1, F'=free_1, G'=free_1, [ free>=0 && free_1>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     26: f11 -> f11 : A'=0, B'=0, D'=2+D, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D && 0>=free_2 && 0>=C && 0>=1+D && 0==free_2 ], cost: 3
     27: f11 -> f11 : A'=0, B'=free_2, D'=2+D, G'=-1+G, [ free_2>=0 && 1>=free_2 && G>=1 && 0>=C && 0>=D && free_2>=1 && 0>=C && 1+D==1 && free_2>=1 ], cost: 3
     29: f11 -> f11 : A'=0, B'=free_4, C'=free_10, D'=0, E'=1+E, G'=-1+G, [ free_4>=0 && 1>=free_4 && G>=1 && 0>=C && D==2 && free_10>=0 && 0>=C && 1+D>=3 && free_4>=1 ], cost: 3
     30: f11 -> f11 : A'=free_6, B'=free_6, C'=-1+free_5, D'=0, E'=1+E, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && free_5>=0 && G>=1 && 0>=C && D>=3 && free_5>=1 && free_6==free_7 ], cost: 3
     32: f11 -> f11 : A'=free_6, B'=free_7, C'=-1+free_5, D'=0, E'=1+E, G'=-1+G, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && free_5>=0 && G>=1 && 0>=C && D>=3 && free_5>=1 && free_6>=1+free_7 ], cost: 3
      1: f0 -> f11 : A'=0, B'=0, C'=free, D'=0, E'=1, F'=free_1, G'=free_1, [ free>=0 && free_1>=1 ], cost: 1

Eliminating 5 self-loops for location f11
  Self-Loop 26 has the metering function: meter, resulting in the new transition 35.
  Self-Loop 27 has the metering function: meter_1, resulting in the new transition 36.
  Self-Loop 29 has the metering function: meter_2, resulting in the new transition 37.
  Found this metering function when nesting loops: meter_3,
  and nested parallel self-loops 26 (outer loop) and 36 (inner loop), obtaining the new transitions: 40.
  Found this metering function when nesting loops: meter_4,
  and nested parallel self-loops 29 (outer loop) and 36 (inner loop), obtaining the new transitions: 41.
  Found this metering function when nesting loops: 2-D,
  and nested parallel self-loops 27 (outer loop) and 37 (inner loop), obtaining the new transitions: 42, 43.
  Found this metering function when nesting loops: -D,
  and nested parallel self-loops 27 (outer loop) and 37 (inner loop), obtaining the new transitions: 44, 45.
  Found this metering function when nesting loops: meter_5,
  Found this metering function when nesting loops: meter_6,
  and nested parallel self-loops 29 (outer loop) and 44 (inner loop), obtaining the new transitions: 46.
  Found this metering function when nesting loops: 2-D,
  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: -D,
  and nested parallel self-loops 27 (outer loop) and 45 (inner loop), obtaining the new transitions: 49, 50.
  Found this metering function when nesting loops: 2-D,
  and nested parallel self-loops 27 (outer loop) and 46 (inner loop), obtaining the new transitions: 51, 52.
  Found this metering function when nesting loops: -D,
  and nested parallel self-loops 27 (outer loop) and 46 (inner loop), obtaining the new transitions: 53, 54.
  Found this metering function when nesting loops: meter_7,
  and nested parallel self-loops 29 (outer loop) and 49 (inner loop), obtaining the new transitions: 55.
  Found this metering function when nesting loops: 2-D,
  and nested parallel self-loops 27 (outer loop) and 50 (inner loop), obtaining the new transitions: 56, 57.
  Found this metering function when nesting loops: -D,
  and nested parallel self-loops 27 (outer loop) and 50 (inner loop), obtaining the new transitions: 58, 59.
  Removing the self-loops: 26 27 29 30 32.
Adding an epsilon transition (to model nonexecution of the loops): 60.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     35: f11 -> [5] : A'=0, B'=0, D'=2*meter+D, [ G>=1 && 0>=C && 0>=1+D && 2*meter==-D ], cost: 3*meter
     36: f11 -> [5] : A'=0, B'=1, D'=2*meter_1+D, G'=-meter_1+G, [ G>=1 && 0>=C && 1+D==1 && 2*meter_1==-D ], cost: 3*meter_1
     37: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_2, G'=G-meter_2, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D ], cost: 3*meter_2
     38: f11 -> [5] : A'=free_7, B'=free_7, C'=-1+free_5, D'=0, E'=1+E, [ free_7>=0 && 1>=free_7 && free_7>=0 && 1>=free_7 && G>=1 && 0>=C && D>=3 && free_5>=1 ], cost: 3
     39: f11 -> [5] : A'=free_6, B'=free_7, C'=-1+free_5, D'=0, E'=1+E, G'=-1+G, [ free_7>=0 && 1>=free_7 && free_6>=0 && 1>=free_6 && G>=1 && 0>=C && D>=3 && free_5>=1 && free_6>=1+free_7 ], cost: 3
     40: f11 -> [5] : A'=0, B'=1, D'=2*meter_3+2*meter_3*meter_1+D, G'=-meter_3*meter_1+G, [ G>=1 && 0>=C && 0>=1+D && G>=1 && 0>=C && 3+D==1 && 2*meter_1==-2-D && 2*meter_3==-2-D ], cost: 3*meter_3+3*meter_3*meter_1
     41: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2*meter_1, E'=E+meter_4, G'=-meter_4-meter_1*meter_4+G, [ G>=1 && 0>=C && D==2 && free_10>=0 && -1+G>=1 && 0>=free_10 && 1==1 && 2*meter_1==0 && 2*meter_4==-2+D ], cost: 3*meter_4+3*meter_1*meter_4
     42: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=E-(-2+D)*meter_2, G'=-2+(-2+D)*meter_2+G+D, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 6-3*(-2+D)*meter_2-3*D
     43: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=-D*meter_2+E, G'=-1+D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D && -1+G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 3-3*D*meter_2-3*D
     44: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=-D*meter_2+E, G'=D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D ], cost: -3*D*meter_2-3*D
     45: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_2, G'=G-meter_2, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 ], cost: 3*meter_2
     46: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_6, G'=-meter_6+G, [ G>=1 && 0>=C && D==2 && free_10>=0 && -1+G>=1 && 0>=free_10 && 1==1 && -2+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==-2+D ], cost: 3*meter_6
     47: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=E-(-2+D)*meter_2, G'=-2+(-2+D)*meter_2+G+D, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 6-3*(-2+D)*meter_2-3*D
     48: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=-D*meter_2+E, G'=-1+D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 3-3*D*meter_2-3*D
     49: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=-D*meter_2+E, G'=D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 ], cost: -3*D*meter_2-3*D
     50: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_2, G'=G-meter_2, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -2+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 ], cost: 3*meter_2
     51: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=E-(-2+D)*meter_6, G'=-2+(-2+D)*meter_6+G+D, [ G>=1 && 0>=C && D==2 && free_10>=0 && -1+G>=1 && 0>=free_10 && 1==1 && -2+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==-2+D && -meter_6+G>=1 && 0>=free_10 && 1==1 ], cost: 6-3*(-2+D)*meter_6-3*D
     52: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=-meter_6*D+E, G'=-1+meter_6*D+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && -2+G>=1 && 0>=free_10 && 1==1 && -3+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==D && -1-meter_6+G>=1 && 0>=free_10 && 1==1 ], cost: 3-3*meter_6*D-3*D
     53: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=-meter_6*D+E, G'=meter_6*D+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && -2+G>=1 && 0>=free_10 && 1==1 && -3+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==D ], cost: -3*meter_6*D-3*D
     54: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_6, G'=-meter_6+G, [ G>=1 && 0>=C && D==2 && free_10>=0 && -1+G>=1 && 0>=free_10 && 1==1 && -2+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==-2+D && -meter_6+G>=1 && 0>=free_10 && 1==1 && -1-meter_6+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && -2-meter_6+G>=1 && 0>=free_10 && 1==1 && -3-meter_6+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_6==0 ], cost: 3*meter_6
     55: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_7, G'=-meter_7+G, [ G>=1 && 0>=C && D==2 && free_10>=0 && -1+G>=1 && 0>=free_10 && 1==1 && -2+G>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -2+G-meter_2>=1 && 0>=free_10 && 1==1 && -3+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && 2*meter_7==-2+D ], cost: 3*meter_7
     56: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=E-(-2+D)*meter_2, G'=-2+(-2+D)*meter_2+G+D, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -2+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 6-3*(-2+D)*meter_2-3*D
     57: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=2, E'=-D*meter_2+E, G'=-1+D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -2+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -3+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-meter_2>=1 && 0>=free_10 && 1==1 ], cost: 3-3*D*meter_2-3*D
     58: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=-D*meter_2+E, G'=D*meter_2+G+D, [ G>=1 && 0>=C && 1+D==1 && -1+G>=1 && 0>=C && 2+D==2 && free_10>=0 && 2*meter_2==D && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-meter_2>=1 && 0>=free_10 && 1==1 && -2+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -2+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -3+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 ], cost: -3*D*meter_2-3*D
     59: f11 -> [5] : A'=0, B'=1, C'=free_10, D'=0, E'=E+meter_2, G'=G-meter_2, [ G>=1 && 0>=C && D==2 && free_10>=0 && 2*meter_2==-2+D && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -2+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && G-meter_2>=1 && 0>=free_10 && 1==1 && -1+G-meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -2+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -1+G-2*meter_2>=1 && 0>=free_10 && 1==1 && -2+G-2*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 && -2+G-3*meter_2>=1 && 0>=free_10 && 1==1 && -3+G-3*meter_2>=1 && 0>=free_10 && 2==2 && free_10>=0 && 2*meter_2==0 ], cost: 3*meter_2
     60: f11 -> [5] : [], cost: 0
      1: f0 -> f11 : A'=0, B'=0, C'=free, D'=0, E'=1, F'=free_1, G'=free_1, [ free>=0 && free_1>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     61: f0 -> [5] : A'=0, B'=1, C'=free, D'=2*meter_1, E'=1, F'=free_1, G'=-meter_1+free_1, [ free>=0 && free_1>=1 && free_1>=1 && 0>=free && 1==1 && 2*meter_1==0 ], cost: 1+3*meter_1


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     61: f0 -> [5] : A'=0, B'=1, C'=free, D'=2*meter_1, E'=1, F'=free_1, G'=-meter_1+free_1, [ free>=0 && free_1>=1 && free_1>=1 && 0>=free && 1==1 && 2*meter_1==0 ], cost: 1+3*meter_1


Computing complexity for remaining 1 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),?)