Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f8
      0: f13 -> f31 : A'=free_1, B'=free, C'=-1+C, D'=-1+C, [ 0>=1+free ], cost: 1
      1: f13 -> f31 : A'=free_3, B'=free_2, C'=-1+C, D'=-1+C, [ free_2>=1 ], cost: 1
      2: f13 -> f29 : A'=free_4, B'=0, C'=-2+D, D'=-1+D, [], cost: 1
     45: f31 -> f31 : A'=free_69, B'=free_68, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_68 && C+D>=1 && E==1 ], cost: 1
     46: f31 -> f31 : A'=free_71, B'=free_70, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_70>=1 && C+D>=1 && E==1 ], cost: 1
     48: f31 -> f31 : A'=free_74, B'=free_73, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_73 && C+D>=1 && E==1 ], cost: 1
     49: f31 -> f31 : A'=free_76, B'=free_75, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_75>=1 && C+D>=1 && E==1 ], cost: 1
     47: f31 -> f29 : A'=free_72, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     50: f31 -> f29 : A'=free_77, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     51: f31 -> f9 : J'=free_78, [ 0>=C ], cost: 1
     44: f31 -> f300 : E'=1, F'=1, [ D>=Q && C>=H && C+D>=H+Q && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     28: f29 -> f31 : A'=free_46, B'=free_45, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_45 && C+D>=1 && E==1 ], cost: 1
     29: f29 -> f31 : A'=free_48, B'=free_47, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_47>=1 && C+D>=1 && E==1 ], cost: 1
     31: f29 -> f31 : A'=free_51, B'=free_50, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_50 && C+D>=1 && E==1 ], cost: 1
     32: f29 -> f31 : A'=free_53, B'=free_52, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_52>=1 && C+D>=1 && E==1 ], cost: 1
     30: f29 -> f29 : A'=free_49, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     33: f29 -> f29 : A'=free_54, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     34: f29 -> f9 : J'=free_55, [ 0>=C ], cost: 1
     35: f29 -> f9 : J'=free_56, [ C>=1 && 0>=D ], cost: 1
     27: f29 -> f300 : E'=1, F'=1, [ D>=Q && C>=H && C+D>=H+Q && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
      3: f19 -> f31 : A'=free_6, B'=free_5, C'=-1+C, D'=-1+C, [ 0>=1+free_5 ], cost: 1
      4: f19 -> f31 : A'=free_8, B'=free_7, C'=-1+C, D'=-1+C, [ free_7>=1 ], cost: 1
      5: f19 -> f29 : A'=free_9, B'=0, C'=-2+D, D'=-1+D, [], cost: 1
      6: f8 -> f27 : E'=0, F'=0, [], cost: 1
      7: f27 -> f27 : A'=free_10, B'=0, C'=-2+D, D'=-1+D, E'=0, G'=0, [ D>=1 && C+D>=1 && C>=1 && E==0 ], cost: 1
      8: f27 -> f27 : A'=free_12, B'=free_11, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && E==0 ], cost: 1
      9: f27 -> f27 : A'=free_14, B'=free_13, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && E==0 ], cost: 1
     10: f27 -> f30 : A'=free_16, B'=free_15, C'=-1+C, D'=-1+C, E'=1, G'=free_17, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_15 && 0>=1+free_17 && E==0 ], cost: 1
     11: f27 -> f30 : A'=free_19, B'=free_18, C'=-1+C, D'=-1+C, E'=1, G'=free_20, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_18 && free_20>=1 && E==0 ], cost: 1
     12: f27 -> f30 : A'=free_22, B'=free_21, C'=-1+C, D'=-1+C, E'=1, G'=free_23, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_21>=1 && 0>=1+free_23 && E==0 ], cost: 1
     13: f27 -> f30 : A'=free_25, B'=free_24, C'=-1+C, D'=-1+C, E'=1, G'=free_26, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_24>=1 && free_26>=1 && E==0 ], cost: 1
     14: f27 -> f28 : A'=free_28, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_27, H'=C, Q'=D, [ D>=1 && C>=1 && 0>=1+free_27 && C+D>=1 && E==0 ], cost: 1
     15: f27 -> f28 : A'=free_30, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_29, H'=C, Q'=D, [ D>=1 && C>=1 && free_29>=1 && C+D>=1 && E==0 ], cost: 1
     16: f27 -> f9 : J'=free_31, [ 0>=C ], cost: 1
     17: f27 -> f9 : J'=free_32, [ C>=1 && 0>=D ], cost: 1
     37: f30 -> f30 : A'=free_58, B'=free_57, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 ], cost: 1
     38: f30 -> f30 : A'=free_60, B'=free_59, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 ], cost: 1
     40: f30 -> f30 : A'=free_63, B'=free_62, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 ], cost: 1
     41: f30 -> f30 : A'=free_65, B'=free_64, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 ], cost: 1
     39: f30 -> f28 : A'=free_61, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     42: f30 -> f28 : A'=free_66, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     43: f30 -> f9 : J'=free_67, [ 0>=C ], cost: 1
     36: f30 -> f300 : E'=1, F'=1, [ D>=Q && C>=H && C+D>=H+Q && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     19: f28 -> f30 : A'=free_34, B'=free_33, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_33 && C+D>=1 && E==1 ], cost: 1
     20: f28 -> f30 : A'=free_36, B'=free_35, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_35>=1 && C+D>=1 && E==1 ], cost: 1
     22: f28 -> f30 : A'=free_39, B'=free_38, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_38 && C+D>=1 && E==1 ], cost: 1
     23: f28 -> f30 : A'=free_41, B'=free_40, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_40>=1 && C+D>=1 && E==1 ], cost: 1
     21: f28 -> f28 : A'=free_37, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     24: f28 -> f28 : A'=free_42, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     25: f28 -> f9 : J'=free_43, [ 0>=C ], cost: 1
     26: f28 -> f9 : J'=free_44, [ C>=1 && 0>=D ], cost: 1
     18: f28 -> f300 : E'=1, F'=1, [ D>=Q && C>=H && C+D>=H+Q && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1


Simplified the transitions:
  Start location: f8
      6: f8 -> f27 : E'=0, F'=0, [], cost: 1
      7: f27 -> f27 : A'=free_10, B'=0, C'=-2+D, D'=-1+D, E'=0, G'=0, [ D>=1 && C+D>=1 && C>=1 && E==0 ], cost: 1
      8: f27 -> f27 : A'=free_12, B'=free_11, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && E==0 ], cost: 1
      9: f27 -> f27 : A'=free_14, B'=free_13, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && E==0 ], cost: 1
     10: f27 -> f30 : A'=free_16, B'=free_15, C'=-1+C, D'=-1+C, E'=1, G'=free_17, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_15 && 0>=1+free_17 && E==0 ], cost: 1
     11: f27 -> f30 : A'=free_19, B'=free_18, C'=-1+C, D'=-1+C, E'=1, G'=free_20, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_18 && free_20>=1 && E==0 ], cost: 1
     12: f27 -> f30 : A'=free_22, B'=free_21, C'=-1+C, D'=-1+C, E'=1, G'=free_23, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_21>=1 && 0>=1+free_23 && E==0 ], cost: 1
     13: f27 -> f30 : A'=free_25, B'=free_24, C'=-1+C, D'=-1+C, E'=1, G'=free_26, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_24>=1 && free_26>=1 && E==0 ], cost: 1
     14: f27 -> f28 : A'=free_28, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_27, H'=C, Q'=D, [ D>=1 && C>=1 && 0>=1+free_27 && C+D>=1 && E==0 ], cost: 1
     15: f27 -> f28 : A'=free_30, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_29, H'=C, Q'=D, [ D>=1 && C>=1 && free_29>=1 && C+D>=1 && E==0 ], cost: 1
     37: f30 -> f30 : A'=free_58, B'=free_57, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 ], cost: 1
     38: f30 -> f30 : A'=free_60, B'=free_59, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 ], cost: 1
     40: f30 -> f30 : A'=free_63, B'=free_62, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 ], cost: 1
     41: f30 -> f30 : A'=free_65, B'=free_64, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 ], cost: 1
     39: f30 -> f28 : A'=free_61, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     42: f30 -> f28 : A'=free_66, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     19: f28 -> f30 : A'=free_34, B'=free_33, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_33 && C+D>=1 && E==1 ], cost: 1
     20: f28 -> f30 : A'=free_36, B'=free_35, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_35>=1 && C+D>=1 && E==1 ], cost: 1
     22: f28 -> f30 : A'=free_39, B'=free_38, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_38 && C+D>=1 && E==1 ], cost: 1
     23: f28 -> f30 : A'=free_41, B'=free_40, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_40>=1 && C+D>=1 && E==1 ], cost: 1
     21: f28 -> f28 : A'=free_37, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     24: f28 -> f28 : A'=free_42, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1

