Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f25 -> f15 : C'=1+C, [ A>=1+B ], cost: 1
      1: f25 -> f15 : C'=1+C, D'=free, E'=0, F'=1, [ B>=A ], cost: 1
     14: f15 -> f25 : S'=free_12, T'=free_13, U'=free_11, V'=free_11, W'=free_11, [ 0>=1+free_11 && R>=1+C ], cost: 1
     15: f15 -> f25 : S'=free_15, T'=free_16, U'=free_14, V'=free_14, W'=free_14, [ free_14>=1 && R>=1+C ], cost: 1
     16: f15 -> f15 : C'=1+C, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: 1
     17: f15 -> f31 : [ C>=R ], cost: 1
      2: f31 -> f31 : [], cost: 1
      3: f33 -> f36 : C'=1, G'=0, [], cost: 1
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> f61 : Q_1'=0, [ C>=1+H ], cost: 1
      8: f45 -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
      5: f45 -> f46 : N'=M, [ 0>=1+M ], cost: 1
      6: f45 -> f46 : N'=M, [ M>=1 ], cost: 1
      7: f46 -> f36 : C'=1+C, [ A>=1+B ], cost: 1
     11: f46 -> f36 : C'=1+C, D'=free_5, E'=0, O'=free_6, [ B>=A ], cost: 1
     12: f46 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, P'=free_8, [ B>=A ], cost: 1
      9: f61 -> f61 : [], cost: 1
     10: f63 -> f65 : [], cost: 1
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f25 -> f15 : C'=1+C, [ A>=1+B ], cost: 1
      1: f25 -> f15 : C'=1+C, D'=free, E'=0, F'=1, [ B>=A ], cost: 1
     14: f15 -> f25 : S'=free_12, T'=free_13, U'=free_11, V'=free_11, W'=free_11, [ 0>=1+free_11 && R>=1+C ], cost: 1
     15: f15 -> f25 : S'=free_15, T'=free_16, U'=free_14, V'=free_14, W'=free_14, [ free_14>=1 && R>=1+C ], cost: 1
     16: f15 -> f15 : C'=1+C, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: 1
     17: f15 -> f31 : [ C>=R ], cost: 1
      2: f31 -> f31 : [], cost: 1
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> f61 : Q_1'=0, [ C>=1+H ], cost: 1
      8: f45 -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
      5: f45 -> f46 : N'=M, [ 0>=1+M ], cost: 1
      6: f45 -> f46 : N'=M, [ M>=1 ], cost: 1
      7: f46 -> f36 : C'=1+C, [ A>=1+B ], cost: 1
     11: f46 -> f36 : C'=1+C, D'=free_5, E'=0, O'=free_6, [ B>=A ], cost: 1
     12: f46 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, P'=free_8, [ B>=A ], cost: 1
      9: f61 -> f61 : [], cost: 1
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1

Eliminating 1 self-loops for location f15
  Self-Loop 16 has the metering function: R-C, resulting in the new transition 21.
  Removing the self-loops: 16.
Eliminating 1 self-loops for location f31
  Self-Loop 2 has unbounded runtime, resulting in the new transition 22.
  Removing the self-loops: 2.
