Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f154 -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f154 -> f156 : B'=A, C'=free, [ 6>=A ], cost: 1
      2: f154 -> f156 : B'=A, C'=free_1, [ A>=8 ], cost: 1
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     22: f156 -> f154 : A'=free_17, A1'=free_16, B1'=-1, C1'=free_17, [ C>=1 && 0>=E ], cost: 1
     23: f156 -> f154 : A'=free_19, A1'=free_18, B1'=-1, C1'=free_19, [ 0>=D && C>=1 && E>=1 ], cost: 1
     21: f156 -> f166 : Y'=1, Z'=free_15, [ 0>=C ], cost: 1
      4: f156 -> f159 : [ D>=1 && C>=1 && E>=1 ], cost: 1
      3: f159 -> f159 : [], cost: 1
      5: f187 -> f190 : B'=7, F'=free_2, G'=free_2, [ B==7 ], cost: 1
      8: f187 -> f115 : [ 6>=B ], cost: 1
      9: f187 -> f115 : [ B>=8 ], cost: 1
      6: f190 -> f200 : H'=free_3, [ 0>=G ], cost: 1
     15: f190 -> f200 : H'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 ], cost: 1
      7: f200 -> f115 : Q'=H, [ H==Q ], cost: 1
     10: f200 -> f115 : J'=1, [ H>=1+Q ], cost: 1
     11: f200 -> f115 : J'=1, [ Q>=1+H ], cost: 1
     30: f115 -> f208 : U1'=0, V1'=free_39, [ J>=1 ], cost: 1
     27: f115 -> f133 : M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 ], cost: 1
     28: f115 -> f133 : M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 ], cost: 1
     29: f115 -> f133 : M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 ], cost: 1
     12: f208 -> f208 : [], cost: 1
     13: f161 -> f213 : [], cost: 1
     14: f210 -> f213 : [], cost: 1
     16: f177 -> f187 : O'=P, Q_1'=P, R'=free_6, [ 3>=B ], cost: 1
     17: f177 -> f187 : O'=P, Q_1'=P, R'=free_7, [ B>=5 ], cost: 1
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     24: f133 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, [ 0>=D1 ], cost: 1
     25: f133 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, [ D1>=2 ], cost: 1
     26: f133 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, [ D1==1 ], cost: 1
     32: f100 -> f115 : D2'=8, [ 0>=W1 ], cost: 1
     31: f100 -> f100 : W1'=-1+W1, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=W, C2'=free_40, [ W1>=1 ], cost: 1
     33: f0 -> f100 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=free_59, D2'=9, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 ], cost: 1
     34: f0 -> f100 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=free_67, D2'=9, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 ], cost: 1
     35: f0 -> f100 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=free_90, D2'=9, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f154 -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f154 -> f156 : B'=A, C'=free, [ 6>=A ], cost: 1
      2: f154 -> f156 : B'=A, C'=free_1, [ A>=8 ], cost: 1
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     22: f156 -> f154 : A'=free_17, A1'=free_16, B1'=-1, C1'=free_17, [ C>=1 && 0>=E ], cost: 1
     23: f156 -> f154 : A'=free_19, A1'=free_18, B1'=-1, C1'=free_19, [ 0>=D && C>=1 && E>=1 ], cost: 1
     21: f156 -> f166 : Y'=1, Z'=free_15, [ 0>=C ], cost: 1
      4: f156 -> f159 : [ D>=1 && C>=1 && E>=1 ], cost: 1
      3: f159 -> f159 : [], cost: 1
      5: f187 -> f190 : B'=7, F'=free_2, G'=free_2, [ B==7 ], cost: 1
      8: f187 -> f115 : [ 6>=B ], cost: 1
      9: f187 -> f115 : [ B>=8 ], cost: 1
      6: f190 -> f200 : H'=free_3, [ 0>=G ], cost: 1
     15: f190 -> f200 : H'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 ], cost: 1
      7: f200 -> f115 : Q'=H, [ H==Q ], cost: 1
     10: f200 -> f115 : J'=1, [ H>=1+Q ], cost: 1
     11: f200 -> f115 : J'=1, [ Q>=1+H ], cost: 1
     30: f115 -> f208 : U1'=0, V1'=free_39, [ J>=1 ], cost: 1
     27: f115 -> f133 : M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 ], cost: 1
     28: f115 -> f133 : M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 ], cost: 1
     29: f115 -> f133 : M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 ], cost: 1
     12: f208 -> f208 : [], cost: 1
     16: f177 -> f187 : O'=P, Q_1'=P, R'=free_6, [ 3>=B ], cost: 1
     17: f177 -> f187 : O'=P, Q_1'=P, R'=free_7, [ B>=5 ], cost: 1
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     24: f133 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, [ 0>=D1 ], cost: 1
     25: f133 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, [ D1>=2 ], cost: 1
     26: f133 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, [ D1==1 ], cost: 1
     32: f100 -> f115 : D2'=8, [ 0>=W1 ], cost: 1
     31: f100 -> f100 : W1'=-1+W1, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=W, C2'=free_40, [ W1>=1 ], cost: 1
     33: f0 -> f100 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=free_59, D2'=9, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 ], cost: 1
     34: f0 -> f100 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=free_67, D2'=9, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 ], cost: 1
     35: f0 -> f100 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=free_90, D2'=9, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 ], cost: 1

