Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1entryin : [], cost: 1
      1: evalrealheapsortstep1entryin -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 1
      2: evalrealheapsortstep1entryin -> evalrealheapsortstep1returnin : [ 2>=A ], cost: 1
      4: evalrealheapsortstep1bb6in -> evalrealheapsortstep1returnin : [ B>=A ], cost: 1
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
     41: evalrealheapsortstep1returnin -> evalrealheapsortstep1stop : [], cost: 1
      5: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb5in : [ 0>=C ], cost: 1
      6: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb4in : [ C>=1 ], cost: 1
     40: evalrealheapsortstep1bb5in -> evalrealheapsortstep1bb6in : B'=1+B, [], cost: 1
     10: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 1+C==0 ], cost: 1
     11: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 1
     12: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 0>=2+C && 0>=free_3 && 2*free_3>=1+C && 2+C>=2*free_3 ], cost: 1
      7: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 1+C==0 ], cost: 1
      8: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ C>=0 && free>=0 && 1+C>=2*free && 2*free>=C ], cost: 1
      9: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 0>=2+C && 0>=free_1 && 2*free_1>=1+C && 2+C>=2*free_1 ], cost: 1
     13: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 1+C==0 ], cost: 1
     14: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_4, [ 0>=1 && free_4>=0 && 0>=2*free_4 && 1+2*free_4>=0 && 1+C==0 ], cost: 1
     15: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_5, [ 0>=1 && 0>=free_5 && 1+C==0 && 2*free_5>=1+C && 2+C>=2*free_5 ], cost: 1
     16: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && free_6>=0 && 0>=2*free_6 && 1+2*free_6>=0 && 1+C==0 ], cost: 1
     17: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_7, [ 0>=1 && free_8>=0 && 0>=2*free_8 && 1+2*free_8>=0 && free_7>=0 && 0>=2*free_7 && 1+2*free_7>=0 && 1+C==0 ], cost: 1
     18: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_9, [ 0>=1 && free_10>=0 && 0>=2*free_10 && 1+2*free_10>=0 && 0>=free_9 && 1+C==0 && 2*free_9>=1+C && 2+C>=2*free_9 ], cost: 1
     19: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && 0>=free_11 && 1+C==0 && 2*free_11>=1+C && 2+C>=2*free_11 ], cost: 1
     20: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_12, [ 0>=1 && 0>=free_13 && free_12>=0 && 0>=2*free_12 && 1+2*free_12>=0 && 1+C==0 && 2*free_13>=1+C && 2+C>=2*free_13 ], cost: 1
     21: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_14, [ 0>=1 && 0>=free_15 && 0>=free_14 && 1+C==0 && 2*free_15>=1+C && 2+C>=2*free_15 && 2*free_14>=1+C && 2+C>=2*free_14 ], cost: 1
     22: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && free_16>=0 && 0>=2*free_16 && 1+2*free_16>=0 && 1+C==0 ], cost: 1
     23: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_17, [ 0>=1 && free_18>=0 && 0>=2*free_18 && 1+2*free_18>=0 && free_17>=0 && 0>=2*free_17 && 1+2*free_17>=0 && 1+C==0 ], cost: 1
     24: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_19, [ 0>=1 && free_20>=0 && 0>=2*free_20 && 1+2*free_20>=0 && 0>=free_19 && 1+C==0 && 2*free_19>=1+C && 2+C>=2*free_19 ], cost: 1
     25: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && free_22>=0 && 0>=2*free_22 && 1+2*free_22>=0 && free_21>=0 && 0>=2*free_21 && 1+2*free_21>=0 && 1+C==0 ], cost: 1
     26: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_23, [ C>=0 && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 1
     27: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_26, [ C>=0 && free_27>=0 && 1+C>=2*free_27 && 2*free_27>=C && free_28>=0 && 1+C>=2*free_28 && 2*free_28>=C && 0>=2+C && 0>=free_26 && 2*free_26>=1+C && 2+C>=2*free_26 ], cost: 1
     28: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && free_30>=0 && 0>=2*free_30 && 1+2*free_30>=0 && 0>=free_29 && 1+C==0 && 2*free_29>=1+C && 2+C>=2*free_29 ], cost: 1
     29: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_31, [ C>=0 && free_32>=0 && 1+C>=2*free_32 && 2*free_32>=C && 0>=2+C && 0>=free_33 && free_31>=0 && 1+C>=2*free_31 && 2*free_31>=C && 2*free_33>=1+C && 2+C>=2*free_33 ], cost: 1
     30: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_34, [ C>=0 && free_35>=0 && 1+C>=2*free_35 && 2*free_35>=C && 0>=2+C && 0>=free_36 && 0>=free_34 && 2*free_36>=1+C && 2+C>=2*free_36 && 2*free_34>=1+C && 2+C>=2*free_34 ], cost: 1
     31: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && 0>=free_37 && 1+C==0 && 2*free_37>=1+C && 2+C>=2*free_37 ], cost: 1
     32: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_38, [ 0>=1 && 0>=free_39 && free_38>=0 && 0>=2*free_38 && 1+2*free_38>=0 && 1+C==0 && 2*free_39>=1+C && 2+C>=2*free_39 ], cost: 1
     33: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_40, [ 0>=1 && 0>=free_41 && 0>=free_40 && 1+C==0 && 2*free_41>=1+C && 2+C>=2*free_41 && 2*free_40>=1+C && 2+C>=2*free_40 ], cost: 1
     34: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && 0>=free_43 && free_42>=0 && 0>=2*free_42 && 1+2*free_42>=0 && 1+C==0 && 2*free_43>=1+C && 2+C>=2*free_43 ], cost: 1
     35: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_44, [ 0>=2+C && 0>=free_45 && C>=0 && free_46>=0 && 1+C>=2*free_46 && 2*free_46>=C && free_44>=0 && 1+C>=2*free_44 && 2*free_44>=C && 2*free_45>=1+C && 2+C>=2*free_45 ], cost: 1
     36: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_47, [ 0>=2+C && 0>=free_48 && C>=0 && free_49>=0 && 1+C>=2*free_49 && 2*free_49>=C && 0>=free_47 && 2*free_48>=1+C && 2+C>=2*free_48 && 2*free_47>=1+C && 2+C>=2*free_47 ], cost: 1
     37: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 && 0>=free_51 && 0>=free_50 && 1+C==0 && 2*free_51>=1+C && 2+C>=2*free_51 && 2*free_50>=1+C && 2+C>=2*free_50 ], cost: 1
     38: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_52, [ 0>=2+C && 0>=free_53 && 0>=free_54 && C>=0 && free_52>=0 && 1+C>=2*free_52 && 2*free_52>=C && 2*free_53>=1+C && 2+C>=2*free_53 && 2*free_54>=1+C && 2+C>=2*free_54 ], cost: 1
     39: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_55, [ 0>=2+C && 0>=free_56 && 0>=free_57 && 0>=free_55 && 2*free_56>=1+C && 2+C>=2*free_56 && 2*free_57>=1+C && 2+C>=2*free_57 && 2*free_55>=1+C && 2+C>=2*free_55 ], cost: 1

