Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ 0>=D && 0>=A ], cost: 1
      2: f20 -> f26 : B'=0, C'=D, [ D>=1 && 0>=A ], cost: 1
     21: f26 -> f26 : C'=1+C, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 ], cost: 1
      3: f26 -> f68 : [ C>=E ], cost: 1
      4: f26 -> f33 : F'=free_1, G'=free, [ free_1>=1 && E>=1+C ], cost: 1
      5: f26 -> f33 : F'=free_3, G'=free_2, [ E>=1+C && 0>=free_3 && 0>=free_2 ], cost: 1
     27: f68 -> f71 : A'=0, [ 0>=U ], cost: 1
     28: f68 -> f71 : A'=1, [ U>=1 ], cost: 1
      8: f33 -> f33 : Q'=1+Q, [ Q>=H && 0>=2+J ], cost: 1
      9: f33 -> f33 : Q'=1+Q, [ Q>=H && J>=0 ], cost: 1
      6: f33 -> f39 : [ H>=1+Q ], cost: 1
      7: f33 -> f39 : J'=-1, [ Q>=H && 1+J==0 ], cost: 1
     22: f39 -> f26 : C'=1+C, K'=free_20, L'=free_20, [ H>=1+Q && free_20>=1 ], cost: 1
     23: f39 -> f26 : C'=1+C, K'=free_23, L'=free_23, M'=free_21, P'=free_22, [ free_22>=1 && free_21>=1 && H>=1+Q && 0>=free_23 ], cost: 1
     10: f39 -> f68 : [ Q>=H ], cost: 1
     11: f39 -> f52 : K'=free_6, L'=free_6, M'=free_4, N'=free_5, O'=free_5, [ 0>=free_4 && H>=1+Q && 0>=free_6 ], cost: 1
     12: f39 -> f52 : K'=free_10, L'=free_10, M'=free_7, N'=free_9, O'=free_9, P'=free_8, [ 0>=free_8 && free_7>=1 && H>=1+Q && 0>=free_10 ], cost: 1
     24: f52 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     13: f52 -> f68 : Q_1'=3, R'=free_11, [ O>=0 && 0>=free_11 && Q_1==3 ], cost: 1
     14: f52 -> f68 : Q_1'=3, R'=free_12, [ O>=0 && free_12>=2 && Q_1==3 ], cost: 1
     15: f52 -> f59 : S'=free_13, [ O>=0 && 2>=Q_1 ], cost: 1
     16: f52 -> f59 : S'=free_14, [ O>=0 && Q_1>=4 ], cost: 1
     17: f52 -> f59 : Q_1'=3, R'=1, S'=free_15, [ O>=0 && Q_1==3 ], cost: 1
     18: f59 -> f63 : O'=free_16, T'=free_16, [ 10>=S ], cost: 1
     19: f59 -> f63 : O'=free_17, S'=10, T'=free_17, [ S>=11 ], cost: 1
     20: f63 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     25: f63 -> f26 : C'=1+C, J'=L, U'=1+U, [ O>=0 ], cost: 1
     26: f71 -> f71 : [], cost: 1
     29: f73 -> f76 : [], cost: 1
     30: f0 -> f20 : A'=free_26, D'=free_24, E'=free_27, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 ], cost: 1
     31: f0 -> f20 : A'=free_30, D'=free_28, E'=free_31, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 ], cost: 1
     32: f0 -> f20 : A'=free_34, D'=free_32, E'=free_35, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ 0>=D && 0>=A ], cost: 1
      2: f20 -> f26 : B'=0, C'=D, [ D>=1 && 0>=A ], cost: 1
     21: f26 -> f26 : C'=1+C, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 ], cost: 1
      3: f26 -> f68 : [ C>=E ], cost: 1
      4: f26 -> f33 : F'=free_1, G'=free, [ free_1>=1 && E>=1+C ], cost: 1
      5: f26 -> f33 : F'=free_3, G'=free_2, [ E>=1+C && 0>=free_3 && 0>=free_2 ], cost: 1
     27: f68 -> f71 : A'=0, [ 0>=U ], cost: 1
     28: f68 -> f71 : A'=1, [ U>=1 ], cost: 1
      8: f33 -> f33 : Q'=1+Q, [ Q>=H && 0>=2+J ], cost: 1
      9: f33 -> f33 : Q'=1+Q, [ Q>=H && J>=0 ], cost: 1
      6: f33 -> f39 : [ H>=1+Q ], cost: 1
      7: f33 -> f39 : J'=-1, [ Q>=H && 1+J==0 ], cost: 1
     22: f39 -> f26 : C'=1+C, K'=free_20, L'=free_20, [ H>=1+Q && free_20>=1 ], cost: 1
     23: f39 -> f26 : C'=1+C, K'=free_23, L'=free_23, M'=free_21, P'=free_22, [ free_22>=1 && free_21>=1 && H>=1+Q && 0>=free_23 ], cost: 1
     10: f39 -> f68 : [ Q>=H ], cost: 1
     11: f39 -> f52 : K'=free_6, L'=free_6, M'=free_4, N'=free_5, O'=free_5, [ 0>=free_4 && H>=1+Q && 0>=free_6 ], cost: 1
     12: f39 -> f52 : K'=free_10, L'=free_10, M'=free_7, N'=free_9, O'=free_9, P'=free_8, [ 0>=free_8 && free_7>=1 && H>=1+Q && 0>=free_10 ], cost: 1
     24: f52 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     13: f52 -> f68 : Q_1'=3, R'=free_11, [ O>=0 && 0>=free_11 && Q_1==3 ], cost: 1
     14: f52 -> f68 : Q_1'=3, R'=free_12, [ O>=0 && free_12>=2 && Q_1==3 ], cost: 1
     15: f52 -> f59 : S'=free_13, [ O>=0 && 2>=Q_1 ], cost: 1
     16: f52 -> f59 : S'=free_14, [ O>=0 && Q_1>=4 ], cost: 1
     17: f52 -> f59 : Q_1'=3, R'=1, S'=free_15, [ O>=0 && Q_1==3 ], cost: 1
     18: f59 -> f63 : O'=free_16, T'=free_16, [ 10>=S ], cost: 1
     19: f59 -> f63 : O'=free_17, S'=10, T'=free_17, [ S>=11 ], cost: 1
     20: f63 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     25: f63 -> f26 : C'=1+C, J'=L, U'=1+U, [ O>=0 ], cost: 1
     26: f71 -> f71 : [], cost: 1
     30: f0 -> f20 : A'=free_26, D'=free_24, E'=free_27, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 ], cost: 1
     31: f0 -> f20 : A'=free_30, D'=free_28, E'=free_31, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 ], cost: 1
     32: f0 -> f20 : A'=free_34, D'=free_32, E'=free_35, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 ], cost: 1