Eliminating 1 self-loops for location f159
  Self-Loop 3 has unbounded runtime, resulting in the new transition 36.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f208
  Self-Loop 12 has unbounded runtime, resulting in the new transition 37.
  Removing the self-loops: 12.
Eliminating 1 self-loops for location f100
  Self-Loop 31 has the metering function: W1, resulting in the new transition 38.
  Removing the self-loops: 31.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f154 -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f154 -> f156 : B'=A, C'=free, [ 6>=A ], cost: 1
      2: f154 -> f156 : B'=A, C'=free_1, [ A>=8 ], cost: 1
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     22: f156 -> f154 : A'=free_17, A1'=free_16, B1'=-1, C1'=free_17, [ C>=1 && 0>=E ], cost: 1
     23: f156 -> f154 : A'=free_19, A1'=free_18, B1'=-1, C1'=free_19, [ 0>=D && C>=1 && E>=1 ], cost: 1
     21: f156 -> f166 : Y'=1, Z'=free_15, [ 0>=C ], cost: 1
      4: f156 -> f159 : [ D>=1 && C>=1 && E>=1 ], cost: 1
     36: f159 -> [16] : [], cost: INF
      5: f187 -> f190 : B'=7, F'=free_2, G'=free_2, [ B==7 ], cost: 1
      8: f187 -> f115 : [ 6>=B ], cost: 1
      9: f187 -> f115 : [ B>=8 ], cost: 1
      6: f190 -> f200 : H'=free_3, [ 0>=G ], cost: 1
     15: f190 -> f200 : H'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 ], cost: 1
      7: f200 -> f115 : Q'=H, [ H==Q ], cost: 1
     10: f200 -> f115 : J'=1, [ H>=1+Q ], cost: 1
     11: f200 -> f115 : J'=1, [ Q>=1+H ], cost: 1
     30: f115 -> f208 : U1'=0, V1'=free_39, [ J>=1 ], cost: 1
     27: f115 -> f133 : M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 ], cost: 1
     28: f115 -> f133 : M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 ], cost: 1
     29: f115 -> f133 : M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 ], cost: 1
     37: f208 -> [17] : [], cost: INF
     16: f177 -> f187 : O'=P, Q_1'=P, R'=free_6, [ 3>=B ], cost: 1
     17: f177 -> f187 : O'=P, Q_1'=P, R'=free_7, [ B>=5 ], cost: 1
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     24: f133 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, [ 0>=D1 ], cost: 1
     25: f133 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, [ D1>=2 ], cost: 1
     26: f133 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, [ D1==1 ], cost: 1
     38: f100 -> [18] : W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=W, C2'=free_40, [ W1>=1 ], cost: W1
     33: f0 -> f100 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=free_59, D2'=9, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 ], cost: 1
     34: f0 -> f100 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=free_67, D2'=9, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 ], cost: 1
     35: f0 -> f100 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=free_90, D2'=9, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 ], cost: 1
     32: [18] -> f115 : D2'=8, [ 0>=W1 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f154 -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
      1: f154 -> f156 : B'=A, C'=free, [ 6>=A ], cost: 1
      2: f154 -> f156 : B'=A, C'=free_1, [ A>=8 ], cost: 1
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     22: f156 -> f154 : A'=free_17, A1'=free_16, B1'=-1, C1'=free_17, [ C>=1 && 0>=E ], cost: 1
     23: f156 -> f154 : A'=free_19, A1'=free_18, B1'=-1, C1'=free_19, [ 0>=D && C>=1 && E>=1 ], cost: 1
     21: f156 -> f166 : Y'=1, Z'=free_15, [ 0>=C ], cost: 1
      4: f156 -> [16] : [ D>=1 && C>=1 && E>=1 ], cost: INF
      5: f187 -> f190 : B'=7, F'=free_2, G'=free_2, [ B==7 ], cost: 1
      8: f187 -> f115 : [ 6>=B ], cost: 1
      9: f187 -> f115 : [ B>=8 ], cost: 1
      6: f190 -> f200 : H'=free_3, [ 0>=G ], cost: 1
     15: f190 -> f200 : H'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 ], cost: 1
      7: f200 -> f115 : Q'=H, [ H==Q ], cost: 1
     10: f200 -> f115 : J'=1, [ H>=1+Q ], cost: 1
     11: f200 -> f115 : J'=1, [ Q>=1+H ], cost: 1
     27: f115 -> f133 : M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 ], cost: 1
     28: f115 -> f133 : M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 ], cost: 1
     29: f115 -> f133 : M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 ], cost: 1
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     16: f177 -> f187 : O'=P, Q_1'=P, R'=free_6, [ 3>=B ], cost: 1
     17: f177 -> f187 : O'=P, Q_1'=P, R'=free_7, [ B>=5 ], cost: 1
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     24: f133 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, [ 0>=D1 ], cost: 1
     25: f133 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, [ D1>=2 ], cost: 1
     26: f133 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, [ D1==1 ], cost: 1
     38: f100 -> f115 : W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=W, C2'=free_40, D2'=8, [ W1>=1 && 0>=0 ], cost: 1+W1
     33: f0 -> f100 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=free_59, D2'=9, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 ], cost: 1
     34: f0 -> f100 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=free_67, D2'=9, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 ], cost: 1
     35: f0 -> f100 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=free_90, D2'=9, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     51: f154 -> f154 : A'=free_17, B'=A, C'=free, A1'=free_16, B1'=-1, C1'=free_17, [ 6>=A && free>=1 && 0>=E ], cost: 2
     52: f154 -> f154 : A'=free_19, B'=A, C'=free, A1'=free_18, B1'=-1, C1'=free_19, [ 6>=A && 0>=D && free>=1 && E>=1 ], cost: 2
     55: f154 -> f154 : A'=free_17, B'=A, C'=free_1, A1'=free_16, B1'=-1, C1'=free_17, [ A>=8 && free_1>=1 && 0>=E ], cost: 2
     56: f154 -> f154 : A'=free_19, B'=A, C'=free_1, A1'=free_18, B1'=-1, C1'=free_19, [ A>=8 && 0>=D && free_1>=1 && E>=1 ], cost: 2
      0: f154 -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
     53: f154 -> f166 : B'=A, C'=free, Y'=1, Z'=free_15, [ 6>=A && 0>=free ], cost: 2
     57: f154 -> f166 : B'=A, C'=free_1, Y'=1, Z'=free_15, [ A>=8 && 0>=free_1 ], cost: 2
     54: f154 -> [16] : B'=A, C'=free, [ 6>=A && D>=1 && free>=1 && E>=1 ], cost: INF
     58: f154 -> [16] : B'=A, C'=free_1, [ A>=8 && D>=1 && free_1>=1 && E>=1 ], cost: INF
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     63: f190 -> f115 : H'=free_3, Q'=free_3, [ 0>=G && free_3==Q ], cost: 2
     64: f190 -> f115 : H'=free_3, J'=1, [ 0>=G && free_3>=1+Q ], cost: 2
     65: f190 -> f115 : H'=free_3, J'=1, [ 0>=G && Q>=1+free_3 ], cost: 2
     66: f190 -> f115 : H'=free_5, Q'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 && free_5==Q ], cost: 2
     68: f190 -> f115 : H'=free_5, J'=1, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 && Q>=1+free_5 ], cost: 2
     42: f115 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 ], cost: 2
     43: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1>=2 ], cost: 2
     45: f115 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && 0>=D1 ], cost: 2
     46: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1>=2 ], cost: 2
     49: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 && D1>=2 ], cost: 2
     44: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 ], cost: 2
     47: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 ], cost: 2
     50: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 && D1==1 ], cost: 2
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     60: f177 -> f190 : B'=7, F'=free_2, G'=free_2, O'=P, Q_1'=P, R'=free_7, [ B>=5 && B==7 ], cost: 2
     59: f177 -> f115 : O'=P, Q_1'=P, R'=free_6, [ 3>=B && 6>=B ], cost: 2
     61: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && 6>=B ], cost: 2
     62: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && B>=8 ], cost: 2
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90

