Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f17 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=0, [ A==0 ], cost: 1
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     27: f17 -> f36 : [ H>=256 ], cost: 1
      3: f17 -> f23 : Q'=free_1, J'=0, K'=free, L'=0, [ 255>=H ], cost: 1
     26: f23 -> f17 : H'=1+H, F1'=K, [ L>=8 ], cost: 1
      4: f23 -> f23 : K'=free_2, L'=1+L, [ 7>=L ], cost: 1
      8: f42 -> f42 : G'=free_6, H'=1+H, M'=free_5, [ 0>=1+F && D>=H ], cost: 1
      9: f42 -> f42 : G'=free_8, H'=1+H, M'=free_7, [ F>=0 && D>=H ], cost: 1
     24: f42 -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: f42 -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f66 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=0, [ A==0 ], cost: 1
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     23: f66 -> f85 : [ U>=256 ], cost: 1
     13: f66 -> f72 : V'=free_10, W'=0, X'=free_9, Y'=0, [ 255>=U ], cost: 1
     22: f72 -> f66 : U'=1+U, D1'=X, [ Y>=8 ], cost: 1
     14: f72 -> f72 : X'=free_11, Y'=1+Y, [ 7>=Y ], cost: 1
     18: f91 -> f91 : T'=free_15, U'=1+U, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1
     19: f91 -> f91 : T'=free_17, U'=1+U, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1
     20: f91 -> f106 : A1'=T, B1'=T, C1'=T, [ S>=0 && U>=1+Q_1 ], cost: 1
     21: f91 -> f106 : A1'=free_18, B1'=free_18, C1'=free_18, [ 0>=1+S && U>=1+Q_1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f17 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=0, [ A==0 ], cost: 1
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     27: f17 -> f36 : [ H>=256 ], cost: 1
      3: f17 -> f23 : Q'=free_1, J'=0, K'=free, L'=0, [ 255>=H ], cost: 1
     26: f23 -> f17 : H'=1+H, F1'=K, [ L>=8 ], cost: 1
      4: f23 -> f23 : K'=free_2, L'=1+L, [ 7>=L ], cost: 1
      8: f42 -> f42 : G'=free_6, H'=1+H, M'=free_5, [ 0>=1+F && D>=H ], cost: 1
      9: f42 -> f42 : G'=free_8, H'=1+H, M'=free_7, [ F>=0 && D>=H ], cost: 1
     24: f42 -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: f42 -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f66 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=0, [ A==0 ], cost: 1
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     23: f66 -> f85 : [ U>=256 ], cost: 1
     13: f66 -> f72 : V'=free_10, W'=0, X'=free_9, Y'=0, [ 255>=U ], cost: 1
     22: f72 -> f66 : U'=1+U, D1'=X, [ Y>=8 ], cost: 1
     14: f72 -> f72 : X'=free_11, Y'=1+Y, [ 7>=Y ], cost: 1
     18: f91 -> f91 : T'=free_15, U'=1+U, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1
     19: f91 -> f91 : T'=free_17, U'=1+U, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1

Eliminating 1 self-loops for location f23
  Self-Loop 4 has the metering function: 8-L, resulting in the new transition 28.
  Removing the self-loops: 4.
Eliminating 2 self-loops for location f42
  Self-Loop 8 has the metering function: 1-H+D, resulting in the new transition 29.
  Self-Loop 9 has the metering function: 1-H+D, resulting in the new transition 30.
  Removing the self-loops: 8 9.
Eliminating 1 self-loops for location f72
  Self-Loop 14 has the metering function: 8-Y, resulting in the new transition 31.
  Removing the self-loops: 14.