Eliminating 1 self-loops for location f61
  Self-Loop 9 has unbounded runtime, resulting in the new transition 23.
  Removing the self-loops: 9.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f25 -> f15 : C'=1+C, [ A>=1+B ], cost: 1
      1: f25 -> f15 : C'=1+C, D'=free, E'=0, F'=1, [ B>=A ], cost: 1
     21: f15 -> [11] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
     22: f31 -> [12] : [], cost: INF
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> f61 : Q_1'=0, [ C>=1+H ], cost: 1
      8: f45 -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
      5: f45 -> f46 : N'=M, [ 0>=1+M ], cost: 1
      6: f45 -> f46 : N'=M, [ M>=1 ], cost: 1
      7: f46 -> f36 : C'=1+C, [ A>=1+B ], cost: 1
     11: f46 -> f36 : C'=1+C, D'=free_5, E'=0, O'=free_6, [ B>=A ], cost: 1
     12: f46 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, P'=free_8, [ B>=A ], cost: 1
     23: f61 -> [13] : [], cost: INF
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
     14: [11] -> f25 : S'=free_12, T'=free_13, U'=free_11, V'=free_11, W'=free_11, [ 0>=1+free_11 && R>=1+C ], cost: 1
     15: [11] -> f25 : S'=free_15, T'=free_16, U'=free_14, V'=free_14, W'=free_14, [ free_14>=1 && R>=1+C ], cost: 1
     17: [11] -> f31 : [ C>=R ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f25 -> f15 : C'=1+C, [ A>=1+B ], cost: 1
      1: f25 -> f15 : C'=1+C, D'=free, E'=0, F'=1, [ B>=A ], cost: 1
     21: f15 -> [11] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> [13] : Q_1'=0, [ C>=1+H ], cost: INF
      8: f45 -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
      5: f45 -> f46 : N'=M, [ 0>=1+M ], cost: 1
      6: f45 -> f46 : N'=M, [ M>=1 ], cost: 1
      7: f46 -> f36 : C'=1+C, [ A>=1+B ], cost: 1
     11: f46 -> f36 : C'=1+C, D'=free_5, E'=0, O'=free_6, [ B>=A ], cost: 1
     12: f46 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, P'=free_8, [ B>=A ], cost: 1
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
     14: [11] -> f25 : S'=free_12, T'=free_13, U'=free_11, V'=free_11, W'=free_11, [ 0>=1+free_11 && R>=1+C ], cost: 1
     15: [11] -> f25 : S'=free_15, T'=free_16, U'=free_14, V'=free_14, W'=free_14, [ free_14>=1 && R>=1+C ], cost: 1
     17: [11] -> [12] : [ C>=R ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     26: f15 -> [12] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C && R>=R ], cost: INF
     24: f15 -> [14] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
     25: f15 -> [15] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> [13] : Q_1'=0, [ C>=1+H ], cost: INF
      8: f45 -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
     27: f45 -> f36 : C'=1+C, N'=M, [ 0>=1+M && A>=1+B ], cost: 2
     28: f45 -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ 0>=1+M && B>=A ], cost: 2
     30: f45 -> f36 : C'=1+C, N'=M, [ M>=1 && A>=1+B ], cost: 2
     31: f45 -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ M>=1 && B>=A ], cost: 2
     29: f45 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=M, P'=free_8, [ 0>=1+M && B>=A ], cost: 2
     32: f45 -> f45 : J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=M, P'=free_8, [ M>=1 && B>=A ], cost: 2
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1

Eliminating 2 self-loops for location f45
  Removing the self-loops: 29 32.
Adding an epsilon transition (to model nonexecution of the loops): 35.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     26: f15 -> [12] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C && R>=R ], cost: INF
     24: f15 -> [14] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
     25: f15 -> [15] : C'=R, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, [ R>=1+C ], cost: R-C
      4: f36 -> f45 : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     13: f36 -> [13] : Q_1'=0, [ C>=1+H ], cost: INF
     33: f45 -> [16] : J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=M, P'=free_8, [ 0>=1+M && B>=A ], cost: 2
     34: f45 -> [16] : J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=M, P'=free_8, [ M>=1 && B>=A ], cost: 2
     35: f45 -> [16] : [], cost: 0
     18: f0 -> f15 : C'=0, G'=0, H'=free_20, Q_1'=0, R'=free_19, X'=1, [], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
      8: [16] -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
     27: [16] -> f36 : C'=1+C, N'=M, [ 0>=1+M && A>=1+B ], cost: 2
     28: [16] -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ 0>=1+M && B>=A ], cost: 2
     30: [16] -> f36 : C'=1+C, N'=M, [ M>=1 && A>=1+B ], cost: 2
     31: [16] -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ M>=1 && B>=A ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     13: f36 -> [13] : Q_1'=0, [ C>=1+H ], cost: INF
     39: f36 -> [16] : Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_2, P'=free_8, [ H>=C && 0>=1+free_2 && B>=A ], cost: 3
     40: f36 -> [16] : Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_2, P'=free_8, [ H>=C && free_2>=1 && B>=A ], cost: 3
     41: f36 -> [16] : Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=free_2, [ H>=C ], cost: 1
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
      8: [16] -> f36 : C'=1+C, M'=0, N'=0, [ M==0 ], cost: 1
     27: [16] -> f36 : C'=1+C, N'=M, [ 0>=1+M && A>=1+B ], cost: 2
     28: [16] -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ 0>=1+M && B>=A ], cost: 2
     30: [16] -> f36 : C'=1+C, N'=M, [ M>=1 && A>=1+B ], cost: 2
     31: [16] -> f36 : C'=1+C, D'=free_5, E'=0, N'=M, O'=free_6, [ M>=1 && B>=A ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     42: f36 -> f36 : C'=1+C, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=0, N'=0, P'=free_8, [ H>=C && 0>=1+free_2 && B>=A && free_7==0 ], cost: 4
     43: f36 -> f36 : C'=1+C, D'=free_5, E'=0, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, [ H>=C && 0>=1+free_2 && B>=A && 0>=1+free_7 && B>=A ], cost: 5
     45: f36 -> f36 : C'=1+C, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=0, N'=0, P'=free_8, [ H>=C && free_2>=1 && B>=A && free_7==0 ], cost: 4
     47: f36 -> f36 : C'=1+C, D'=free_5, E'=0, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, [ H>=C && free_2>=1 && B>=A && free_7>=1 && B>=A ], cost: 5
     48: f36 -> f36 : C'=1+C, Q'=free_3, J'=free_4, K'=free_1, L'=free_2, M'=0, N'=0, [ H>=C && free_2==0 ], cost: 2
     13: f36 -> [13] : Q_1'=0, [ C>=1+H ], cost: INF
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19