Eliminating 4 self-loops for location f154
  Removing the self-loops: 51 52 55 56.
Adding an epsilon transition (to model nonexecution of the loops): 73.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     69: f154 -> [19] : A'=free_17, B'=A, C'=free, A1'=free_16, B1'=-1, C1'=free_17, [ 6>=A && free>=1 && 0>=E ], cost: 2
     70: f154 -> [19] : A'=free_19, B'=A, C'=free, A1'=free_18, B1'=-1, C1'=free_19, [ 6>=A && 0>=D && free>=1 && E>=1 ], cost: 2
     71: f154 -> [19] : A'=free_17, B'=A, C'=free_1, A1'=free_16, B1'=-1, C1'=free_17, [ A>=8 && free_1>=1 && 0>=E ], cost: 2
     72: f154 -> [19] : A'=free_19, B'=A, C'=free_1, A1'=free_18, B1'=-1, C1'=free_19, [ A>=8 && 0>=D && free_1>=1 && E>=1 ], cost: 2
     73: f154 -> [19] : [], cost: 0
     19: f166 -> f177 : B'=free_11, P'=free_12, W'=1, X'=free_12, [ U>=1+V ], cost: 1
     20: f166 -> f177 : B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ V>=U ], cost: 1
     63: f190 -> f115 : H'=free_3, Q'=free_3, [ 0>=G && free_3==Q ], cost: 2
     64: f190 -> f115 : H'=free_3, J'=1, [ 0>=G && free_3>=1+Q ], cost: 2
     65: f190 -> f115 : H'=free_3, J'=1, [ 0>=G && Q>=1+free_3 ], cost: 2
     66: f190 -> f115 : H'=free_5, Q'=free_5, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 && free_5==Q ], cost: 2
     68: f190 -> f115 : H'=free_5, J'=1, K'=1, L'=G, M'=free_4, N'=G, [ G>=1 && Q>=1+free_5 ], cost: 2
     42: f115 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 ], cost: 2
     43: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1>=2 ], cost: 2
     45: f115 -> f154 : A'=free_21, A1'=free_20, B1'=-1, C1'=free_21, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && 0>=D1 ], cost: 2
     46: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1>=2 ], cost: 2
     49: f115 -> f154 : A'=free_25, A1'=free_24, B1'=-1, C1'=free_25, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 && D1>=2 ], cost: 2
     44: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 ], cost: 2
     47: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 ], cost: 2
     50: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 && D1==1 ], cost: 2
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     18: f177 -> f190 : B'=4, F'=free_8, G'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 ], cost: 1
     60: f177 -> f190 : B'=7, F'=free_2, G'=free_2, O'=P, Q_1'=P, R'=free_7, [ B>=5 && B==7 ], cost: 2
     59: f177 -> f115 : O'=P, Q_1'=P, R'=free_6, [ 3>=B && 6>=B ], cost: 2
     61: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && 6>=B ], cost: 2
     62: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && B>=8 ], cost: 2
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
      0: [19] -> f166 : A'=7, B'=7, [ A==7 ], cost: 1
     53: [19] -> f166 : B'=A, C'=free, Y'=1, Z'=free_15, [ 6>=A && 0>=free ], cost: 2
     57: [19] -> f166 : B'=A, C'=free_1, Y'=1, Z'=free_15, [ A>=8 && 0>=free_1 ], cost: 2
     54: [19] -> [16] : B'=A, C'=free, [ 6>=A && D>=1 && free>=1 && E>=1 ], cost: INF
     58: [19] -> [16] : B'=A, C'=free_1, [ A>=8 && D>=1 && free_1>=1 && E>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     44: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 ], cost: 2
     47: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 ], cost: 2
     50: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_37, N1'=free_36, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, S1'=0, T1'=free_38, [ L1>=1 && 0>=J && Q1_1>=L1 && D1==1 ], cost: 2
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     74: f115 -> [19] : A'=free_17, B'=free_21, C'=free, A1'=free_16, B1'=-1, C1'=free_17, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && 6>=free_21 && free>=1 && 0>=E ], cost: 4
     75: f115 -> [19] : A'=free_19, B'=free_21, C'=free, A1'=free_18, B1'=-1, C1'=free_19, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && 6>=free_21 && 0>=D && free>=1 && E>=1 ], cost: 4
     77: f115 -> [19] : A'=free_19, B'=free_21, C'=free_1, A1'=free_18, B1'=-1, C1'=free_19, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && free_21>=8 && 0>=D && free_1>=1 && E>=1 ], cost: 4
     81: f115 -> [19] : A'=free_17, B'=free_25, C'=free_1, A1'=free_16, B1'=-1, C1'=free_17, E1'=0, F1'=free_26, G1'=free_26, H1'=free_26, Q1'=free_26, J1'=free_27, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1>=2 && free_25>=8 && free_1>=1 && 0>=E ], cost: 4
     86: f115 -> [19] : A'=free_17, B'=free_21, C'=free_1, A1'=free_16, B1'=-1, C1'=free_17, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && 0>=D1 && free_21>=8 && free_1>=1 && 0>=E ], cost: 4
     59: f177 -> f115 : O'=P, Q_1'=P, R'=free_6, [ 3>=B && 6>=B ], cost: 2
     61: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && 6>=B ], cost: 2
     99: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_3, Q'=free_3, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && 0>=free_8 && free_3==Q ], cost: 3
    102: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_5, Q'=free_5, K'=1, L'=free_8, M'=free_4, N'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && free_8>=1 && free_5==Q ], cost: 3
    103: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_5, J'=1, K'=1, L'=free_8, M'=free_4, N'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && free_8>=1 && Q>=1+free_5 ], cost: 3
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
    109: [19] -> f177 : A'=7, B'=free_11, P'=free_12, W'=1, X'=free_12, [ A==7 && U>=1+V ], cost: 2
    110: [19] -> f177 : A'=7, B'=free_13, P'=free_14, V'=0, W'=1, X'=free_14, [ A==7 && V>=U ], cost: 2
    111: [19] -> f177 : B'=free_11, C'=free, P'=free_12, W'=1, X'=free_12, Y'=1, Z'=free_15, [ 6>=A && 0>=free && U>=1+V ], cost: 3
    112: [19] -> f177 : B'=free_13, C'=free, P'=free_14, V'=0, W'=1, X'=free_14, Y'=1, Z'=free_15, [ 6>=A && 0>=free && V>=U ], cost: 3
    114: [19] -> f177 : B'=free_13, C'=free_1, P'=free_14, V'=0, W'=1, X'=free_14, Y'=1, Z'=free_15, [ A>=8 && 0>=free_1 && V>=U ], cost: 3
     54: [19] -> [16] : B'=A, C'=free, [ 6>=A && D>=1 && free>=1 && E>=1 ], cost: INF
     58: [19] -> [16] : B'=A, C'=free_1, [ A>=8 && D>=1 && free_1>=1 && E>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     44: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 ], cost: 2
     47: f115 -> f177 : B'=free_30, P'=free_29, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 ], cost: 2
    115: f115 -> f177 : A'=7, B'=free_11, C'=free, P'=free_12, W'=1, X'=free_12, A1'=free_16, B1'=-1, C1'=free_17, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && 6>=free_21 && free>=1 && 0>=E && free_17==7 && U>=1+V ], cost: 6
    119: f115 -> f177 : A'=7, B'=free_13, C'=free, P'=free_14, V'=0, W'=1, X'=free_14, A1'=free_18, B1'=-1, C1'=free_19, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && 6>=free_21 && 0>=D && free>=1 && E>=1 && free_19==7 && V>=U ], cost: 6
    122: f115 -> f177 : A'=7, B'=free_13, C'=free_1, P'=free_14, V'=0, W'=1, X'=free_14, A1'=free_18, B1'=-1, C1'=free_19, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && free_21>=8 && 0>=D && free_1>=1 && E>=1 && free_19==7 && V>=U ], cost: 6
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     59: f177 -> f115 : O'=P, Q_1'=P, R'=free_6, [ 3>=B && 6>=B ], cost: 2
     61: f177 -> f115 : O'=P, Q_1'=P, R'=free_7, [ B>=5 && 6>=B ], cost: 2
     99: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_3, Q'=free_3, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && 0>=free_8 && free_3==Q ], cost: 3
    102: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_5, Q'=free_5, K'=1, L'=free_8, M'=free_4, N'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && free_8>=1 && free_5==Q ], cost: 3
    103: f177 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_5, J'=1, K'=1, L'=free_8, M'=free_4, N'=free_8, O'=P, Q_1'=P, R'=free_9, S'=1, T'=free_10, [ B==4 && free_8>=1 && Q>=1+free_5 ], cost: 3
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90


