Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f23
      0: f8 -> f8 : C'=B, D'=B, [ A>=1+B ], cost: 1
      1: f8 -> f8 : C'=B, D'=B, [ B>=1+A ], cost: 1
      6: f2 -> f8 : B'=free_26, C'=free_26, D'=free_26, E'=F, Q_1'=free_24, U'=free_27, A1'=free_25, [ A>=1+free_26 && G>=1 && H>=0 && F==E ], cost: 1
      7: f2 -> f8 : B'=free_30, C'=free_30, D'=free_30, E'=F, Q_1'=free_28, U'=free_31, A1'=free_29, [ free_30>=1+A && G>=1 && H>=0 && F==E ], cost: 1
      2: f2 -> f2 : F'=free, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_1, L'=free_2, M'=-1+G, [ E>=1+F && G>=1 && H>=0 ], cost: 1
      3: f2 -> f2 : F'=free_3, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_4, L'=free_5, M'=-1+G, [ F>=1+E && G>=1 && H>=0 ], cost: 1
      4: f23 -> f2 : F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [ E>=1+free_14 ], cost: 1
      5: f23 -> f2 : F'=free_16, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_19, P'=free_22, Q_1'=free_18, R'=free_21, S'=free_21, T'=free_21, U'=free_21, V'=free_15, W'=free_17, X'=2, Y'=free_20, Z'=0, [ free_23>=1+E ], cost: 1


Simplified the transitions:
  Start location: f23
      0: f8 -> f8 : C'=B, D'=B, [ A>=1+B ], cost: 1
      1: f8 -> f8 : C'=B, D'=B, [ B>=1+A ], cost: 1
      6: f2 -> f8 : B'=free_26, C'=free_26, D'=free_26, E'=F, Q_1'=free_24, U'=free_27, A1'=free_25, [ A>=1+free_26 && G>=1 && H>=0 && F==E ], cost: 1
      7: f2 -> f8 : B'=free_30, C'=free_30, D'=free_30, E'=F, Q_1'=free_28, U'=free_31, A1'=free_29, [ free_30>=1+A && G>=1 && H>=0 && F==E ], cost: 1
      2: f2 -> f2 : F'=free, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_1, L'=free_2, M'=-1+G, [ E>=1+F && G>=1 && H>=0 ], cost: 1
      3: f2 -> f2 : F'=free_3, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_4, L'=free_5, M'=-1+G, [ F>=1+E && G>=1 && H>=0 ], cost: 1
      4: f23 -> f2 : F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [], cost: 1
      5: f23 -> f2 : F'=free_16, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_19, P'=free_22, Q_1'=free_18, R'=free_21, S'=free_21, T'=free_21, U'=free_21, V'=free_15, W'=free_17, X'=2, Y'=free_20, Z'=0, [], cost: 1

Eliminating 2 self-loops for location f8
  Self-Loop 0 has unbounded runtime, resulting in the new transition 8.
  Self-Loop 1 has unbounded runtime, resulting in the new transition 9.
  Removing the self-loops: 0 1.
Eliminating 2 self-loops for location f2
  Removing the self-loops: 2 3.
Adding an epsilon transition (to model nonexecution of the loops): 12.

Removed all Self-loops using metering functions (where possible):
  Start location: f23
      8: f8 -> [3] : [ A>=1+B ], cost: INF
      9: f8 -> [3] : [ B>=1+A ], cost: INF
     10: f2 -> [4] : F'=free, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_1, L'=free_2, M'=-1+G, [ E>=1+F && G>=1 && H>=0 ], cost: 1
     11: f2 -> [4] : F'=free_3, G'=-1+G, H'=1+H, Q'=1+H, J'=-1+G, K'=free_4, L'=free_5, M'=-1+G, [ F>=1+E && G>=1 && H>=0 ], cost: 1
     12: f2 -> [4] : [], cost: 0
      4: f23 -> f2 : F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [], cost: 1
      5: f23 -> f2 : F'=free_16, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_19, P'=free_22, Q_1'=free_18, R'=free_21, S'=free_21, T'=free_21, U'=free_21, V'=free_15, W'=free_17, X'=2, Y'=free_20, Z'=0, [], cost: 1
      6: [4] -> f8 : B'=free_26, C'=free_26, D'=free_26, E'=F, Q_1'=free_24, U'=free_27, A1'=free_25, [ A>=1+free_26 && G>=1 && H>=0 && F==E ], cost: 1
      7: [4] -> f8 : B'=free_30, C'=free_30, D'=free_30, E'=F, Q_1'=free_28, U'=free_31, A1'=free_29, [ free_30>=1+A && G>=1 && H>=0 && F==E ], cost: 1


