MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (?,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (?,1) 14. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (?,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (?,1) 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_2 >= v_size] (?,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (?,1) 27. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_4 >= v_size] (?,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (?,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (?,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (?,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (?,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (?,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13,14},12->{15 ,16},13->{42},14->{42},15->{17,18,19},16->{24,25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24 ,25},23->{24,25},24->{26,27,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34 ,35},32->{33,34,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42} ,40->{42},41->{12,13,14},42->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (1,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (1,1) 14. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (1,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (1,1) 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_2 >= v_size] (1,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (1,1) 27. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_4 >= v_size] (1,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (1,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (1,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (1,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (1,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (1,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13,14},12->{15 ,16},13->{42},14->{42},15->{17,18,19},16->{24,25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24 ,25},23->{24,25},24->{26,27,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34 ,35},32->{33,34,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42} ,40->{42},41->{12,13,14},42->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(11,14),(15,18),(16,24),(24,27),(41,13),(41,14)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (1,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (1,1) 14. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (1,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (1,1) 18. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_2 >= v_size] (1,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (1,1) 27. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_4 >= v_size] (1,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (1,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (1,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (1,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (1,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (1,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{15,16} ,13->{42},14->{42},15->{17,19},16->{25},17->{42},18->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24 ,25},24->{26,28},25->{33,34,35},26->{42},27->{42},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34 ,35},33->{36,37,38},34->{36,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42},40->{42},41->{12} ,42->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [14,18,27] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (1,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (1,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (1,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (1,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (1,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (1,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (1,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (1,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (1,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{15,16} ,13->{42},15->{17,19},16->{25},17->{42},19->{20},20->{21},21->{22,23},22->{24,25},23->{24,25},24->{26,28} ,25->{33,34,35},26->{42},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34,35},33->{36,37,38},34->{36 ,37,38},35->{42},36->{42},37->{42},38->{39,40,41},39->{42},40->{42},41->{12},42->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (?,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (?,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (?,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (?,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (?,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (?,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (?,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (?,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (?,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 43. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8) ;(exitus616,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{15,16} ,13->{42,43},15->{17,19},16->{24,25},17->{42,43},19->{20},20->{21},21->{22,23},22->{24,25},23->{24,25} ,24->{26,28},25->{33,34,35},26->{42,43},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34,35},33->{36 ,37,38},34->{36,37,38},35->{42,43},36->{42,43},37->{42,43},38->{39,40,41},39->{42,43},40->{42,43},41->{12 ,13},42->{},43->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(16,24),(41,13)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. eval_heapsort_start(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (1,1) 1. eval_heapsort_bb0_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 2. eval_heapsort_0(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 3. eval_heapsort_1(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 4. eval_heapsort_2(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 5. eval_heapsort_3(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 6. eval_heapsort_4(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 7. eval_heapsort_5(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 8. eval_heapsort_6(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 9. eval_heapsort_7(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 10. eval_heapsort_8(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 11. eval_heapsort_9(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,1,v_max_1,v_max_3,v_size) True (?,1) 12. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_size >= 0 && v_i_0 >= 1] (?,1) 13. eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_size] (?,1) 15. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb3_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= 2*v_i_0] (?,1) 16. eval_heapsort_bb2_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,2*v_i_0,1 + 2*v_i_0,v_8,v_i_0,v_i_0,v_max_3,v_size) [-1 + 2*v_i_0 >= v_size] (?,1) 17. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_2] (?,1) 19. eval_heapsort_bb3_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_2 >= 1 && v_size >= v_2] (?,1) 20. eval_heapsort_bb4_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 21. eval_heapsort_14(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_15(v_13,v_2,v_4,nondef_0,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 22. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_2,v_max_3,v_size) [-1 + v_8 >= 0] (?,1) 23. eval_heapsort_15(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_i_0,v_max_3,v_size) [0 >= v_8] (?,1) 24. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_size >= v_4] (?,1) 25. eval_heapsort_bb5_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [-1 + v_4 >= v_size] (?,1) 26. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_4] (?,1) 28. eval_heapsort_bb6_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_4 >= 1 && v_size >= v_4] (?,1) 29. eval_heapsort_bb7_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 30. eval_heapsort_17(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_18(nondef_1,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 31. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_4,v_size) [-1 + v_13 >= 0] (?,1) 32. eval_heapsort_18(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_1,v_size) [0 >= v_13] (?,1) 33. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_i_0] (?,1) 34. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_max_3] (?,1) 35. eval_heapsort_bb8_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 = v_max_3] (?,1) 36. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_i_0] (?,1) 37. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_i_0 >= v_size] (?,1) 38. eval_heapsort_bb9_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [v_i_0 >= 1 && v_size >= v_i_0] (?,1) 39. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [0 >= v_max_3] (?,1) 40. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) [-1 + v_max_3 >= v_size] (?,1) 41. eval_heapsort_bb10_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_bb1_in(v_13,v_2,v_4,v_8,v_max_3,v_max_1,v_max_3,v_size) [v_max_3 >= 1 && v_size >= v_max_3] (?,1) 42. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> eval_heapsort_stop(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) 43. eval_heapsort_bb11_in(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) -> exitus616(v_13,v_2,v_4,v_8,v_i_0,v_max_1,v_max_3,v_size) True (?,1) Signature: {(eval_heapsort_0,8) ;(eval_heapsort_1,8) ;(eval_heapsort_14,8) ;(eval_heapsort_15,8) ;(eval_heapsort_17,8) ;(eval_heapsort_18,8) ;(eval_heapsort_2,8) ;(eval_heapsort_3,8) ;(eval_heapsort_4,8) ;(eval_heapsort_5,8) ;(eval_heapsort_6,8) ;(eval_heapsort_7,8) ;(eval_heapsort_8,8) ;(eval_heapsort_9,8) ;(eval_heapsort_bb0_in,8) ;(eval_heapsort_bb10_in,8) ;(eval_heapsort_bb11_in,8) ;(eval_heapsort_bb1_in,8) ;(eval_heapsort_bb2_in,8) ;(eval_heapsort_bb3_in,8) ;(eval_heapsort_bb4_in,8) ;(eval_heapsort_bb5_in,8) ;(eval_heapsort_bb6_in,8) ;(eval_heapsort_bb7_in,8) ;(eval_heapsort_bb8_in,8) ;(eval_heapsort_bb9_in,8) ;(eval_heapsort_start,8) ;(eval_heapsort_stop,8) ;(exitus616,8)} Flow Graph: [0->{1},1->{2},2->{3},3->{4},4->{5},5->{6},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12,13},12->{15,16} ,13->{42,43},15->{17,19},16->{25},17->{42,43},19->{20},20->{21},21->{22,23},22->{24,25},23->{24,25},24->{26 ,28},25->{33,34,35},26->{42,43},28->{29},29->{30},30->{31,32},31->{33,34,35},32->{33,34,35},33->{36,37,38} ,34->{36,37,38},35->{42,43},36->{42,43},37->{42,43},38->{39,40,41},39->{42,43},40->{42,43},41->{12},42->{} ,43->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,19,20,21,22,23,24,25,26,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43] | `- p:[12,41,38,33,25,16,22,21,20,19,15,23,31,30,29,28,24,32,34] c: [] MAYBE