Eliminating 3 self-loops for location f27
  Removing the self-loops: 7 8 9.
Adding an epsilon transition (to model nonexecution of the loops): 55.
Eliminating 4 self-loops for location f30
  Removing the self-loops: 37 38 40 41.
Adding an epsilon transition (to model nonexecution of the loops): 60.
Eliminating 2 self-loops for location f28
  Removing the self-loops: 21 24.
Adding an epsilon transition (to model nonexecution of the loops): 63.

Removed all Self-loops using metering functions (where possible):
  Start location: f8
      6: f8 -> f27 : E'=0, F'=0, [], cost: 1
     52: f27 -> [10] : A'=free_10, B'=0, C'=-2+D, D'=-1+D, E'=0, G'=0, [ D>=1 && C+D>=1 && C>=1 && E==0 ], cost: 1
     53: f27 -> [10] : A'=free_12, B'=free_11, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && E==0 ], cost: 1
     54: f27 -> [10] : A'=free_14, B'=free_13, C'=-1+C, D'=-1+C, E'=0, G'=0, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && E==0 ], cost: 1
     55: f27 -> [10] : [], cost: 0
     56: f30 -> [11] : A'=free_58, B'=free_57, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 ], cost: 1
     57: f30 -> [11] : A'=free_60, B'=free_59, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 ], cost: 1
     58: f30 -> [11] : A'=free_63, B'=free_62, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 ], cost: 1
     59: f30 -> [11] : A'=free_65, B'=free_64, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 ], cost: 1
     60: f30 -> [11] : [], cost: 0
     61: f28 -> [12] : A'=free_37, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     62: f28 -> [12] : A'=free_42, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     63: f28 -> [12] : [], cost: 0
     10: [10] -> f30 : A'=free_16, B'=free_15, C'=-1+C, D'=-1+C, E'=1, G'=free_17, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_15 && 0>=1+free_17 && E==0 ], cost: 1
     11: [10] -> f30 : A'=free_19, B'=free_18, C'=-1+C, D'=-1+C, E'=1, G'=free_20, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_18 && free_20>=1 && E==0 ], cost: 1
     12: [10] -> f30 : A'=free_22, B'=free_21, C'=-1+C, D'=-1+C, E'=1, G'=free_23, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_21>=1 && 0>=1+free_23 && E==0 ], cost: 1
     13: [10] -> f30 : A'=free_25, B'=free_24, C'=-1+C, D'=-1+C, E'=1, G'=free_26, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_24>=1 && free_26>=1 && E==0 ], cost: 1
     14: [10] -> f28 : A'=free_28, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_27, H'=C, Q'=D, [ D>=1 && C>=1 && 0>=1+free_27 && C+D>=1 && E==0 ], cost: 1
     15: [10] -> f28 : A'=free_30, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_29, H'=C, Q'=D, [ D>=1 && C>=1 && free_29>=1 && C+D>=1 && E==0 ], cost: 1
     39: [11] -> f28 : A'=free_61, B'=0, C'=-2+D, D'=-1+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     42: [11] -> f28 : A'=free_66, B'=0, C'=-2+D, D'=-1+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 ], cost: 1
     19: [12] -> f30 : A'=free_34, B'=free_33, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_33 && C+D>=1 && E==1 ], cost: 1
     20: [12] -> f30 : A'=free_36, B'=free_35, C'=-1+C, D'=-1+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_35>=1 && C+D>=1 && E==1 ], cost: 1
     22: [12] -> f30 : A'=free_39, B'=free_38, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_38 && C+D>=1 && E==1 ], cost: 1
     23: [12] -> f30 : A'=free_41, B'=free_40, C'=-1+C, D'=-1+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_40>=1 && C+D>=1 && E==1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f8
     64: f8 -> [10] : A'=free_10, B'=0, C'=-2+D, D'=-1+D, E'=0, F'=0, G'=0, [ D>=1 && C+D>=1 && C>=1 && 0==0 ], cost: 2
     65: f8 -> [10] : A'=free_12, B'=free_11, C'=-1+C, D'=-1+C, E'=0, F'=0, G'=0, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && 0==0 ], cost: 2
     66: f8 -> [10] : A'=free_14, B'=free_13, C'=-1+C, D'=-1+C, E'=0, F'=0, G'=0, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 ], cost: 2
     67: f8 -> [10] : E'=0, F'=0, [], cost: 1
     68: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     69: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     71: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     72: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     73: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     76: f28 -> f30 : A'=free_34, B'=free_33, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && 0>=1+free_33 && -3+2*D>=1 && 1==1 ], cost: 2
     77: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     79: f28 -> f30 : A'=free_41, B'=free_40, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && free_40>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     81: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     82: f28 -> f30 : A'=free_39, B'=free_38, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && 0>=1+free_38 && -3+2*D>=1 && 1==1 ], cost: 2
     10: [10] -> f30 : A'=free_16, B'=free_15, C'=-1+C, D'=-1+C, E'=1, G'=free_17, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_15 && 0>=1+free_17 && E==0 ], cost: 1
     11: [10] -> f30 : A'=free_19, B'=free_18, C'=-1+C, D'=-1+C, E'=1, G'=free_20, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && 0>=1+free_18 && free_20>=1 && E==0 ], cost: 1
     12: [10] -> f30 : A'=free_22, B'=free_21, C'=-1+C, D'=-1+C, E'=1, G'=free_23, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_21>=1 && 0>=1+free_23 && E==0 ], cost: 1
     13: [10] -> f30 : A'=free_25, B'=free_24, C'=-1+C, D'=-1+C, E'=1, G'=free_26, H'=C, Q'=D, [ D>=1 && C>=1 && C+D>=1 && free_24>=1 && free_26>=1 && E==0 ], cost: 1
     14: [10] -> f28 : A'=free_28, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_27, H'=C, Q'=D, [ D>=1 && C>=1 && 0>=1+free_27 && C+D>=1 && E==0 ], cost: 1
     15: [10] -> f28 : A'=free_30, B'=0, C'=-2+D, D'=-1+D, E'=1, G'=free_29, H'=C, Q'=D, [ D>=1 && C>=1 && free_29>=1 && C+D>=1 && E==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f8
     88: f8 -> f30 : A'=free_16, B'=free_15, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_17, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && 0>=1+free_15 && 0>=1+free_17 && 0==0 ], cost: 3
     89: f8 -> f30 : A'=free_19, B'=free_18, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_20, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && 0>=1+free_18 && free_20>=1 && 0==0 ], cost: 3
     91: f8 -> f30 : A'=free_25, B'=free_24, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_26, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && free_24>=1 && free_26>=1 && 0==0 ], cost: 3
     97: f8 -> f30 : A'=free_25, B'=free_24, C'=-2+C, D'=-2+C, E'=1, F'=0, G'=free_26, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && -2+2*C>=1 && free_24>=1 && free_26>=1 && 0==0 ], cost: 3
    101: f8 -> f30 : A'=free_19, B'=free_18, C'=-2+C, D'=-2+C, E'=1, F'=0, G'=free_20, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && -2+2*C>=1 && 0>=1+free_18 && free_20>=1 && 0==0 ], cost: 3
     92: f8 -> f28 : A'=free_28, B'=0, C'=-3+D, D'=-2+D, E'=1, F'=0, G'=free_27, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && 0>=1+free_27 && -3+2*D>=1 && 0==0 ], cost: 3
     93: f8 -> f28 : A'=free_30, B'=0, C'=-3+D, D'=-2+D, E'=1, F'=0, G'=free_29, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && free_29>=1 && -3+2*D>=1 && 0==0 ], cost: 3
     99: f8 -> f28 : A'=free_30, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_29, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && free_29>=1 && -2+2*C>=1 && 0==0 ], cost: 3
    104: f8 -> f28 : A'=free_28, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_27, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && 0>=1+free_27 && -2+2*C>=1 && 0==0 ], cost: 3
    105: f8 -> f28 : A'=free_30, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_29, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && free_29>=1 && -2+2*C>=1 && 0==0 ], cost: 3
     68: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     69: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     71: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     72: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     73: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     76: f28 -> f30 : A'=free_34, B'=free_33, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && 0>=1+free_33 && -3+2*D>=1 && 1==1 ], cost: 2
     77: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     79: f28 -> f30 : A'=free_41, B'=free_40, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && free_40>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     81: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     82: f28 -> f30 : A'=free_39, B'=free_38, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && 0>=1+free_38 && -3+2*D>=1 && 1==1 ], cost: 2


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f8
     88: f8 -> f30 : A'=free_16, B'=free_15, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_17, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && 0>=1+free_15 && 0>=1+free_17 && 0==0 ], cost: 3
     89: f8 -> f30 : A'=free_19, B'=free_18, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_20, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && 0>=1+free_18 && free_20>=1 && 0==0 ], cost: 3
     91: f8 -> f30 : A'=free_25, B'=free_24, C'=-3+D, D'=-3+D, E'=1, F'=0, G'=free_26, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && -3+2*D>=1 && free_24>=1 && free_26>=1 && 0==0 ], cost: 3
     97: f8 -> f30 : A'=free_25, B'=free_24, C'=-2+C, D'=-2+C, E'=1, F'=0, G'=free_26, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && -2+2*C>=1 && free_24>=1 && free_26>=1 && 0==0 ], cost: 3
    101: f8 -> f30 : A'=free_19, B'=free_18, C'=-2+C, D'=-2+C, E'=1, F'=0, G'=free_20, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && -2+2*C>=1 && 0>=1+free_18 && free_20>=1 && 0==0 ], cost: 3
     92: f8 -> f28 : A'=free_28, B'=0, C'=-3+D, D'=-2+D, E'=1, F'=0, G'=free_27, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && 0>=1+free_27 && -3+2*D>=1 && 0==0 ], cost: 3
     93: f8 -> f28 : A'=free_30, B'=0, C'=-3+D, D'=-2+D, E'=1, F'=0, G'=free_29, H'=-2+D, Q'=-1+D, [ D>=1 && C+D>=1 && C>=1 && 0==0 && -1+D>=1 && -2+D>=1 && free_29>=1 && -3+2*D>=1 && 0==0 ], cost: 3
     99: f8 -> f28 : A'=free_30, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_29, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && 0>=1+free_11 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && free_29>=1 && -2+2*C>=1 && 0==0 ], cost: 3
    104: f8 -> f28 : A'=free_28, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_27, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && 0>=1+free_27 && -2+2*C>=1 && 0==0 ], cost: 3
    105: f8 -> f28 : A'=free_30, B'=0, C'=-3+C, D'=-2+C, E'=1, F'=0, G'=free_29, H'=-1+C, Q'=-1+C, [ D>=1 && C>=1 && free_13>=1 && C+D>=1 && 0==0 && -1+C>=1 && -1+C>=1 && free_29>=1 && -2+2*C>=1 && 0==0 ], cost: 3
     68: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && 0>=1+free_57 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     69: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ H>=1+C && D>=1 && C>=1 && free_59>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     71: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && 0>=1+free_62 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     72: f30 -> f28 : A'=free_61, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && H>=C && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     73: f30 -> f28 : A'=free_66, B'=0, C'=-3+C, D'=-2+C, E'=1, [ Q>=1+D && C>=H && D>=1 && C>=1 && free_64>=1 && C+D>=1 && E==1 && Q>=C && -1+C>=H && -1+C>=1 && -2+2*C>=1 && -1+C>=1 && 1==1 ], cost: 2
     76: f28 -> f30 : A'=free_34, B'=free_33, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && 0>=1+free_33 && -3+2*D>=1 && 1==1 ], cost: 2
     77: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     79: f28 -> f30 : A'=free_41, B'=free_40, C'=-3+D, D'=-3+D, E'=1, [ H>=1+C && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && free_40>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     81: f28 -> f30 : A'=free_36, B'=free_35, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && H>=-1+D && -1+D>=1 && -2+D>=1 && free_35>=1 && -3+2*D>=1 && 1==1 ], cost: 2
     82: f28 -> f30 : A'=free_39, B'=free_38, C'=-3+D, D'=-3+D, E'=1, [ Q>=1+D && C>=H && D>=1 && C+D>=1 && C>=1 && E==1 && Q>=D && -2+D>=H && -1+D>=1 && -2+D>=1 && 0>=1+free_38 && -3+2*D>=1 && 1==1 ], cost: 2

This is only a partial result (probably due to a timeout), trying to find max complexity

Removed transitions with const cost
  Start location: f8
    <empty>


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