Applied chaining over branches and pruning:
  Start location: f0
    133: f115 -> f115 : B'=free_30, O'=free_29, P'=free_29, Q_1'=free_29, R'=free_6, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 && 3>=free_30 && 6>=free_30 ], cost: 4
    134: f115 -> f115 : B'=free_30, O'=free_29, P'=free_29, Q_1'=free_29, R'=free_7, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 && free_30>=5 && 6>=free_30 ], cost: 4
    136: f115 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_5, Q'=free_5, K'=1, L'=free_8, M'=free_4, N'=free_8, O'=free_29, P'=free_29, Q_1'=free_29, R'=free_9, S'=1, T'=free_10, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && D1==1 && free_30==4 && free_8>=1 && free_5==Q ], cost: 5
    140: f115 -> f115 : B'=4, F'=free_8, G'=free_8, H'=free_3, Q'=free_3, O'=free_29, P'=free_29, Q_1'=free_29, R'=free_9, S'=1, T'=free_10, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=1+Q1_1, R1'=Q1_1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 && free_30==4 && 0>=free_8 && free_3==Q ], cost: 5
    145: f115 -> f115 : A'=7, B'=4, C'=free, F'=free_8, G'=free_8, H'=free_3, Q'=free_3, O'=free_12, P'=free_12, Q_1'=free_12, R'=free_9, S'=1, T'=free_10, W'=1, X'=free_12, A1'=free_16, B1'=-1, C1'=free_17, E1'=0, F1'=free_22, G1'=free_22, H1'=free_22, Q1'=free_22, J1'=free_23, M1'=free_32, N1'=free_33, O1'=1, P1'=0, [ 0>=J && 0>=L1 && 0>=D1 && 6>=free_21 && free>=1 && 0>=E && free_17==7 && U>=1+V && free_11==4 && 0>=free_8 && free_3==Q ], cost: 9
     30: f115 -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90