Removing duplicate transition: 16.
Removing duplicate transition: 19.
Removing duplicate transition: 22.
Removing duplicate transition: 25.
Removing duplicate transition: 28.
Removing duplicate transition: 31.
Removing duplicate transition: 34.

Simplified the transitions:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1entryin : [], cost: 1
      1: evalrealheapsortstep1entryin -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 1
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
      5: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb5in : [ 0>=C ], cost: 1
      6: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb4in : [ C>=1 ], cost: 1
     40: evalrealheapsortstep1bb5in -> evalrealheapsortstep1bb6in : B'=1+B, [], cost: 1
     10: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 1+C==0 ], cost: 1
     11: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 1
     12: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 0>=2+C && 0>=free_3 && 2*free_3>=1+C && 2+C>=2*free_3 ], cost: 1
      7: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 1+C==0 ], cost: 1
      8: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ C>=0 && free>=0 && 1+C>=2*free && 2*free>=C ], cost: 1
      9: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 0>=2+C && 0>=free_1 && 2*free_1>=1+C && 2+C>=2*free_1 ], cost: 1
     13: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 1+C==0 ], cost: 1
     14: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_4, [ 0>=1 ], cost: 1
     15: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_5, [ 0>=1 ], cost: 1
     17: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_7, [ 0>=1 ], cost: 1
     18: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_9, [ 0>=1 ], cost: 1
     20: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_12, [ 0>=1 ], cost: 1
     21: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_14, [ 0>=1 ], cost: 1
     23: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_17, [ 0>=1 ], cost: 1
     24: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_19, [ 0>=1 ], cost: 1
     26: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_23, [ C>=0 && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 1
     27: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_26, [ C>=0 && free_27>=0 && 1+C>=2*free_27 && 2*free_27>=C && free_28>=0 && 1+C>=2*free_28 && 2*free_28>=C && 0>=2+C && 0>=free_26 && 2*free_26>=1+C && 2+C>=2*free_26 ], cost: 1
     29: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_31, [ C>=0 && free_32>=0 && 1+C>=2*free_32 && 2*free_32>=C && 0>=2+C && 0>=free_33 && free_31>=0 && 1+C>=2*free_31 && 2*free_31>=C && 2*free_33>=1+C && 2+C>=2*free_33 ], cost: 1
     30: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_34, [ C>=0 && free_35>=0 && 1+C>=2*free_35 && 2*free_35>=C && 0>=2+C && 0>=free_36 && 0>=free_34 && 2*free_36>=1+C && 2+C>=2*free_36 && 2*free_34>=1+C && 2+C>=2*free_34 ], cost: 1
     32: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_38, [ 0>=1 ], cost: 1
     33: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_40, [ 0>=1 ], cost: 1
     35: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_44, [ 0>=2+C && 0>=free_45 && C>=0 && free_46>=0 && 1+C>=2*free_46 && 2*free_46>=C && free_44>=0 && 1+C>=2*free_44 && 2*free_44>=C && 2*free_45>=1+C && 2+C>=2*free_45 ], cost: 1
     36: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_47, [ 0>=2+C && 0>=free_48 && C>=0 && free_49>=0 && 1+C>=2*free_49 && 2*free_49>=C && 0>=free_47 && 2*free_48>=1+C && 2+C>=2*free_48 && 2*free_47>=1+C && 2+C>=2*free_47 ], cost: 1
     37: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 ], cost: 1
     38: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_52, [ 0>=2+C && 0>=free_53 && 0>=free_54 && C>=0 && free_52>=0 && 1+C>=2*free_52 && 2*free_52>=C && 2*free_53>=1+C && 2+C>=2*free_53 && 2*free_54>=1+C && 2+C>=2*free_54 ], cost: 1
     39: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_55, [ 0>=2+C && 0>=free_56 && 0>=free_57 && 0>=free_55 && 2*free_56>=1+C && 2+C>=2*free_56 && 2*free_57>=1+C && 2+C>=2*free_57 && 2*free_55>=1+C && 2+C>=2*free_55 ], cost: 1


