Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: f2 -> f2 : B'=1+B, [ A>=B ], cost: 1
     28: f2 -> f10 : [ B>=1+A ], cost: 1
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
      6: f15 -> f15 : D'=1+D, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: 1
      7: f15 -> f15 : D'=1+D, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: 1
      4: f15 -> f24 : [ D>=A ], cost: 1
      5: f15 -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     27: f10 -> f1 : [ C>=1+A ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ free_18>=K*free_14+free_14*free_16 && K*free_14+free_14*free_16+free_14>=1+free_18 && K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ free_21*free_19+free_23>=K*free_19 && free_19+K*free_19>=1+free_21*free_19+free_23 && 0>=1+K ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=P*free_28, T'=free_32*O, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 ], cost: 1
     19: f42 -> f60 : K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_42*P, T'=O*free_46, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     26: f60 -> f42 : B'=-1+B, [ U>=1+A ], cost: 1
     20: f60 -> f60 : S'=free_54, U'=1+U, [ A>=U ], cost: 1
     29: start -> f2 : [], cost: 1


Simplified the transitions:
  Start location: start
      0: f2 -> f2 : B'=1+B, [ A>=B ], cost: 1
     28: f2 -> f10 : [ B>=1+A ], cost: 1
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
      6: f15 -> f15 : D'=1+D, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: 1
      7: f15 -> f15 : D'=1+D, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: 1
      4: f15 -> f24 : [ D>=A ], cost: 1
      5: f15 -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=P*free_28, T'=free_32*O, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 ], cost: 1
     19: f42 -> f60 : K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_42*P, T'=O*free_46, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     26: f60 -> f42 : B'=-1+B, [ U>=1+A ], cost: 1
     20: f60 -> f60 : S'=free_54, U'=1+U, [ A>=U ], cost: 1
     29: start -> f2 : [], cost: 1

Eliminating 1 self-loops for location f2
  Self-Loop 0 has the metering function: 1-B+A, resulting in the new transition 30.
  Removing the self-loops: 0.
Eliminating 2 self-loops for location f15
  Self-Loop 6 has the metering function: -D+A, resulting in the new transition 31.
  Self-Loop 7 has the metering function: -D+A, resulting in the new transition 32.
  Removing the self-loops: 6 7.
Eliminating 1 self-loops for location f60
  Self-Loop 20 has the metering function: 1-U+A, resulting in the new transition 33.
  Removing the self-loops: 20.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     30: f2 -> [12] : B'=1+A, [ A>=B ], cost: 1-B+A
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     31: f15 -> [13] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     32: f15 -> [13] : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=P*free_28, T'=free_32*O, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 ], cost: 1
     19: f42 -> f60 : K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_42*P, T'=O*free_46, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     33: f60 -> [14] : S'=free_54, U'=1+A, [ A>=U ], cost: 1-U+A
     29: start -> f2 : [], cost: 1
     28: [12] -> f10 : [ B>=1+A ], cost: 1
      4: [13] -> f24 : [ D>=A ], cost: 1
      5: [13] -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
     26: [14] -> f42 : B'=-1+B, [ U>=1+A ], cost: 1


Applied simple chaining:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     31: f15 -> [13] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     32: f15 -> [13] : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=P*free_28, T'=free_32*O, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 ], cost: 1
     19: f42 -> f60 : K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_42*P, T'=O*free_46, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     33: f60 -> f42 : B'=-1+B, S'=free_54, U'=1+A, [ A>=U && 1+A>=1+A ], cost: 2-U+A
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
      4: [13] -> f24 : [ D>=A ], cost: 1
      5: [13] -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     34: f15 -> f24 : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A ], cost: 1-D+A
     36: f15 -> f24 : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A ], cost: 1-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
     38: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ C>=1+D && 29>=E ], cost: 2
     39: f24 -> f32 : E'=1+E, J'=E, K'=free_10, L'=free_11, [ C>=1+D && E>=31 ], cost: 2
     40: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ C>=1+D && E==30 ], cost: 2
     41: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ D>=1+C && 29>=E ], cost: 2
     43: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ D>=1+C && E==30 ], cost: 2
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     44: f42 -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: f42 -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: f42 -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: f42 -> f75 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C && B>=C && 0==0 ], cost: 2
     48: f42 -> f42 : B'=-1+B, K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=free_54, T'=free_32*O, U'=1+A, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 && A>=U && 1+A>=1+A ], cost: 3-U+A
     49: f42 -> f42 : B'=-1+B, K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_54, T'=O*free_46, U'=1+A, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 && A>=U && 1+A>=1+A ], cost: 3-U+A
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 2 self-loops for location f42
  Removing the self-loops: 48 49.