Eliminating 5 self-loops for location f115
  Self-Loop 133 has unbounded runtime, resulting in the new transition 158.
  Self-Loop 134 has unbounded runtime, resulting in the new transition 159.
  Self-Loop 136 has unbounded runtime, resulting in the new transition 160.
  Self-Loop 140 has the metering function: L1-Q1_1, resulting in the new transition 161.
  Self-Loop 145 has unbounded runtime, resulting in the new transition 162.
  Removing the self-loops: 133 134 136 140 145.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
    158: f115 -> [20] : [ 0>=J && 0>=L1 && D1==1 && 3>=free_30 ], cost: INF
    159: f115 -> [20] : [ 0>=J && 0>=L1 && D1==1 && free_30>=5 && 6>=free_30 ], cost: INF
    160: f115 -> [20] : [ 0>=J && 0>=L1 && D1==1 && free_8>=1 ], cost: INF
    161: f115 -> [20] : B'=4, F'=free_8, G'=free_8, H'=Q, O'=free_29, P'=free_29, Q_1'=free_29, R'=free_9, S'=1, T'=free_10, W'=K1, X'=free_29, D1'=1, E1'=0, F1'=free_31, G1'=free_31, H1'=free_31, Q1'=free_31, J1'=free_28, M1'=free_34, N1'=free_35, O1'=1, P1'=0, Q1_1'=L1, R1'=-1+L1, [ L1>=1+Q1_1 && 0>=J && L1>=1 && D1==1 && 0>=free_8 ], cost: 5*L1-5*Q1_1
    162: f115 -> [20] : [ 0>=J && 0>=L1 && 0>=D1 && free>=1 && 0>=E && U>=1+V && 0>=free_8 ], cost: INF
     39: f0 -> f115 : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
     40: f0 -> f115 : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
     41: f0 -> f115 : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
     30: [20] -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    163: f0 -> [20] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && 3>=free_30 ], cost: INF
    164: f0 -> [20] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && free_30>=5 && 6>=free_30 ], cost: INF
    169: f0 -> [20] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_30>=5 && 6>=free_30 ], cost: INF
    170: f0 -> [20] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_8>=1 ], cost: INF
    174: f0 -> [20] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 && 0>=0 && 0>=L1 && free_90==1 && free_30>=5 && 6>=free_30 ], cost: INF
    167: f0 -> [21] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
    172: f0 -> [22] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
    177: f0 -> [23] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
     30: [20] -> [17] : U1'=0, V1'=free_39, [ J>=1 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    167: f0 -> [21] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
    172: f0 -> [22] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
    177: f0 -> [23] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
    178: f0 -> [24] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && 3>=free_30 ], cost: INF
    179: f0 -> [25] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && free_30>=5 && 6>=free_30 ], cost: INF
    180: f0 -> [26] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_30>=5 && 6>=free_30 ], cost: INF
    181: f0 -> [27] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_8>=1 ], cost: INF
    182: f0 -> [28] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 && 0>=0 && 0>=L1 && free_90==1 && free_30>=5 && 6>=free_30 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    167: f0 -> [21] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 ], cost: 2+free_59
    172: f0 -> [22] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 ], cost: 2+free_67
    177: f0 -> [23] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 ], cost: 2+free_90
    178: f0 -> [24] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && 3>=free_30 ], cost: INF
    179: f0 -> [25] : B'=7, J'=0, K'=0, V'=0, W'=free_61, D1'=free_59, E1'=0, K1'=free_61, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_61, C2'=free_40, D2'=8, E2'=free_54, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_54, N2'=free_46, O2'=free_46, P2'=free_46, Q2_1'=free_52, R2'=free_45, S2'=free_51, T2'=free_58, U2'=0, V2'=free_43, W2'=free_49, X2'=free_56, Y2'=free_44, Z2'=free_50, A3'=free_57, B3'=0, C3'=0, D3'=free_42, E3'=free_48, F3'=7, G3'=7, H3'=free_55, Q3'=free_41, J3'=free_47, K3'=free_54, L3'=0, M3'=free_53, N3'=1, O3'=0, P3'=D1, Q3_1'=free_60, R3'=0, [ free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0 && 0>=0 && 0>=L1 && free_59==1 && free_30>=5 && 6>=free_30 ], cost: INF
    180: f0 -> [26] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_30>=5 && 6>=free_30 ], cost: INF
    181: f0 -> [27] : B'=free_78, J'=0, K'=0, V'=0, W'=free_84, D1'=free_67, E1'=0, K1'=free_84, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_84, C2'=free_40, D2'=8, E2'=free_77, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_77, N2'=free_68, O2'=free_68, P2'=free_68, Q2_1'=free_75, R2'=free_66, S2'=free_73, T2'=free_81, U2'=0, V2'=free_64, W2'=free_71, X2'=free_79, Y2'=free_65, Z2'=free_72, A3'=free_80, B3'=0, C3'=0, D3'=free_63, E3'=free_70, F3'=free_78, G3'=free_78, H3'=free_69, Q3'=free_76, J3'=free_83, K3'=free_77, L3'=0, M3'=free_82, N3'=1, O3'=0, P3'=D1, Q3_1'=free_74, R3'=0, S3'=1, T3'=free_62, [ free_84>=1 && free_77>=1 && 6>=free_78 && free_67>=1 && free_67>=1 && 0>=0 && 0>=0 && 0>=L1 && free_67==1 && free_8>=1 ], cost: INF
    182: f0 -> [28] : B'=free_101, J'=0, K'=0, V'=0, W'=free_107, D1'=free_90, E1'=0, K1'=free_107, Q1_1'=0, W1'=0, X1'=0, Y1'=6, Z1'=1, A2'=5, B2'=free_107, C2'=free_40, D2'=8, E2'=free_100, F2'=0, G2'=0, H2'=0, Q2'=0, J2'=0, K2'=256, L2'=0, M2'=free_100, N2'=free_91, O2'=free_91, P2'=free_91, Q2_1'=free_98, R2'=free_89, S2'=free_96, T2'=free_104, U2'=0, V2'=free_87, W2'=free_94, X2'=free_102, Y2'=free_88, Z2'=free_95, A3'=free_103, B3'=0, C3'=0, D3'=free_86, E3'=free_93, F3'=free_101, G3'=free_101, H3'=free_92, Q3'=free_99, J3'=free_106, K3'=free_100, L3'=0, M3'=free_105, N3'=1, O3'=0, P3'=D1, Q3_1'=free_97, R3'=0, S3'=1, T3'=free_85, [ free_107>=1 && free_100>=1 && free_101>=8 && free_90>=1 && free_90>=1 && 0>=0 && 0>=0 && 0>=L1 && free_90==1 && free_30>=5 && 6>=free_30 ], cost: INF


Computing complexity for remaining 8 transitions.

  Found configuration with infinitely models for cost: 2+free_59
  and guard: free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0:
  free_54: Pos, free_61: Pos, free_59: Pos

Found new complexity INF, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: free_61>=1 && free_59>=1 && free_54>=1 && free_59>=1 && 0>=0
  Final Cost:  2+free_59

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

WORST_CASE(INF,?)