Eliminating 1 self-loops for location f26
  Self-Loop 21 has the metering function: E-C, resulting in the new transition 33.
  Removing the self-loops: 21.
Eliminating 2 self-loops for location f33
  Self-Loop 8 has unbounded runtime, resulting in the new transition 34.
  Self-Loop 9 has unbounded runtime, resulting in the new transition 35.
  Removing the self-loops: 8 9.
Eliminating 1 self-loops for location f71
  Self-Loop 26 has unbounded runtime, resulting in the new transition 36.
  Removing the self-loops: 26.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ 0>=D && 0>=A ], cost: 1
      2: f20 -> f26 : B'=0, C'=D, [ D>=1 && 0>=A ], cost: 1
     33: f26 -> [12] : C'=E, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 ], cost: E-C
     27: f68 -> f71 : A'=0, [ 0>=U ], cost: 1
     28: f68 -> f71 : A'=1, [ U>=1 ], cost: 1
     34: f33 -> [13] : [ Q>=H && 0>=2+J ], cost: INF
     35: f33 -> [13] : [ Q>=H && J>=0 ], cost: INF
     22: f39 -> f26 : C'=1+C, K'=free_20, L'=free_20, [ H>=1+Q && free_20>=1 ], cost: 1
     23: f39 -> f26 : C'=1+C, K'=free_23, L'=free_23, M'=free_21, P'=free_22, [ free_22>=1 && free_21>=1 && H>=1+Q && 0>=free_23 ], cost: 1
     10: f39 -> f68 : [ Q>=H ], cost: 1
     11: f39 -> f52 : K'=free_6, L'=free_6, M'=free_4, N'=free_5, O'=free_5, [ 0>=free_4 && H>=1+Q && 0>=free_6 ], cost: 1
     12: f39 -> f52 : K'=free_10, L'=free_10, M'=free_7, N'=free_9, O'=free_9, P'=free_8, [ 0>=free_8 && free_7>=1 && H>=1+Q && 0>=free_10 ], cost: 1
     24: f52 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     13: f52 -> f68 : Q_1'=3, R'=free_11, [ O>=0 && 0>=free_11 && Q_1==3 ], cost: 1
     14: f52 -> f68 : Q_1'=3, R'=free_12, [ O>=0 && free_12>=2 && Q_1==3 ], cost: 1
     15: f52 -> f59 : S'=free_13, [ O>=0 && 2>=Q_1 ], cost: 1
     16: f52 -> f59 : S'=free_14, [ O>=0 && Q_1>=4 ], cost: 1
     17: f52 -> f59 : Q_1'=3, R'=1, S'=free_15, [ O>=0 && Q_1==3 ], cost: 1
     18: f59 -> f63 : O'=free_16, T'=free_16, [ 10>=S ], cost: 1
     19: f59 -> f63 : O'=free_17, S'=10, T'=free_17, [ S>=11 ], cost: 1
     20: f63 -> f26 : C'=1+C, [ 0>=1+O ], cost: 1
     25: f63 -> f26 : C'=1+C, J'=L, U'=1+U, [ O>=0 ], cost: 1
     36: f71 -> [14] : [], cost: INF
     30: f0 -> f20 : A'=free_26, D'=free_24, E'=free_27, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 ], cost: 1
     31: f0 -> f20 : A'=free_30, D'=free_28, E'=free_31, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 ], cost: 1
     32: f0 -> f20 : A'=free_34, D'=free_32, E'=free_35, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 ], cost: 1
      3: [12] -> f68 : [ C>=E ], cost: 1
      4: [12] -> f33 : F'=free_1, G'=free, [ free_1>=1 && E>=1+C ], cost: 1
      5: [12] -> f33 : F'=free_3, G'=free_2, [ E>=1+C && 0>=free_3 && 0>=free_2 ], cost: 1
      6: [13] -> f39 : [ H>=1+Q ], cost: 1
      7: [13] -> f39 : J'=-1, [ Q>=H && 1+J==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     46: f26 -> f68 : C'=E, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 && E>=E ], cost: 1+E-C
     47: f26 -> [15] : C'=E, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 ], cost: E-C
     48: f26 -> [16] : C'=E, F'=free_19, G'=free_18, [ E>=1+C && 0>=free_19 && free_18>=1 ], cost: E-C
     49: f68 -> [14] : A'=0, [ 0>=U ], cost: INF
     50: f68 -> [14] : A'=1, [ U>=1 ], cost: INF
     37: f0 -> f26 : A'=free_26, B'=1, C'=free_24, D'=free_24, E'=free_27, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 ], cost: 2
     38: f0 -> f26 : A'=free_26, B'=1, C'=free_24, D'=free_24, E'=free_27, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 ], cost: 2
     40: f0 -> f26 : A'=free_30, B'=1, C'=free_28, D'=free_28, E'=free_31, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 ], cost: 2
     41: f0 -> f26 : A'=free_30, B'=1, C'=free_28, D'=free_28, E'=free_31, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 ], cost: 2
     43: f0 -> f26 : A'=free_34, B'=1, C'=free_32, D'=free_32, E'=free_35, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     49: f68 -> [14] : A'=0, [ 0>=U ], cost: INF
     50: f68 -> [14] : A'=1, [ U>=1 ], cost: INF
     51: f0 -> f68 : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     54: f0 -> f68 : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     57: f0 -> f68 : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     60: f0 -> f68 : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     63: f0 -> f68 : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 && free_35>=free_35 ], cost: 3+free_35-free_32
     52: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     55: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     58: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     61: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     64: f0 -> [15] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32
     53: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     56: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     59: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     62: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     65: f0 -> [16] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32


