Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f26
      0: f12 -> f11 : C'=A, D'=A, [ A>=1+B ], cost: 1
      1: f12 -> f11 : C'=A, D'=A, [ B>=1+A ], cost: 1
      2: f11 -> f11 : C'=A, D'=A, [ A>=1+B ], cost: 1
      3: f11 -> f11 : C'=A, D'=A, [ B>=1+A ], cost: 1
      8: f6 -> f12 : A'=free_30, C'=free_30, D'=free_30, F'=E, N'=free_29, Z'=free_31, E1'=free_28, [ free_30>=1+B && G>=0 && H>=1 && E==F ], cost: 1
      9: f6 -> f12 : A'=free_34, C'=free_34, D'=free_34, F'=E, N'=free_33, Z'=free_35, E1'=free_32, [ B>=1+free_34 && G>=0 && H>=1 && E==F ], cost: 1
      4: f6 -> f6 : E'=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
      5: f6 -> f6 : E'=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
      6: f26 -> f6 : E'=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, [ free_16>=1+F ], cost: 1
      7: f26 -> f6 : E'=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, [ F>=1+free_27 ], cost: 1


Simplified the transitions:
  Start location: f26
      0: f12 -> f11 : C'=A, D'=A, [ A>=1+B ], cost: 1
      1: f12 -> f11 : C'=A, D'=A, [ B>=1+A ], cost: 1
      2: f11 -> f11 : C'=A, D'=A, [ A>=1+B ], cost: 1
      3: f11 -> f11 : C'=A, D'=A, [ B>=1+A ], cost: 1
      8: f6 -> f12 : A'=free_30, C'=free_30, D'=free_30, F'=E, N'=free_29, Z'=free_31, E1'=free_28, [ free_30>=1+B && G>=0 && H>=1 && E==F ], cost: 1
      9: f6 -> f12 : A'=free_34, C'=free_34, D'=free_34, F'=E, N'=free_33, Z'=free_35, E1'=free_32, [ B>=1+free_34 && G>=0 && H>=1 && E==F ], cost: 1
      4: f6 -> f6 : E'=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
      5: f6 -> f6 : E'=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
      6: f26 -> f6 : E'=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
      7: f26 -> f6 : E'=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 2 has unbounded runtime, resulting in the new transition 10.
  Self-Loop 3 has unbounded runtime, resulting in the new transition 11.
  Removing the self-loops: 2 3.
Eliminating 2 self-loops for location f6
  Removing the self-loops: 4 5.
Adding an epsilon transition (to model nonexecution of the loops): 14.

Removed all Self-loops using metering functions (where possible):
  Start location: f26
      0: f12 -> f11 : C'=A, D'=A, [ A>=1+B ], cost: 1
      1: f12 -> f11 : C'=A, D'=A, [ B>=1+A ], cost: 1
     10: f11 -> [4] : [ A>=1+B ], cost: INF
     11: f11 -> [4] : [ B>=1+A ], cost: INF
     12: f6 -> [5] : E'=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
     13: f6 -> [5] : E'=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
     14: f6 -> [5] : [], cost: 0
      6: f26 -> f6 : E'=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
      7: f26 -> f6 : E'=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
      8: [5] -> f12 : A'=free_30, C'=free_30, D'=free_30, F'=E, N'=free_29, Z'=free_31, E1'=free_28, [ free_30>=1+B && G>=0 && H>=1 && E==F ], cost: 1
      9: [5] -> f12 : A'=free_34, C'=free_34, D'=free_34, F'=E, N'=free_33, Z'=free_35, E1'=free_32, [ B>=1+free_34 && G>=0 && H>=1 && E==F ], cost: 1


Applied chaining over branches and pruning:
  Start location: f26
     10: f11 -> [4] : [ A>=1+B ], cost: INF
     11: f11 -> [4] : [ B>=1+A ], cost: INF
     15: f26 -> [5] : E'=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, [ free_10>=1+F && 1>=0 && 4>=1 ], cost: 2
     16: f26 -> [5] : E'=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, [ F>=1+free_10 && 1>=0 && 4>=1 ], cost: 2
     17: f26 -> [5] : E'=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
     18: f26 -> [5] : E'=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, [ free_21>=1+F && 1>=0 && 4>=1 ], cost: 2
     20: f26 -> [5] : E'=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
     21: [5] -> f11 : A'=free_30, C'=free_30, D'=free_30, F'=E, N'=free_29, Z'=free_31, E1'=free_28, [ free_30>=1+B && G>=0 && H>=1 && E==F && free_30>=1+B ], cost: 2
     22: [5] -> f11 : A'=free_34, C'=free_34, D'=free_34, F'=E, N'=free_33, Z'=free_35, E1'=free_32, [ B>=1+free_34 && G>=0 && H>=1 && E==F && B>=1+free_34 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f26
     10: f11 -> [4] : [ A>=1+B ], cost: INF
     11: f11 -> [4] : [ B>=1+A ], cost: INF
     23: f26 -> f11 : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && free_30>=1+B && 2>=0 && 3>=1 && free==F && free_30>=1+B ], cost: 4
     24: f26 -> f11 : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free==F && B>=1+free_34 ], cost: 4
     26: f26 -> f11 : A'=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, [ F>=1+free_10 && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free_3==F && B>=1+free_34 ], cost: 4
     27: f26 -> f11 : A'=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, [ free_30>=1+B && 1>=0 && 4>=1 && free_10==F && free_30>=1+B ], cost: 3
     28: f26 -> f11 : A'=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, [ B>=1+free_34 && 1>=0 && 4>=1 && free_10==F && B>=1+free_34 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f26
     33: f26 -> [4] : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && free_30>=1+B && 2>=0 && 3>=1 && free==F && free_30>=1+B && free_30>=1+B ], cost: INF
     34: f26 -> [4] : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free==F && B>=1+free_34 && B>=1+free_34 ], cost: INF
     35: f26 -> [4] : A'=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, [ F>=1+free_10 && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free_3==F && B>=1+free_34 && B>=1+free_34 ], cost: INF
     36: f26 -> [4] : A'=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, [ free_30>=1+B && 1>=0 && 4>=1 && free_10==F && free_30>=1+B && free_30>=1+B ], cost: INF
     37: f26 -> [4] : A'=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, [ B>=1+free_34 && 1>=0 && 4>=1 && free_10==F && B>=1+free_34 && B>=1+free_34 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f26
     33: f26 -> [4] : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && free_30>=1+B && 2>=0 && 3>=1 && free==F && free_30>=1+B && free_30>=1+B ], cost: INF
     34: f26 -> [4] : A'=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, [ free_10>=1+F && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free==F && B>=1+free_34 && B>=1+free_34 ], cost: INF
     35: f26 -> [4] : A'=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, [ F>=1+free_10 && 1>=0 && 4>=1 && B>=1+free_34 && 2>=0 && 3>=1 && free_3==F && B>=1+free_34 && B>=1+free_34 ], cost: INF
     36: f26 -> [4] : A'=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, [ free_30>=1+B && 1>=0 && 4>=1 && free_10==F && free_30>=1+B && free_30>=1+B ], cost: INF
     37: f26 -> [4] : A'=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, [ B>=1+free_34 && 1>=0 && 4>=1 && free_10==F && B>=1+free_34 && B>=1+free_34 ], 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: free_10>=1+F && 1>=0 && 4>=1 && free_30>=1+B && 2>=0 && 3>=1 && free==F && free_30>=1+B && free_30>=1+B
  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,?)