Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      1: f1 -> f7 : A'=1, B'=C, D'=E, F'=free_1, G'=free, H'=0, Q'=1, J'=free_1, K'=free, L'=7, [ 7>=free && 7>=free_1 && 3>=free && free>=1 && free_1>=1 ], cost: 1
      2: f1 -> f7 : A'=1, B'=C, D'=E, F'=free_3, G'=free_2, H'=0, Q'=1, J'=free_3, K'=free_2, L'=7, [ 7>=free_2 && 7>=free_3 && free_2>=5 && free_3>=1 ], cost: 1
      3: f1 -> f7 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_4, G'=4, H'=1, Q'=1, J'=free_4, K'=4, L'=7, [ 7>=free_4 && free_4>=1 ], cost: 1
      4: f1 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_5, H'=0, Q'=0, J'=3, K'=free_5, L'=2, [ 7>=free_5 && 3>=free_5 && free_5>=1 ], cost: 1
      5: f1 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_6, H'=0, Q'=0, J'=3, K'=free_6, L'=2, [ 7>=free_6 && free_6>=5 ], cost: 1
      6: f1 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=3, G'=4, H'=1, Q'=0, J'=3, K'=4, L'=2, [], cost: 1
      7: f2 -> f7 : A'=1, B'=C, D'=E, F'=free_8, G'=free_7, Q'=1, J'=free_8, K'=free_7, L'=7, [ 7>=free_7 && 7>=free_8 && 3>=free_7 && free_7>=1 && free_8>=1 ], cost: 1
      8: f2 -> f7 : A'=1, B'=C, D'=E, F'=free_10, G'=free_9, Q'=1, J'=free_10, K'=free_9, L'=7, [ 7>=free_9 && 7>=free_10 && free_9>=5 && free_10>=1 ], cost: 1
      9: f2 -> f7 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_11, G'=4, H'=1, Q'=1, J'=free_11, K'=4, L'=7, [ 7>=free_11 && free_11>=1 ], cost: 1
     10: f2 -> f3 : A'=0, B'=C, D'=E, F'=free_13, G'=free_12, Q'=0, J'=free_13, K'=free_12, L'=3, [ 7>=free_12 && 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 ], cost: 1
     11: f2 -> f3 : A'=0, B'=C, D'=E, F'=free_15, G'=free_14, Q'=0, J'=free_15, K'=free_14, L'=3, [ 7>=free_14 && 7>=free_15 && free_14>=5 && free_15>=1 ], cost: 1
     12: f2 -> f3 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_16, G'=4, H'=1, Q'=0, J'=free_16, K'=4, L'=3, [ 7>=free_16 && free_16>=1 ], cost: 1
     13: f3 -> f6 : A'=1, B'=C, D'=E, F'=free_18, G'=free_17, Q'=1, J'=free_18, K'=free_17, L'=6, [ 7>=free_17 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 ], cost: 1
     14: f3 -> f6 : A'=1, B'=C, D'=E, F'=free_20, G'=free_19, Q'=1, J'=free_20, K'=free_19, L'=6, [ 7>=free_19 && 7>=free_20 && free_19>=5 && free_20>=1 ], cost: 1
     15: f3 -> f6 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_21, G'=4, H'=1, Q'=1, J'=free_21, K'=4, L'=6, [ 7>=free_21 && free_21>=1 ], cost: 1
     16: f6 -> f4 : A'=free_23, B'=C, D'=E, F'=free_22, G'=2, H'=0, Q'=free_23, J'=free_22, K'=2, L'=4, [ 7>=free_22 && 1>=free_23 && free_23>=0 && free_22>=1 ], cost: 1
     17: f6 -> f4 : A'=free_25, B'=C, D'=E, F'=free_24, G'=7, H'=1, Q'=free_25, J'=free_24, K'=7, L'=4, [ 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 ], cost: 1
     21: f4 -> f7 : A'=0, B'=C, D'=E, F'=free_34, G'=free_33, Q'=0, J'=free_34, K'=free_33, L'=7, [ E>=M && C>=N && 7>=free_33 && 7>=free_34 && 3>=free_33 && free_33>=1 && free_34>=1 ], cost: 1
     22: f4 -> f7 : A'=0, B'=C, D'=E, F'=free_36, G'=free_35, Q'=0, J'=free_36, K'=free_35, L'=7, [ E>=M && C>=N && 7>=free_35 && 7>=free_36 && free_35>=5 && free_36>=1 ], cost: 1
     23: f4 -> f7 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_37, G'=4, H'=1, Q'=0, J'=free_37, K'=4, L'=7, [ 1+E>=M && 1+C>=N && 7>=free_37 && free_37>=1 ], cost: 1
     24: f4 -> f7 : A'=1, B'=C, D'=E, F'=free_39, G'=free_38, Q'=1, J'=free_39, K'=free_38, L'=7, [ 7>=free_38 && 7>=free_39 && 3>=free_38 && free_38>=1 && free_39>=1 ], cost: 1
     25: f4 -> f7 : A'=1, B'=C, D'=E, F'=free_41, G'=free_40, Q'=1, J'=free_41, K'=free_40, L'=7, [ 7>=free_40 && 7>=free_41 && free_40>=5 && free_41>=1 ], cost: 1
     26: f4 -> f7 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_42, G'=4, H'=1, Q'=1, J'=free_42, K'=4, L'=7, [ 7>=free_42 && free_42>=1 ], cost: 1
     18: f4 -> f2 : A'=0, B'=C, D'=E, F'=free_27, G'=free_26, H'=0, Q'=0, J'=free_27, K'=free_26, L'=2, [ M>=1+free_28 && N>=1+free_29 && M>=1 && N>=1 && 7>=free_26 && 7>=free_27 && 3>=free_26 && free_26>=1 && free_27>=1 && H==1 ], cost: 1
     19: f4 -> f2 : A'=0, B'=C, D'=E, F'=free_31, G'=free_30, H'=0, Q'=0, J'=free_31, K'=free_30, L'=2, [ M>=1 && M>=1+E && N>=1 && N>=1+C && 7>=free_30 && 7>=free_31 && free_30>=5 && free_31>=1 && H==1 ], cost: 1
     20: f4 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      4: f1 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_5, H'=0, Q'=0, J'=3, K'=free_5, L'=2, [ 3>=free_5 && free_5>=1 ], cost: 1
      5: f1 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_6, H'=0, Q'=0, J'=3, K'=free_6, L'=2, [ 7>=free_6 && free_6>=5 ], cost: 1
      6: f1 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=3, G'=4, H'=1, Q'=0, J'=3, K'=4, L'=2, [], cost: 1
     10: f2 -> f3 : A'=0, B'=C, D'=E, F'=free_13, G'=free_12, Q'=0, J'=free_13, K'=free_12, L'=3, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 ], cost: 1
     11: f2 -> f3 : A'=0, B'=C, D'=E, F'=free_15, G'=free_14, Q'=0, J'=free_15, K'=free_14, L'=3, [ 7>=free_14 && 7>=free_15 && free_14>=5 && free_15>=1 ], cost: 1
     12: f2 -> f3 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_16, G'=4, H'=1, Q'=0, J'=free_16, K'=4, L'=3, [ 7>=free_16 && free_16>=1 ], cost: 1
     13: f3 -> f6 : A'=1, B'=C, D'=E, F'=free_18, G'=free_17, Q'=1, J'=free_18, K'=free_17, L'=6, [ 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 ], cost: 1
     14: f3 -> f6 : A'=1, B'=C, D'=E, F'=free_20, G'=free_19, Q'=1, J'=free_20, K'=free_19, L'=6, [ 7>=free_19 && 7>=free_20 && free_19>=5 && free_20>=1 ], cost: 1
     15: f3 -> f6 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_21, G'=4, H'=1, Q'=1, J'=free_21, K'=4, L'=6, [ 7>=free_21 && free_21>=1 ], cost: 1
     16: f6 -> f4 : A'=free_23, B'=C, D'=E, F'=free_22, G'=2, H'=0, Q'=free_23, J'=free_22, K'=2, L'=4, [ 7>=free_22 && 1>=free_23 && free_23>=0 && free_22>=1 ], cost: 1
     17: f6 -> f4 : A'=free_25, B'=C, D'=E, F'=free_24, G'=7, H'=1, Q'=free_25, J'=free_24, K'=7, L'=4, [ 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 ], cost: 1
     18: f4 -> f2 : A'=0, B'=C, D'=E, F'=free_27, G'=free_26, H'=0, Q'=0, J'=free_27, K'=free_26, L'=2, [ M>=1 && N>=1 && 7>=free_27 && 3>=free_26 && free_26>=1 && free_27>=1 && H==1 ], cost: 1
     19: f4 -> f2 : A'=0, B'=C, D'=E, F'=free_31, G'=free_30, H'=0, Q'=0, J'=free_31, K'=free_30, L'=2, [ M>=1 && M>=1+E && N>=1 && N>=1+C && 7>=free_30 && 7>=free_31 && free_30>=5 && free_31>=1 && H==1 ], cost: 1
     20: f4 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     27: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_5, H'=0, Q'=0, J'=3, K'=free_5, L'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_6, H'=0, Q'=0, J'=3, K'=free_6, L'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=3, G'=4, H'=1, Q'=0, J'=3, K'=4, L'=2, [], cost: 2
     30: f2 -> f6 : A'=1, B'=C, D'=E, F'=free_18, G'=free_17, Q'=1, J'=free_18, K'=free_17, L'=6, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 ], cost: 2
     31: f2 -> f6 : A'=1, B'=C, D'=E, F'=free_20, G'=free_19, Q'=1, J'=free_20, K'=free_19, L'=6, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_19 && 7>=free_20 && free_19>=5 && free_20>=1 ], cost: 2
     33: f2 -> f6 : A'=1, B'=C, D'=E, F'=free_18, G'=free_17, Q'=1, J'=free_18, K'=free_17, L'=6, [ 7>=free_14 && 7>=free_15 && free_14>=5 && free_15>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 ], cost: 2
     34: f2 -> f6 : A'=1, B'=C, D'=E, F'=free_20, G'=free_19, Q'=1, J'=free_20, K'=free_19, L'=6, [ 7>=free_14 && 7>=free_15 && free_14>=5 && free_15>=1 && 7>=free_19 && 7>=free_20 && free_19>=5 && free_20>=1 ], cost: 2
     36: f2 -> f6 : A'=1, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_18, G'=free_17, H'=1, Q'=1, J'=free_18, K'=free_17, L'=6, [ 7>=free_16 && free_16>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 ], cost: 2
     39: f6 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ 7>=free_22 && 1>=free_23 && free_23>=0 && free_22>=1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 2
     40: f6 -> f2 : A'=0, B'=C, D'=E, F'=free_27, G'=free_26, H'=0, Q'=0, J'=free_27, K'=free_26, L'=2, [ 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=1 && N>=1 && 7>=free_27 && 3>=free_26 && free_26>=1 && free_27>=1 && 1==1 ], cost: 2
     41: f6 -> f2 : A'=0, B'=C, D'=E, F'=free_31, G'=free_30, H'=0, Q'=0, J'=free_31, K'=free_30, L'=2, [ 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=1 && M>=1+E && N>=1 && N>=1+C && 7>=free_30 && 7>=free_31 && free_30>=5 && free_31>=1 && 1==1 ], cost: 2
     42: f6 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     27: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_5, H'=0, Q'=0, J'=3, K'=free_5, L'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_6, H'=0, Q'=0, J'=3, K'=free_6, L'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=3, G'=4, H'=1, Q'=0, J'=3, K'=4, L'=2, [], cost: 2
     43: f2 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 && 7>=free_22 && 1>=free_23 && free_23>=0 && free_22>=1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 4
     44: f2 -> f2 : A'=0, B'=C, D'=E, F'=free_27, G'=free_26, H'=0, Q'=0, J'=free_27, K'=free_26, L'=2, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 && 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=1 && N>=1 && 7>=free_27 && 3>=free_26 && free_26>=1 && free_27>=1 && 1==1 ], cost: 4
     46: f2 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 && 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 4
     50: f2 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ 7>=free_13 && 3>=free_12 && free_12>=1 && free_13>=1 && 7>=free_19 && 7>=free_20 && free_19>=5 && free_20>=1 && 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 4
     53: f2 -> f2 : A'=0, B'=C, D'=E, F'=free_31, G'=free_30, H'=0, Q'=0, J'=free_31, K'=free_30, L'=2, [ 7>=free_14 && 7>=free_15 && free_14>=5 && free_15>=1 && 7>=free_18 && 3>=free_17 && free_17>=1 && free_18>=1 && 7>=free_24 && 1>=free_25 && free_25>=0 && free_24>=1 && H==1 && M>=1 && M>=1+E && N>=1 && N>=1+C && 7>=free_30 && 7>=free_31 && free_30>=5 && free_31>=1 && 1==1 ], cost: 4