Adding an epsilon transition (to model nonexecution of the loops): 52.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     34: f15 -> f24 : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A ], cost: 1-D+A
     36: f15 -> f24 : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A ], cost: 1-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
     38: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ C>=1+D && 29>=E ], cost: 2
     39: f24 -> f32 : E'=1+E, J'=E, K'=free_10, L'=free_11, [ C>=1+D && E>=31 ], cost: 2
     40: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ C>=1+D && E==30 ], cost: 2
     41: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ D>=1+C && 29>=E ], cost: 2
     43: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ D>=1+C && E==30 ], cost: 2
     14: f32 -> f42 : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     15: f32 -> f42 : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     50: f42 -> [17] : B'=-1+B, K'=free_30-free_32*O, L'=free_27, O'=free_31, P'=free_29, Q_1'=free_26, S'=free_54, T'=free_32*O, U'=1+A, [ K*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1+K*free_27 && 0>=1+free_33 && B>=C && P*free_28>=free_33*free_37 && free_33*free_37+free_37>=1+P*free_28 && free_37>=free_29 && P*free_28>=free_39*free_33 && free_39+free_39*free_33>=1+P*free_28 && free_29>=free_39 && K>=free_33*free_34 && free_33*free_34+free_34>=1+K && free_34>=free_31 && K>=free_36*free_33 && free_36+free_36*free_33>=1+K && free_31>=free_36 && free_27*P*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*P*free_28 && free_38>=free_26 && free_27*P*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*P*free_28 && free_26>=free_35 && A>=U ], cost: 3-U+A
     51: f42 -> [17] : B'=-1+B, K'=-O*free_46+free_44, L'=free_41, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_54, T'=O*free_46, U'=1+A, [ K*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+K*free_41 && free_47>=1 && B>=C && free_42*P>=free_51*free_47 && free_51+free_51*free_47>=1+free_42*P && free_51>=free_43 && free_42*P>=free_53*free_47 && free_53*free_47+free_53>=1+free_42*P && free_43>=free_53 && K>=free_48*free_47 && free_48+free_48*free_47>=1+K && free_48>=free_45 && K>=free_50*free_47 && free_50+free_50*free_47>=1+K && free_45>=free_50 && free_42*P*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*P*free_41 && free_52>=free_40 && free_42*P*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*P*free_41 && free_40>=free_49 && A>=U ], cost: 3-U+A
     52: f42 -> [17] : [], cost: 0
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     44: [17] -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: [17] -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: [17] -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: [17] -> f75 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C && B>=C && 0==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     53: f15 -> f75 : D'=C, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     59: f15 -> f75 : D'=C, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     54: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_8, L'=free_9, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E ], cost: 3-D+A
     55: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_10, L'=free_11, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 ], cost: 3-D+A
     57: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_8, L'=free_9, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E ], cost: 3-D+A
     58: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=30, K'=free_12, L'=free_13, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && E==30 ], cost: 3-D+A
     60: f15 -> f32 : D'=A, E'=1+E, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, J'=E, K'=free_8, L'=free_9, [ free_5>=1 && A>=1+D && A>=A && C>=1+A && 29>=E ], cost: 3-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_6+free_7, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     65: f32 -> [17] : B'=-1+B, K'=-free_32+free_30, L'=free_27, M'=free_16, N'=free_16, O'=free_31, P'=free_29, Q_1'=free_26, S'=free_54, T'=free_32, U'=1+A, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 && -(free_17-free_14-free_15)*free_27>=free_33*free_30*free_27 && free_33*free_30*free_27+free_30>=1-(free_17-free_14-free_15)*free_27 && 0>=1+free_33 && B>=C && free_28>=free_33*free_37 && free_33*free_37+free_37>=1+free_28 && free_37>=free_29 && free_28>=free_39*free_33 && free_39+free_39*free_33>=1+free_28 && free_29>=free_39 && -free_17+free_14+free_15>=free_33*free_34 && free_33*free_34+free_34>=1-free_17+free_14+free_15 && free_34>=free_31 && -free_17+free_14+free_15>=free_36*free_33 && free_36+free_36*free_33>=1-free_17+free_14+free_15 && free_31>=free_36 && free_27*free_28>=free_33*free_27*free_38 && free_33*free_27*free_38+free_38>=1+free_27*free_28 && free_38>=free_26 && free_27*free_28>=free_35*free_33*free_27 && free_35+free_35*free_33*free_27>=1+free_27*free_28 && free_26>=free_35 && A>=U ], cost: 4-U+A
     66: f32 -> [17] : B'=-1+B, K'=-free_46+free_44, L'=free_41, M'=free_16, N'=free_16, O'=free_45, P'=free_43, Q_1'=free_40, S'=free_54, T'=free_46, U'=1+A, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 && -(free_17-free_14-free_15)*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1-(free_17-free_14-free_15)*free_41 && free_47>=1 && B>=C && free_42>=free_51*free_47 && free_51+free_51*free_47>=1+free_42 && free_51>=free_43 && free_42>=free_53*free_47 && free_53*free_47+free_53>=1+free_42 && free_43>=free_53 && -free_17+free_14+free_15>=free_48*free_47 && free_48+free_48*free_47>=1-free_17+free_14+free_15 && free_48>=free_45 && -free_17+free_14+free_15>=free_50*free_47 && free_50+free_50*free_47>=1-free_17+free_14+free_15 && free_45>=free_50 && free_42*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*free_41 && free_52>=free_40 && free_42*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*free_41 && free_40>=free_49 && A>=U ], cost: 4-U+A
     67: f32 -> [17] : K'=-free_17+free_14+free_15, M'=free_16, N'=free_16, O'=1, P'=1, Q_1'=0, [ K>=0 && K*free_14+free_14*free_16<=-1+K*free_14+free_14*free_16+free_14 ], cost: 1
     69: f32 -> [17] : B'=-1+B, K'=-free_46+free_44, L'=free_41, N'=-free_21, O'=free_45, P'=free_43, Q_1'=free_40, R'=free_21, S'=free_54, T'=free_46, U'=1+A, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 && (free_20-free_22+free_19)*free_41>=free_47*free_41*free_44 && free_47*free_41*free_44+free_44>=1+(free_20-free_22+free_19)*free_41 && free_47>=1 && B>=C && free_42>=free_51*free_47 && free_51+free_51*free_47>=1+free_42 && free_51>=free_43 && free_42>=free_53*free_47 && free_53*free_47+free_53>=1+free_42 && free_43>=free_53 && free_20-free_22+free_19>=free_48*free_47 && free_48+free_48*free_47>=1+free_20-free_22+free_19 && free_48>=free_45 && free_20-free_22+free_19>=free_50*free_47 && free_50+free_50*free_47>=1+free_20-free_22+free_19 && free_45>=free_50 && free_42*free_41>=free_52*free_47*free_41 && free_52*free_47*free_41+free_52>=1+free_42*free_41 && free_52>=free_40 && free_42*free_41>=free_49*free_47*free_41 && free_49+free_49*free_47*free_41>=1+free_42*free_41 && free_40>=free_49 && A>=U ], cost: 4-U+A
     70: f32 -> [17] : K'=free_20-free_22+free_19, N'=-free_21, O'=1, P'=1, Q_1'=0, R'=free_21, [ 0>=1+K && -free_21*free_19+K*free_19<=-1-free_21*free_19+free_19+K*free_19 ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     44: [17] -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: [17] -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: [17] -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: [17] -> f75 : L'=0, S'=free_24*P, T'=O*free_25, [ B>=C && B>=C && 0==0 ], cost: 2