Applied chaining over branches and pruning:
  Start location: f0
     66: f0 -> [14] : A'=0, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 && 0>=0 ], cost: INF
     68: f0 -> [14] : A'=0, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 && 0>=0 ], cost: INF
     70: f0 -> [14] : A'=0, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 && 0>=0 ], cost: INF
     72: f0 -> [14] : A'=0, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 && 0>=0 ], cost: INF
     74: f0 -> [14] : A'=0, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 && free_35>=free_35 && 0>=0 ], cost: INF
     52: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     55: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     58: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     61: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     64: f0 -> [15] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32
     53: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     56: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     59: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     62: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     65: f0 -> [16] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32
     67: f0 -> [17] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     69: f0 -> [18] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     71: f0 -> [19] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     73: f0 -> [20] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     75: f0 -> [21] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 && free_35>=free_35 ], cost: 3+free_35-free_32


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     66: f0 -> [14] : A'=0, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 && 0>=0 ], cost: INF
     68: f0 -> [14] : A'=0, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 && 0>=0 ], cost: INF
     70: f0 -> [14] : A'=0, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 && 0>=0 ], cost: INF
     72: f0 -> [14] : A'=0, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 && 0>=0 ], cost: INF
     74: f0 -> [14] : A'=0, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 && free_35>=free_35 && 0>=0 ], cost: INF
     52: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     55: f0 -> [15] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     58: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     61: f0 -> [15] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     64: f0 -> [15] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32
     53: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     56: f0 -> [16] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 ], cost: 2+free_27-free_24
     59: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     62: f0 -> [16] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 ], cost: 2+free_31-free_28
     65: f0 -> [16] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 ], cost: 2+free_35-free_32
     67: f0 -> [17] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     69: f0 -> [18] : A'=free_26, B'=1, C'=free_27, D'=free_24, E'=free_27, F'=free_19, G'=free_18, Q'=0, U'=0, V'=3, W'=1, X'=free_25, Y'=free_26, [ free_24>=0 && free_25>=1 && V==3 && 0>=free_24 && 0>=free_26 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 ], cost: 3+free_27-free_24
     71: f0 -> [19] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && free_30>=1 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     73: f0 -> [20] : A'=free_30, B'=1, C'=free_31, D'=free_28, E'=free_31, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_29, Y'=free_30, [ 2>=V && free_28>=0 && free_29>=1 && 0>=free_28 && 0>=free_30 && free_31>=1+free_28 && 0>=free_19 && free_18>=1 && free_31>=free_31 ], cost: 3+free_31-free_28
     75: f0 -> [21] : A'=free_34, B'=1, C'=free_35, D'=free_32, E'=free_35, F'=free_19, G'=free_18, Q'=0, U'=0, W'=1, X'=free_33, Y'=free_34, [ V>=4 && free_32>=0 && free_33>=1 && free_34>=1 && free_35>=1+free_32 && 0>=free_19 && free_18>=1 && free_35>=free_35 ], cost: 3+free_35-free_32


Computing complexity for remaining 20 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_24>=0 && free_25>=1 && V==3 && free_26>=1 && free_27>=1+free_24 && 0>=free_19 && free_18>=1 && free_27>=free_27 && 0>=0
  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,?)