Applied simple chaining:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
      5: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb5in : [ 0>=C ], cost: 1
      6: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb4in : [ C>=1 ], cost: 1
     40: evalrealheapsortstep1bb5in -> evalrealheapsortstep1bb6in : B'=1+B, [], cost: 1
     10: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 1+C==0 ], cost: 1
     11: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 1
     12: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb5in : [ 0>=2+C && 0>=free_3 && 2*free_3>=1+C && 2+C>=2*free_3 ], cost: 1
      7: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 1+C==0 ], cost: 1
      8: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ C>=0 && free>=0 && 1+C>=2*free && 2*free>=C ], cost: 1
      9: evalrealheapsortstep1bb4in -> evalrealheapsortstep1bb2in : [ 0>=2+C && 0>=free_1 && 2*free_1>=1+C && 2+C>=2*free_1 ], cost: 1
     13: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 1+C==0 ], cost: 1
     14: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_4, [ 0>=1 ], cost: 1
     15: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_5, [ 0>=1 ], cost: 1
     17: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_7, [ 0>=1 ], cost: 1
     18: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_9, [ 0>=1 ], cost: 1
     20: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_12, [ 0>=1 ], cost: 1
     21: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_14, [ 0>=1 ], cost: 1
     23: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_17, [ 0>=1 ], cost: 1
     24: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_19, [ 0>=1 ], cost: 1
     26: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_23, [ C>=0 && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 1
     27: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_26, [ C>=0 && free_27>=0 && 1+C>=2*free_27 && 2*free_27>=C && free_28>=0 && 1+C>=2*free_28 && 2*free_28>=C && 0>=2+C && 0>=free_26 && 2*free_26>=1+C && 2+C>=2*free_26 ], cost: 1
     29: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_31, [ C>=0 && free_32>=0 && 1+C>=2*free_32 && 2*free_32>=C && 0>=2+C && 0>=free_33 && free_31>=0 && 1+C>=2*free_31 && 2*free_31>=C && 2*free_33>=1+C && 2+C>=2*free_33 ], cost: 1
     30: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_34, [ C>=0 && free_35>=0 && 1+C>=2*free_35 && 2*free_35>=C && 0>=2+C && 0>=free_36 && 0>=free_34 && 2*free_36>=1+C && 2+C>=2*free_36 && 2*free_34>=1+C && 2+C>=2*free_34 ], cost: 1
     32: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_38, [ 0>=1 ], cost: 1
     33: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_40, [ 0>=1 ], cost: 1
     35: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_44, [ 0>=2+C && 0>=free_45 && C>=0 && free_46>=0 && 1+C>=2*free_46 && 2*free_46>=C && free_44>=0 && 1+C>=2*free_44 && 2*free_44>=C && 2*free_45>=1+C && 2+C>=2*free_45 ], cost: 1
     36: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_47, [ 0>=2+C && 0>=free_48 && C>=0 && free_49>=0 && 1+C>=2*free_49 && 2*free_49>=C && 0>=free_47 && 2*free_48>=1+C && 2+C>=2*free_48 && 2*free_47>=1+C && 2+C>=2*free_47 ], cost: 1
     37: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 0>=1 ], cost: 1
     38: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_52, [ 0>=2+C && 0>=free_53 && 0>=free_54 && C>=0 && free_52>=0 && 1+C>=2*free_52 && 2*free_52>=C && 2*free_53>=1+C && 2+C>=2*free_53 && 2*free_54>=1+C && 2+C>=2*free_54 ], cost: 1
     39: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_55, [ 0>=2+C && 0>=free_56 && 0>=free_57 && 0>=free_55 && 2*free_56>=1+C && 2+C>=2*free_56 && 2*free_57>=1+C && 2+C>=2*free_57 && 2*free_55>=1+C && 2+C>=2*free_55 ], cost: 1


