Trying to load file: main.koat

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


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

Eliminating 2 self-loops for location f11
  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 f6
  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: f26
      8: f11 -> [3] : [ A>=1+B ], cost: INF
      9: f11 -> [3] : [ B>=1+A ], cost: INF
     10: f6 -> [4] : F'=free, G'=1+G, H'=-1+H, Q'=1+G, J'=-1+H, K'=free_1, L'=free_2, M'=-1+H, [ E>=1+F && G>=0 && H>=1 ], cost: 1
     11: f6 -> [4] : F'=free_3, G'=1+G, H'=-1+H, Q'=1+G, J'=-1+H, K'=free_4, L'=free_5, M'=-1+H, [ F>=1+E && G>=0 && H>=1 ], cost: 1
     12: f6 -> [4] : [], cost: 0
      4: f26 -> f6 : F'=free_10, G'=1, H'=4, Q'=1, J'=4, N'=free_11, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_13, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, [], cost: 1
      5: f26 -> f6 : F'=free_21, G'=1, H'=4, Q'=1, J'=4, N'=free_22, O'=2, P'=3, Q_1'=free_26, R'=free_19, S'=4, T'=free_25, U'=0, V'=free_18, W'=free_24, X'=free_24, Y'=free_24, Z'=free_24, A1'=free_17, B1'=free_20, C1'=free_23, D1'=4, [], cost: 1
      6: [4] -> f11 : B'=free_30, C'=free_30, D'=free_30, E'=F, N'=free_29, Z'=free_31, E1'=free_28, [ A>=1+free_30 && G>=0 && H>=1 && F==E ], cost: 1
      7: [4] -> f11 : B'=free_34, C'=free_34, D'=free_34, E'=F, N'=free_33, Z'=free_35, E1'=free_32, [ free_34>=1+A && G>=0 && H>=1 && F==E ], cost: 1


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


Applied chaining over branches and pruning:
  Start location: f26
     21: f26 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free, F'=free, G'=2, H'=3, Q'=2, J'=3, K'=free_1, L'=free_2, M'=3, N'=free_29, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_31, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_28, [ E>=1+free_10 && 1>=0 && 4>=1 && A>=1+free_30 && 2>=0 && 3>=1 && free==E && A>=1+free_30 ], cost: INF
     22: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free, F'=free, G'=2, H'=3, Q'=2, J'=3, K'=free_1, L'=free_2, M'=3, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ E>=1+free_10 && 1>=0 && 4>=1 && free_34>=1+A && 2>=0 && 3>=1 && free==E && free_34>=1+A ], cost: INF
     24: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free_3, F'=free_3, G'=2, H'=3, Q'=2, J'=3, K'=free_4, L'=free_5, M'=3, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ free_10>=1+E && 1>=0 && 4>=1 && free_34>=1+A && 2>=0 && 3>=1 && free_3==E && free_34>=1+A ], cost: INF
     25: f26 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_10, F'=free_10, G'=1, H'=4, Q'=1, J'=4, N'=free_29, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_31, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_28, [ A>=1+free_30 && 1>=0 && 4>=1 && free_10==E && A>=1+free_30 ], cost: INF
     26: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free_10, F'=free_10, G'=1, H'=4, Q'=1, J'=4, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ free_34>=1+A && 1>=0 && 4>=1 && free_10==E && free_34>=1+A ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f26
     21: f26 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free, F'=free, G'=2, H'=3, Q'=2, J'=3, K'=free_1, L'=free_2, M'=3, N'=free_29, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_31, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_28, [ E>=1+free_10 && 1>=0 && 4>=1 && A>=1+free_30 && 2>=0 && 3>=1 && free==E && A>=1+free_30 ], cost: INF
     22: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free, F'=free, G'=2, H'=3, Q'=2, J'=3, K'=free_1, L'=free_2, M'=3, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ E>=1+free_10 && 1>=0 && 4>=1 && free_34>=1+A && 2>=0 && 3>=1 && free==E && free_34>=1+A ], cost: INF
     24: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free_3, F'=free_3, G'=2, H'=3, Q'=2, J'=3, K'=free_4, L'=free_5, M'=3, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ free_10>=1+E && 1>=0 && 4>=1 && free_34>=1+A && 2>=0 && 3>=1 && free_3==E && free_34>=1+A ], cost: INF
     25: f26 -> [3] : B'=free_30, C'=free_30, D'=free_30, E'=free_10, F'=free_10, G'=1, H'=4, Q'=1, J'=4, N'=free_29, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_31, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_28, [ A>=1+free_30 && 1>=0 && 4>=1 && free_10==E && A>=1+free_30 ], cost: INF
     26: f26 -> [3] : B'=free_34, C'=free_34, D'=free_34, E'=free_10, F'=free_10, G'=1, H'=4, Q'=1, J'=4, N'=free_33, O'=2, P'=3, Q_1'=free_15, R'=free_8, S'=4, T'=free_14, U'=0, V'=free_7, W'=free_13, X'=free_13, Y'=free_13, Z'=free_35, A1'=free_6, B1'=free_9, C1'=free_12, D1'=4, E1'=free_32, [ free_34>=1+A && 1>=0 && 4>=1 && free_10==E && free_34>=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_10 && 1>=0 && 4>=1 && A>=1+free_30 && 2>=0 && 3>=1 && free==E && A>=1+free_30
  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,?)