Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f76 -> f78 : A'=0, [ A==0 ], cost: 1
     12: f76 -> f78 : K'=1, [ 0>=1+A ], cost: 1
     13: f76 -> f78 : K'=1, [ A>=1 ], cost: 1
      7: f78 -> f82 : [ 0>=1+K ], cost: 1
      8: f78 -> f82 : [ K>=1 ], cost: 1
     24: f78 -> f82 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f91 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f91 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     35: f44 -> f44 : H'=free_21, N'=H, V'=0, W'=0, X'=0, [ V==0 ], cost: 1
     33: f44 -> f51 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: f44 -> f51 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     36: f44 -> f91 : C'=1, N'=H, W'=free_22, X'=free_22, [ 0>=1+free_22 ], cost: 1
     37: f44 -> f91 : C'=1, N'=H, W'=free_23, X'=free_23, [ free_23>=1 ], cost: 1
     16: f59 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f59 -> f64 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f59 -> f64 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f64 -> f78 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f64 -> f82 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f64 -> f82 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f82 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f82 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f82 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f75 -> f76 : [ 0>=1+M ], cost: 1
     10: f75 -> f76 : [ M>=1 ], cost: 1
     11: f75 -> f78 : M'=0, [ M==0 ], cost: 1
     14: f51 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f51 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f51 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f51 -> f59 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f51 -> f59 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     18: f91 -> f91 : [], cost: 1
     21: f93 -> f95 : [], cost: 1
     39: f0 -> f34 : B'=free_28, C'=free_29, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 ], cost: 1
     40: f0 -> f34 : B'=free_34, C'=free_36, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 ], cost: 1
     41: f0 -> f34 : B'=free_40, C'=free_41, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 ], cost: 1
     38: f0 -> f91 : C'=1, V'=free_25, Y'=free_26, Z'=free_26, A1'=free_27, B1'=free_27, C1'=free_24, D1'=free_25, [ 0>=free_27 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f76 -> f78 : A'=0, [ A==0 ], cost: 1
     12: f76 -> f78 : K'=1, [ 0>=1+A ], cost: 1
     13: f76 -> f78 : K'=1, [ A>=1 ], cost: 1
      7: f78 -> f82 : [ 0>=1+K ], cost: 1
      8: f78 -> f82 : [ K>=1 ], cost: 1
     24: f78 -> f82 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f91 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f91 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     35: f44 -> f44 : H'=free_21, N'=H, V'=0, W'=0, X'=0, [ V==0 ], cost: 1
     33: f44 -> f51 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: f44 -> f51 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     36: f44 -> f91 : C'=1, N'=H, W'=free_22, X'=free_22, [ 0>=1+free_22 ], cost: 1
     37: f44 -> f91 : C'=1, N'=H, W'=free_23, X'=free_23, [ free_23>=1 ], cost: 1
     16: f59 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f59 -> f64 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f59 -> f64 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f64 -> f78 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f64 -> f82 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f64 -> f82 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f82 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f82 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f82 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f75 -> f76 : [ 0>=1+M ], cost: 1
     10: f75 -> f76 : [ M>=1 ], cost: 1
     11: f75 -> f78 : M'=0, [ M==0 ], cost: 1
     14: f51 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f51 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f51 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f51 -> f59 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f51 -> f59 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     18: f91 -> f91 : [], cost: 1
     39: f0 -> f34 : B'=free_28, C'=free_29, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 ], cost: 1
     40: f0 -> f34 : B'=free_34, C'=free_36, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 ], cost: 1
     41: f0 -> f34 : B'=free_40, C'=free_41, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 ], cost: 1
     38: f0 -> f91 : C'=1, V'=free_25, Y'=free_26, Z'=free_26, A1'=free_27, B1'=free_27, C1'=free_24, D1'=free_25, [ 0>=free_27 ], cost: 1

Eliminating 1 self-loops for location f44
  Self-Loop 35 has unbounded runtime, resulting in the new transition 42.
  Removing the self-loops: 35.