Applied chaining over branches and pruning:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
      5: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb5in : [ 0>=C ], cost: 1
     42: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb5in : [ C>=1 && C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 2
     43: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb2in : [ C>=1 && C>=0 && free>=0 && 1+C>=2*free && 2*free>=C ], cost: 2
     40: evalrealheapsortstep1bb5in -> evalrealheapsortstep1bb6in : B'=1+B, [], cost: 1
     13: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1, [ 1+C==0 ], cost: 1
     14: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_4, [ 0>=1 ], cost: 1
     17: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_7, [ 0>=1 ], cost: 1
     26: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_23, [ C>=0 && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 1
     39: evalrealheapsortstep1bb2in -> evalrealheapsortstep1bb3in : C'=-1+free_55, [ 0>=2+C && 0>=free_56 && 0>=free_57 && 0>=free_55 && 2*free_56>=1+C && 2+C>=2*free_56 && 2*free_57>=1+C && 2+C>=2*free_57 && 2*free_55>=1+C && 2+C>=2*free_55 ], cost: 1


Applied chaining over branches and pruning:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
     44: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb6in : B'=1+B, [ 0>=C ], cost: 2
     45: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb6in : B'=1+B, [ C>=1 && C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 3
     46: evalrealheapsortstep1bb3in -> evalrealheapsortstep1bb3in : C'=-1+free_23, [ C>=1 && C>=0 && free>=0 && 1+C>=2*free && 2*free>=C && C>=0 && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 3

Eliminating 1 self-loops for location evalrealheapsortstep1bb3in
  Removing the self-loops: 46.
Adding an epsilon transition (to model nonexecution of the loops): 48.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
      3: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb3in : C'=B, [ A>=1+B ], cost: 1
     47: evalrealheapsortstep1bb3in -> [9] : C'=-1+free_23, [ C>=1 && free>=0 && 1+C>=2*free && 2*free>=C && free_24>=0 && 1+C>=2*free_24 && 2*free_24>=C && free_25>=0 && 1+C>=2*free_25 && 2*free_25>=C && free_23>=0 && 1+C>=2*free_23 && 2*free_23>=C ], cost: 3
     48: evalrealheapsortstep1bb3in -> [9] : [], cost: 0
     44: [9] -> evalrealheapsortstep1bb6in : B'=1+B, [ 0>=C ], cost: 2
     45: [9] -> evalrealheapsortstep1bb6in : B'=1+B, [ C>=1 && C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 3


Applied chaining over branches and pruning:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
     49: evalrealheapsortstep1bb6in -> [9] : C'=-1+free_23, [ A>=1+B && B>=1 && free>=0 && 1+B>=2*free && 2*free>=B && free_24>=0 && 1+B>=2*free_24 && 2*free_24>=B && free_25>=0 && 1+B>=2*free_25 && 2*free_25>=B && free_23>=0 && 1+B>=2*free_23 && 2*free_23>=B ], cost: 4
     50: evalrealheapsortstep1bb6in -> [9] : C'=B, [ A>=1+B ], cost: 1
     44: [9] -> evalrealheapsortstep1bb6in : B'=1+B, [ 0>=C ], cost: 2
     45: [9] -> evalrealheapsortstep1bb6in : B'=1+B, [ C>=1 && C>=0 && free_2>=0 && 1+C>=2*free_2 && 2*free_2>=C ], cost: 3


Applied chaining over branches and pruning:
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
     51: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb6in : B'=1+B, C'=-1+free_23, [ A>=1+B && B>=1 && free>=0 && 1+B>=2*free && 2*free>=B && free_24>=0 && 1+B>=2*free_24 && 2*free_24>=B && free_25>=0 && 1+B>=2*free_25 && 2*free_25>=B && free_23>=0 && 1+B>=2*free_23 && 2*free_23>=B && 0>=-1+free_23 ], cost: 6
     52: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb6in : B'=1+B, C'=-1+free_23, [ A>=1+B && B>=1 && free>=0 && 1+B>=2*free && 2*free>=B && free_24>=0 && 1+B>=2*free_24 && 2*free_24>=B && free_25>=0 && 1+B>=2*free_25 && 2*free_25>=B && free_23>=0 && 1+B>=2*free_23 && 2*free_23>=B && -1+free_23>=1 && -1+free_23>=0 && free_2>=0 && free_23>=2*free_2 && 2*free_2>=-1+free_23 ], cost: 7
     53: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb6in : B'=1+B, C'=B, [ A>=1+B && 0>=B ], cost: 3
     54: evalrealheapsortstep1bb6in -> evalrealheapsortstep1bb6in : B'=1+B, C'=B, [ A>=1+B && B>=1 && B>=0 && free_2>=0 && 1+B>=2*free_2 && 2*free_2>=B ], cost: 4

Eliminating 4 self-loops for location evalrealheapsortstep1bb6in
  Removing the self-loops: 51 52 53 54.
Adding an epsilon transition (to model nonexecution of the loops): 59.

Removed all Self-loops using metering functions (where possible):
  Start location: evalrealheapsortstep1start
      0: evalrealheapsortstep1start -> evalrealheapsortstep1bb6in : B'=1, [ A>=3 ], cost: 2
     55: evalrealheapsortstep1bb6in -> [10] : B'=1+B, C'=-1+free_23, [ A>=1+B && B>=1 && free>=0 && 1+B>=2*free && 2*free>=B && free_24>=0 && 1+B>=2*free_24 && 2*free_24>=B && free_25>=0 && 1+B>=2*free_25 && 2*free_25>=B && free_23>=0 && 1+B>=2*free_23 && 2*free_23>=B && 0>=-1+free_23 ], cost: 6
     56: evalrealheapsortstep1bb6in -> [10] : B'=1+B, C'=-1+free_23, [ A>=1+B && B>=1 && free>=0 && 1+B>=2*free && 2*free>=B && free_24>=0 && 1+B>=2*free_24 && 2*free_24>=B && free_25>=0 && 1+B>=2*free_25 && 2*free_25>=B && 1+B>=2*free_23 && 2*free_23>=B && -1+free_23>=1 && free_2>=0 && free_23>=2*free_2 && 2*free_2>=-1+free_23 ], cost: 7
     57: evalrealheapsortstep1bb6in -> [10] : B'=1+B, C'=B, [ A>=1+B && 0>=B ], cost: 3
     58: evalrealheapsortstep1bb6in -> [10] : B'=1+B, C'=B, [ A>=1+B && B>=1 && free_2>=0 && 1+B>=2*free_2 && 2*free_2>=B ], cost: 4
     59: evalrealheapsortstep1bb6in -> [10] : [], cost: 0


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


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: evalrealheapsortstep1start
    <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),?)