Eliminating 5 self-loops for location f2
  Self-Loop 44 has the metering function: H, resulting in the new transition 64.
  Self-Loop 46 has the metering function: -1+H, resulting in the new transition 65.
  Self-Loop 50 has the metering function: -1+H, resulting in the new transition 66.
  Self-Loop 53 has the metering function: H, resulting in the new transition 67.
  Found this metering function when nesting loops: -1+H,
  Found this metering function when nesting loops: H,
  Found this metering function when nesting loops: H,
  Found this metering function when nesting loops: -1+H,
  Removing the self-loops: 43 44 46 50 53.
Adding an epsilon transition (to model nonexecution of the loops): 68.
Removing duplicate transition: 65.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     27: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_5, H'=0, Q'=0, J'=3, K'=free_5, L'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : A'=0, B'=C, D'=E, F'=3, G'=free_6, H'=0, Q'=0, J'=3, K'=free_6, L'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=3, G'=4, H'=1, Q'=0, J'=3, K'=4, L'=2, [], cost: 2
     63: f2 -> [7] : A'=0, B'=1+C, C'=1+C, D'=1+E, E'=1+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: 4
     64: f2 -> [7] : A'=0, B'=C, D'=E, F'=free_27, G'=free_26, H'=0, Q'=0, J'=free_27, K'=free_26, L'=2, [ H==1 && M>=1 && N>=1 && 7>=free_27 && 3>=free_26 && free_26>=1 && free_27>=1 ], cost: 4*H
     66: f2 -> [7] : A'=0, B'=-1+H+C, C'=-1+H+C, D'=-1+H+E, E'=-1+H+E, F'=free_32, G'=4, H'=0, Q'=0, J'=free_32, K'=4, L'=2, [ H==1 && M>=2+E && N>=2+C && M>=1 && N>=1 && 7>=free_32 && free_32>=1 ], cost: -4+4*H
     67: f2 -> [7] : A'=0, B'=C, D'=E, F'=free_31, G'=free_30, H'=0, Q'=0, J'=free_31, K'=free_30, L'=2, [ H==1 && M>=1 && M>=1+E && N>=1 && N>=1+C && 7>=free_30 && 7>=free_31 && free_30>=5 && free_31>=1 ], cost: 4*H
     68: f2 -> [7] : [], cost: 0


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),?)