Eliminating 1 self-loops for location f91
  Self-Loop 18 has unbounded runtime, resulting in the new transition 43.
  Removing the self-loops: 18.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f76 -> f78 : A'=0, [ A==0 ], cost: 1
     12: f76 -> f78 : K'=1, [ 0>=1+A ], cost: 1
     13: f76 -> f78 : K'=1, [ A>=1 ], cost: 1
      7: f78 -> f82 : [ 0>=1+K ], cost: 1
      8: f78 -> f82 : [ K>=1 ], cost: 1
     24: f78 -> f82 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f91 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f91 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     42: f44 -> [14] : [ V==0 ], cost: INF
     16: f59 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f59 -> f64 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f59 -> f64 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f64 -> f78 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f64 -> f82 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f64 -> f82 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f64 -> f75 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f82 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f82 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f82 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f75 -> f76 : [ 0>=1+M ], cost: 1
     10: f75 -> f76 : [ M>=1 ], cost: 1
     11: f75 -> f78 : M'=0, [ M==0 ], cost: 1
     14: f51 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f51 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f51 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f51 -> f59 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f51 -> f59 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     43: f91 -> [15] : [], cost: INF
     39: f0 -> f34 : B'=free_28, C'=free_29, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 ], cost: 1
     40: f0 -> f34 : B'=free_34, C'=free_36, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 ], cost: 1
     41: f0 -> f34 : B'=free_40, C'=free_41, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 ], cost: 1
     38: f0 -> f91 : C'=1, V'=free_25, Y'=free_26, Z'=free_26, A1'=free_27, B1'=free_27, C1'=free_24, D1'=free_25, [ 0>=free_27 ], cost: 1
     33: [14] -> f51 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: [14] -> f51 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     36: [14] -> f91 : C'=1, N'=H, W'=free_22, X'=free_22, [ 0>=1+free_22 ], cost: 1
     37: [14] -> f91 : C'=1, N'=H, W'=free_23, X'=free_23, [ free_23>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f91 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     55: f44 -> f91 : C'=1, N'=H, W'=free_22, X'=free_22, [ V==0 && 0>=1+free_22 ], cost: INF
     56: f44 -> f91 : C'=1, N'=H, W'=free_23, X'=free_23, [ V==0 && free_23>=1 ], cost: INF
     53: f44 -> [16] : [ V==0 ], cost: INF
     54: f44 -> [17] : [ V==0 ], cost: INF
     43: f91 -> [15] : [], cost: INF
     44: f0 -> f39 : B'=free_28, C'=1, D'=free_28, E'=free, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 ], cost: 2
     45: f0 -> f39 : B'=free_28, C'=1, D'=free_28, E'=free_1, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 ], cost: 2
     47: f0 -> f39 : B'=free_34, C'=1, D'=free_34, E'=free, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 ], cost: 2
     48: f0 -> f39 : B'=free_34, C'=1, D'=free_34, E'=free_1, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && free_34>=1 ], cost: 2
     51: f0 -> f39 : B'=free_40, C'=1, D'=free_40, E'=free_1, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 && free_40>=1 ], cost: 2
     38: f0 -> f91 : C'=1, V'=free_25, Y'=free_26, Z'=free_26, A1'=free_27, B1'=free_27, C1'=free_24, D1'=free_25, [ 0>=free_27 ], cost: 1
     46: f0 -> f91 : B'=0, C'=1, D'=0, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28==0 ], cost: 2
     49: f0 -> f91 : B'=0, C'=1, D'=0, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && free_34==0 ], cost: 2
     52: f0 -> f91 : B'=0, C'=1, D'=0, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 && free_40==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     55: f44 -> f91 : C'=1, N'=H, W'=free_22, X'=free_22, [ V==0 && 0>=1+free_22 ], cost: INF
     56: f44 -> f91 : C'=1, N'=H, W'=free_23, X'=free_23, [ V==0 && free_23>=1 ], cost: INF
     53: f44 -> [16] : [ V==0 ], cost: INF
     54: f44 -> [17] : [ V==0 ], cost: INF
     43: f91 -> [15] : [], cost: INF
     57: f0 -> f44 : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free ], cost: 3
     58: f0 -> f44 : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 ], cost: 3
     61: f0 -> f44 : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 ], cost: 3
     63: f0 -> f44 : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free ], cost: 3
     64: f0 -> f44 : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 ], cost: 3
     38: f0 -> f91 : C'=1, V'=free_25, Y'=free_26, Z'=free_26, A1'=free_27, B1'=free_27, C1'=free_24, D1'=free_25, [ 0>=free_27 ], cost: 1
     46: f0 -> f91 : B'=0, C'=1, D'=0, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28==0 ], cost: 2
     52: f0 -> f91 : B'=0, C'=1, D'=0, V'=free_42, Y'=free_43, Z'=20, A1'=free_45, B1'=free_45, C1'=free_41, D1'=free_42, E1'=free_44, [ free_45>=1 && free_44>=21 && free_40==0 ], cost: 2
     59: f0 -> f91 : B'=free_28, C'=1, D'=free_28, E'=0, F'=0, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free==0 ], cost: 3
     65: f0 -> f91 : B'=free_34, C'=1, D'=free_34, E'=0, F'=0, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
     43: f91 -> [15] : [], cost: INF
     76: f0 -> f91 : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     77: f0 -> f91 : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_23, X'=free_23, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && free_23>=1 ], cost: INF
     80: f0 -> f91 : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     85: f0 -> f91 : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 && free_23>=1 ], cost: INF
     89: f0 -> f91 : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 && free_23>=1 ], cost: INF
     74: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     78: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     82: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     86: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     90: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF
     75: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     79: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     83: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     87: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     91: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     92: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     93: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_23, X'=free_23, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && free_23>=1 ], cost: INF
     94: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     95: f0 -> [15] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 && free_23>=1 ], cost: INF
     96: f0 -> [15] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 && free_23>=1 ], cost: INF
     74: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     78: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     82: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     86: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     90: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF
     75: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     79: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     83: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     87: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     91: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     92: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     93: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_23, X'=free_23, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && free_23>=1 ], cost: INF
     94: f0 -> [15] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_30, W'=free_22, X'=free_22, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 && 0>=1+free_22 ], cost: INF
     95: f0 -> [15] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 && free_23>=1 ], cost: INF
     96: f0 -> [15] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_38, W'=free_23, X'=free_23, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 && free_23>=1 ], cost: INF
     74: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     78: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     82: f0 -> [16] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     86: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     90: f0 -> [16] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF
     75: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_2, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && 0>=1+free && free_30==0 ], cost: INF
     79: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free, F'=free, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 ], cost: INF
     83: f0 -> [17] : B'=free_28, C'=1, D'=free_28, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_30, Y'=free_31, Z'=5, A1'=free_33, B1'=free_33, C1'=free_29, D1'=free_30, E1'=free_32, [ free_33>=1 && 4>=free_32 && free_28>=1 && free_1>=1 && free_30==0 ], cost: INF
     87: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_2, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && 0>=1+free && free_38==0 ], cost: INF
     91: f0 -> [17] : B'=free_34, C'=1, D'=free_34, E'=free, F'=free, G'=10, H'=free_3, V'=free_38, Y'=free_37, Z'=free_39, A1'=free_35, B1'=free_35, C1'=free_36, D1'=free_38, E1'=free_39, [ free_35>=1 && 20>=free_39 && free_39>=5 && 0>=1+free_34 && free>=1 && free_38==0 ], cost: INF


Computing complexity for remaining 15 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_33>=1 && 4>=free_32 && 0>=1+free_28 && free>=1 && free_30==0 && 0>=1+free_22
  Final Cost:  INF

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

WORST_CASE(INF,?)