Applied chaining over branches and pruning:
  Start location: f23
     13: f23 -> [4] : F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [ E>=1+free_7 && 2>=1 && 1>=0 ], cost: 2
     14: f23 -> [4] : F'=free_3, G'=1, H'=2, Q'=2, J'=1, K'=free_4, L'=free_5, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [ free_7>=1+E && 2>=1 && 1>=0 ], cost: 2
     15: f23 -> [4] : F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_9, R'=free_12, S'=free_12, T'=free_12, U'=free_12, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, [], cost: 1
     16: f23 -> [4] : F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_19, P'=free_22, Q_1'=free_18, R'=free_21, S'=free_21, T'=free_21, U'=free_21, V'=free_15, W'=free_17, X'=2, Y'=free_20, Z'=0, [ E>=1+free_16 && 2>=1 && 1>=0 ], cost: 2
     18: f23 -> [4] : F'=free_16, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_19, P'=free_22, Q_1'=free_18, R'=free_21, S'=free_21, T'=free_21, U'=free_21, V'=free_15, W'=free_17, X'=2, Y'=free_20, Z'=0, [], cost: 1
     19: [4] -> [3] : B'=free_26, C'=free_26, D'=free_26, E'=F, Q_1'=free_24, U'=free_27, A1'=free_25, [ A>=1+free_26 && G>=1 && H>=0 && F==E && A>=1+free_26 ], cost: INF
     20: [4] -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=F, Q_1'=free_28, U'=free_31, A1'=free_29, [ free_30>=1+A && G>=1 && H>=0 && F==E && free_30>=1+A ], cost: INF


Applied chaining over branches and pruning:
  Start location: f23
     21: f23 -> [3] : B'=free_26, C'=free_26, D'=free_26, E'=free, F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_24, R'=free_12, S'=free_12, T'=free_12, U'=free_27, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_25, [ E>=1+free_7 && 2>=1 && 1>=0 && A>=1+free_26 && 1>=1 && 2>=0 && free==E && A>=1+free_26 ], cost: INF
     22: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free, F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ E>=1+free_7 && 2>=1 && 1>=0 && free_30>=1+A && 1>=1 && 2>=0 && free==E && free_30>=1+A ], cost: INF
     24: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_3, F'=free_3, G'=1, H'=2, Q'=2, J'=1, K'=free_4, L'=free_5, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ free_7>=1+E && 2>=1 && 1>=0 && free_30>=1+A && 1>=1 && 2>=0 && free_3==E && free_30>=1+A ], cost: INF
     25: f23 -> [3] : B'=free_26, C'=free_26, D'=free_26, E'=free_7, F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_24, R'=free_12, S'=free_12, T'=free_12, U'=free_27, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_25, [ A>=1+free_26 && 2>=1 && 1>=0 && free_7==E && A>=1+free_26 ], cost: INF
     26: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_7, F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ free_30>=1+A && 2>=1 && 1>=0 && free_7==E && free_30>=1+A ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f23
     21: f23 -> [3] : B'=free_26, C'=free_26, D'=free_26, E'=free, F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_24, R'=free_12, S'=free_12, T'=free_12, U'=free_27, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_25, [ E>=1+free_7 && 2>=1 && 1>=0 && A>=1+free_26 && 1>=1 && 2>=0 && free==E && A>=1+free_26 ], cost: INF
     22: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free, F'=free, G'=1, H'=2, Q'=2, J'=1, K'=free_1, L'=free_2, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ E>=1+free_7 && 2>=1 && 1>=0 && free_30>=1+A && 1>=1 && 2>=0 && free==E && free_30>=1+A ], cost: INF
     24: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_3, F'=free_3, G'=1, H'=2, Q'=2, J'=1, K'=free_4, L'=free_5, M'=1, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ free_7>=1+E && 2>=1 && 1>=0 && free_30>=1+A && 1>=1 && 2>=0 && free_3==E && free_30>=1+A ], cost: INF
     25: f23 -> [3] : B'=free_26, C'=free_26, D'=free_26, E'=free_7, F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_24, R'=free_12, S'=free_12, T'=free_12, U'=free_27, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_25, [ A>=1+free_26 && 2>=1 && 1>=0 && free_7==E && A>=1+free_26 ], cost: INF
     26: f23 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_7, F'=free_7, G'=2, H'=1, Q'=1, J'=2, N'=2, O'=free_10, P'=free_13, Q_1'=free_28, R'=free_12, S'=free_12, T'=free_12, U'=free_31, V'=free_6, W'=free_8, X'=2, Y'=free_11, Z'=0, A1'=free_29, [ free_30>=1+A && 2>=1 && 1>=0 && free_7==E && free_30>=1+A ], cost: INF


Computing complexity for remaining 5 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: E>=1+free_7 && 2>=1 && 1>=0 && A>=1+free_26 && 1>=1 && 2>=0 && free==E && A>=1+free_26
  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,?)