Eliminating 5 self-loops for location f36
  Self-Loop 42 has the metering function: 1+H-C, resulting in the new transition 53.
  Self-Loop 43 has the metering function: 1+H-C, resulting in the new transition 54.
  Self-Loop 45 has the metering function: 1+H-C, resulting in the new transition 55.
  Self-Loop 47 has the metering function: 1+H-C, resulting in the new transition 56.
  Self-Loop 48 has the metering function: 1+H-C, resulting in the new transition 57.
  Removing the self-loops: 42 43 45 47 48.
Removing duplicate transition: 53.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     54: f36 -> [17] : C'=1+H, D'=free_5, E'=0, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, [ H>=C && B>=A && 0>=1+free_7 ], cost: 5+5*H-5*C
     55: f36 -> [17] : C'=1+H, Q'=free_3, J'=free_9, K'=free_10, L'=0, M'=0, N'=0, P'=free_8, [ H>=C && B>=A ], cost: 4+4*H-4*C
     56: f36 -> [17] : C'=1+H, D'=free_5, E'=0, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, [ H>=C && B>=A && free_7>=1 ], cost: 5+5*H-5*C
     57: f36 -> [17] : C'=1+H, Q'=free_3, J'=free_4, K'=free_1, L'=0, M'=0, N'=0, [ H>=C ], cost: 2+2*H-2*C
     19: f0 -> f36 : C'=1, G'=0, H'=free_21, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 ], cost: 1
     20: f0 -> f36 : C'=1, G'=0, H'=free_24, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 ], cost: 1
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     13: [17] -> [13] : Q_1'=0, [ C>=1+H ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     58: f0 -> [17] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && 0>=1+free_7 ], cost: 1+5*free_21
     59: f0 -> [17] : C'=1+free_21, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=0, M'=0, N'=0, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A ], cost: 1+4*free_21
     60: f0 -> [17] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && free_7>=1 ], cost: 1+5*free_21
     62: f0 -> [17] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && 0>=1+free_7 ], cost: 1+5*free_24
     64: f0 -> [17] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && free_7>=1 ], cost: 1+5*free_24
     13: [17] -> [13] : Q_1'=0, [ C>=1+H ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     66: f0 -> [13] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && 0>=1+free_7 && 1+free_21>=1+free_21 ], cost: INF
     67: f0 -> [13] : C'=1+free_21, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=0, M'=0, N'=0, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && 1+free_21>=1+free_21 ], cost: INF
     68: f0 -> [13] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && free_7>=1 && 1+free_21>=1+free_21 ], cost: INF
     69: f0 -> [13] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && 0>=1+free_7 && 1+free_24>=1+free_24 ], cost: INF
     70: f0 -> [13] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && free_7>=1 && 1+free_24>=1+free_24 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     36: f0 -> [12] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 && free_19>=free_19 ], cost: INF
     66: f0 -> [13] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && 0>=1+free_7 && 1+free_21>=1+free_21 ], cost: INF
     67: f0 -> [13] : C'=1+free_21, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=0, M'=0, N'=0, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && 1+free_21>=1+free_21 ], cost: INF
     68: f0 -> [13] : C'=1+free_21, D'=free_5, E'=0, G'=0, H'=free_21, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_23, X'=free_22, [ 0>=free_22 && free_21>=1 && B>=A && free_7>=1 && 1+free_21>=1+free_21 ], cost: INF
     69: f0 -> [13] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && 0>=1+free_7 && 1+free_24>=1+free_24 ], cost: INF
     70: f0 -> [13] : C'=1+free_24, D'=free_5, E'=0, G'=0, H'=free_24, Q'=free_3, J'=free_9, K'=free_10, L'=free_7, M'=free_7, N'=free_7, O'=free_6, P'=free_8, Q_1'=0, R'=free_26, X'=free_25, [ free_25>=2 && free_24>=1 && B>=A && free_7>=1 && 1+free_24>=1+free_24 ], cost: INF
     37: f0 -> [14] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19
     38: f0 -> [15] : C'=free_19, G'=0, H'=free_20, Q_1'=0, R'=free_19, S'=free_17, T'=free_18, U'=0, V'=0, W'=0, X'=1, [ free_19>=1 ], cost: 1+free_19


Computing complexity for remaining 8 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_19>=1 && free_19>=free_19
  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,?)