Eliminating 2 self-loops for location f91
  Self-Loop 18 has the metering function: 1+Q_1-U, resulting in the new transition 32.
  Self-Loop 19 has the metering function: 1+Q_1-U, resulting in the new transition 33.
  Removing the self-loops: 18 19.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f17 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=0, [ A==0 ], cost: 1
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     27: f17 -> f36 : [ H>=256 ], cost: 1
      3: f17 -> f23 : Q'=free_1, J'=0, K'=free, L'=0, [ 255>=H ], cost: 1
     28: f23 -> [11] : K'=free_2, L'=8, [ 7>=L ], cost: 8-L
     29: f42 -> [12] : G'=free_6, H'=1+D, M'=free_5, [ 0>=1+F && D>=H ], cost: 1-H+D
     30: f42 -> [12] : G'=free_8, H'=1+D, M'=free_7, [ F>=0 && D>=H ], cost: 1-H+D
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f66 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=0, [ A==0 ], cost: 1
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     23: f66 -> f85 : [ U>=256 ], cost: 1
     13: f66 -> f72 : V'=free_10, W'=0, X'=free_9, Y'=0, [ 255>=U ], cost: 1
     31: f72 -> [13] : X'=free_11, Y'=8, [ 7>=Y ], cost: 8-Y
     32: f91 -> [14] : T'=free_15, U'=1+Q_1, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1+Q_1-U
     33: f91 -> [14] : T'=free_17, U'=1+Q_1, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1+Q_1-U
     26: [11] -> f17 : H'=1+H, F1'=K, [ L>=8 ], cost: 1
     24: [12] -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: [12] -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1
     22: [13] -> f66 : U'=1+U, D1'=X, [ Y>=8 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f17 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=0, [ A==0 ], cost: 1
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     27: f17 -> f36 : [ H>=256 ], cost: 1
      3: f17 -> f17 : H'=1+H, Q'=free_1, J'=0, K'=free_2, L'=8, F1'=free_2, [ 255>=H && 7>=0 && 8>=8 ], cost: 10
     29: f42 -> [12] : G'=free_6, H'=1+D, M'=free_5, [ 0>=1+F && D>=H ], cost: 1-H+D
     30: f42 -> [12] : G'=free_8, H'=1+D, M'=free_7, [ F>=0 && D>=H ], cost: 1-H+D
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f66 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=0, [ A==0 ], cost: 1
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     23: f66 -> f85 : [ U>=256 ], cost: 1
     13: f66 -> f66 : U'=1+U, V'=free_10, W'=0, X'=free_11, Y'=8, D1'=free_11, [ 255>=U && 7>=0 && 8>=8 ], cost: 10
     32: f91 -> [14] : T'=free_15, U'=1+Q_1, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1+Q_1-U
     33: f91 -> [14] : T'=free_17, U'=1+Q_1, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1+Q_1-U
     24: [12] -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: [12] -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1

Eliminating 1 self-loops for location f17
  Self-Loop 3 has the metering function: 256-H, resulting in the new transition 34.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f66
  Self-Loop 13 has the metering function: 256-U, resulting in the new transition 35.
  Removing the self-loops: 13.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f17 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=0, [ A==0 ], cost: 1
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     34: f17 -> [15] : H'=256, Q'=free_1, J'=0, K'=free_2, L'=8, F1'=free_2, [ 255>=H ], cost: 2560-10*H
     29: f42 -> [12] : G'=free_6, H'=1+D, M'=free_5, [ 0>=1+F && D>=H ], cost: 1-H+D
     30: f42 -> [12] : G'=free_8, H'=1+D, M'=free_7, [ F>=0 && D>=H ], cost: 1-H+D
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f66 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=0, [ A==0 ], cost: 1
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     35: f66 -> [16] : U'=256, V'=free_10, W'=0, X'=free_11, Y'=8, D1'=free_11, [ 255>=U ], cost: 2560-10*U
     32: f91 -> [14] : T'=free_15, U'=1+Q_1, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1+Q_1-U
     33: f91 -> [14] : T'=free_17, U'=1+Q_1, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1+Q_1-U
     24: [12] -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: [12] -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1
     27: [15] -> f36 : [ H>=256 ], cost: 1
     23: [16] -> f85 : [ U>=256 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ 0>=1+A ], cost: 1
      1: f0 -> f36 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, [ A>=1 ], cost: 1
      2: f0 -> f36 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=0, H'=256, Q'=free_1, J'=0, K'=free_2, L'=8, F1'=free_2, [ A==0 && 255>=0 && 256>=256 ], cost: 2562
      5: f36 -> f42 : G'=free_3, H'=1, [ E>=0 ], cost: 1
      6: f36 -> f42 : H'=1, [ 0>=1+E && F>=0 ], cost: 1
      7: f36 -> f42 : G'=free_4, H'=1, [ 0>=1+E && 0>=1+F ], cost: 1
     29: f42 -> [12] : G'=free_6, H'=1+D, M'=free_5, [ 0>=1+F && D>=H ], cost: 1-H+D
     30: f42 -> [12] : G'=free_8, H'=1+D, M'=free_7, [ F>=0 && D>=H ], cost: 1-H+D
     10: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ 0>=1+A ], cost: 1
     11: f56 -> f85 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, [ A>=1 ], cost: 1
     12: f56 -> f85 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=O, U'=256, V'=free_10, W'=0, X'=free_11, Y'=8, D1'=free_11, [ A==0 && 255>=0 && 256>=256 ], cost: 2562
     15: f85 -> f91 : T'=free_12, U'=1, [ R>=0 ], cost: 1
     16: f85 -> f91 : U'=1, [ 0>=1+R && S>=0 ], cost: 1
     17: f85 -> f91 : T'=free_13, U'=1, [ 0>=1+R && 0>=1+S ], cost: 1
     32: f91 -> [14] : T'=free_15, U'=1+Q_1, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1+Q_1-U
     33: f91 -> [14] : T'=free_17, U'=1+Q_1, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1+Q_1-U
     24: [12] -> f56 : O'=G, E1'=G, [ F>=0 && H>=1+D ], cost: 1
     25: [12] -> f56 : O'=free_19, E1'=free_19, [ 0>=1+F && H>=1+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     36: f0 -> f42 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_3, H'=1, [ 0>=1+A && 0>=0 ], cost: 2
     37: f0 -> f42 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_3, H'=1, [ A>=1 && 0>=0 ], cost: 2
     38: f0 -> f42 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_3, H'=1, Q'=free_1, J'=0, K'=free_2, L'=8, F1'=free_2, [ A==0 && 255>=0 && 256>=256 && 0>=0 ], cost: 2563
     40: f42 -> f56 : G'=free_6, H'=1+D, M'=free_5, O'=free_19, E1'=free_19, [ 0>=1+F && D>=H && 0>=1+F && 1+D>=1+D ], cost: 2-H+D
     41: f42 -> f56 : G'=free_8, H'=1+D, M'=free_7, O'=free_8, E1'=free_8, [ F>=0 && D>=H && F>=0 && 1+D>=1+D ], cost: 2-H+D
     39: f42 -> [17] : G'=free_6, H'=1+D, M'=free_5, [ 0>=1+F && D>=H ], cost: 1-H+D
     42: f42 -> [18] : G'=free_8, H'=1+D, M'=free_7, [ F>=0 && D>=H ], cost: 1-H+D
     43: f56 -> f91 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_12, U'=1, [ 0>=1+A && 0>=0 ], cost: 2
     44: f56 -> f91 : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_12, U'=1, [ A>=1 && 0>=0 ], cost: 2
     45: f56 -> f91 : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_12, U'=1, V'=free_10, W'=0, X'=free_11, Y'=8, D1'=free_11, [ A==0 && 255>=0 && 256>=256 && 0>=0 ], cost: 2563
     32: f91 -> [14] : T'=free_15, U'=1+Q_1, Z'=free_14, [ 0>=1+S && Q_1>=U ], cost: 1+Q_1-U
     33: f91 -> [14] : T'=free_17, U'=1+Q_1, Z'=free_16, [ S>=0 && Q_1>=U ], cost: 1+Q_1-U


Applied chaining over branches and pruning:
  Start location: f0
     46: f0 -> f56 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_8, H'=41, M'=free_7, O'=free_8, E1'=free_8, [ 0>=1+A && 0>=0 && 1>=0 && 40>=1 && 1>=0 && 41>=41 ], cost: 43
     48: f0 -> f56 : B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_8, H'=41, M'=free_7, O'=free_8, E1'=free_8, [ A>=1 && 0>=0 && 1>=0 && 40>=1 && 1>=0 && 41>=41 ], cost: 43
     50: f0 -> f56 : A'=1, B'=40, C'=0, D'=40, E'=0, F'=1, G'=free_8, H'=41, Q'=free_1, J'=0, K'=free_2, L'=8, M'=free_7, O'=free_8, E1'=free_8, F1'=free_2, [ A==0 && 255>=0 && 256>=256 && 0>=0 && 1>=0 && 40>=1 && 1>=0 && 41>=41 ], cost: 2604
     52: f56 -> [14] : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_17, U'=3+B, Z'=free_16, [ 0>=1+A && 0>=0 && 1>=0 && 2+B>=1 ], cost: 4+B
     53: f56 -> [14] : N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_17, U'=3+B, Z'=free_16, [ A>=1 && 0>=0 && 1>=0 && 2+B>=1 ], cost: 4+B
     54: f56 -> [14] : A'=1, N'=O, P'=O, Q_1'=2+B, R'=0, S'=1, T'=free_17, U'=3+B, V'=free_10, W'=0, X'=free_11, Y'=8, Z'=free_16, D1'=free_11, [ A==0 && 255>=0 && 256>=256 && 0>=0 && 1>=0 && 2+B>=1 ], cost: 2565+B


Applied chaining over branches and pruning:
  Start location: f0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    <empty>


Computing complexity for remaining 0 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: const
  Complexity value: 0

WORST_CASE(Omega(1),?)