MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. eval_bin_search_StepSize2_start(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 1. eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 2. eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 3. eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 4. eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 5. eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 6. eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 7. eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 8. eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 9. eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 10. eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 11. eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 12. eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 13. eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 14. eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 15. eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 16. eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 17. eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v_s,v_0,4,v_c_1,v_c_2,v_c_3,0,0,v_f_1,v_f_2,v_r,v_s) True (?,1) 18. eval_bin_search_StepSize2_bb1_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 19. eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_17(v__0,nondef_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 20. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 1] (?,1) 21. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [0 >= v_c_0] (?,1) 22. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 1] (?,1) 23. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 24. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 25. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_0,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_f_0 = 0] (?,1) 26. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 0 && nondef_1 = 0] (?,1) 27. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 0 && nondef_1 >= 0 && -2*nondef_1 + v_c_0 >= 0 && 1 >= -2*nondef_1 + v_c_0] (?,1) 28. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_c_0 && 0 >= nondef_1 && 2*nondef_1 + -1*v_c_0 >= 0 && 1 >= 2*nondef_1 + -1*v_c_0] (?,1) 29. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_0 >= v_r] (?,1) 30. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_r >= v_0] (?,1) 31. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [0 >= v_d_0] (?,1) 32. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_d_0 >= 1] (?,1) 33. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 34. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 35. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 1 && v_f_0 = 0] (?,1) 36. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [v_c_1 = 0 && nondef_2 = 0] (?,1) 37. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_2 >= 0 && -2*nondef_2 + v_c_1 >= 0 && 1 >= -2*nondef_2 + v_c_1] (?,1) 38. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_2 && 2*nondef_2 + -1*v_c_1 >= 0 && 1 >= 2*nondef_2 + -1*v_c_1] (?,1) 39. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v__0 + v_c_2 >= 255] (?,1) 40. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + v_c_2,v_0,v_c_2,v_c_1,v_c_2,v_c_3,2,v_f_1,v_f_1,v_f_2,v_r,v_s) [255 >= v__0 + v_c_2] (?,1) 41. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_r >= v_0] (?,1) 42. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_0 >= v_r] (?,1) 43. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [1 >= v_d_0] (?,1) 44. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_d_0 >= 2] (?,1) 45. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 >= v_f_0] (?,1) 46. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 47. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 2 && v_f_0 = 0] (?,1) 48. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [v_c_1 = 0 && nondef_3 = 0] (?,1) 49. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_3 >= 0 && -2*nondef_3 + v_c_1 >= 0 && 1 >= -2*nondef_3 + v_c_1] (?,1) 50. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_3 && 2*nondef_3 + -1*v_c_1 >= 0 && 1 >= 2*nondef_3 + -1*v_c_1] (?,1) 51. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v__0 + -1*v_c_3] (?,1) 52. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + -1*v_c_3,v_0,v_c_3,v_c_1,v_c_2,v_c_3,1,v_f_2,v_f_1,v_f_2,v_r [v__0 + -1*v_c_3 >= 0] (?,1) ,v_s) 53. eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_stop(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) Signature: {(eval_bin_search_StepSize2_0,12) ;(eval_bin_search_StepSize2_1,12) ;(eval_bin_search_StepSize2_10,12) ;(eval_bin_search_StepSize2_11,12) ;(eval_bin_search_StepSize2_12,12) ;(eval_bin_search_StepSize2_13,12) ;(eval_bin_search_StepSize2_14,12) ;(eval_bin_search_StepSize2_15,12) ;(eval_bin_search_StepSize2_16,12) ;(eval_bin_search_StepSize2_17,12) ;(eval_bin_search_StepSize2_2,12) ;(eval_bin_search_StepSize2_3,12) ;(eval_bin_search_StepSize2_4,12) ;(eval_bin_search_StepSize2_5,12) ;(eval_bin_search_StepSize2_6,12) ;(eval_bin_search_StepSize2_7,12) ;(eval_bin_search_StepSize2_8,12) ;(eval_bin_search_StepSize2_9,12) ;(eval_bin_search_StepSize2_bb0_in,12) ;(eval_bin_search_StepSize2_bb10_in,12) ;(eval_bin_search_StepSize2_bb11_in,12) ;(eval_bin_search_StepSize2_bb12_in,12) ;(eval_bin_search_StepSize2_bb1_in,12) ;(eval_bin_search_StepSize2_bb2_in,12) ;(eval_bin_search_StepSize2_bb3_in,12) ;(eval_bin_search_StepSize2_bb4_in,12) ;(eval_bin_search_StepSize2_bb5_in,12) ;(eval_bin_search_StepSize2_bb6_in,12) ;(eval_bin_search_StepSize2_bb7_in,12) ;(eval_bin_search_StepSize2_bb8_in,12) ;(eval_bin_search_StepSize2_bb9_in,12) ;(eval_bin_search_StepSize2_start,12) ;(eval_bin_search_StepSize2_stop,12)} 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},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20,21,22},20->{53},21->{23,24,25},22->{23,24,25} ,23->{26,27,28},24->{26,27,28},25->{29,30},26->{29,30},27->{29,30},28->{29,30},29->{31,32,33,34,35},30->{41 ,42},31->{39,40},32->{39,40},33->{39,40},34->{39,40},35->{36,37,38},36->{39,40},37->{39,40},38->{39,40} ,39->{53},40->{18},41->{43,44,45,46,47},42->{53},43->{51,52},44->{51,52},45->{51,52},46->{51,52},47->{48,49 ,50},48->{51,52},49->{51,52},50->{51,52},51->{53},52->{18},53->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: AddSinks MAYBE + Considered Problem: Rules: 0. eval_bin_search_StepSize2_start(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 1. eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 2. eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 3. eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 4. eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 5. eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 6. eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 7. eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 8. eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 9. eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 10. eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 11. eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 12. eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 13. eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 14. eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 15. eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 16. eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 17. eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v_s,v_0,4,v_c_1,v_c_2,v_c_3,0,0,v_f_1,v_f_2,v_r,v_s) True (1,1) 18. eval_bin_search_StepSize2_bb1_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 19. eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_17(v__0,nondef_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 20. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 1] (1,1) 21. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [0 >= v_c_0] (?,1) 22. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 1] (?,1) 23. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 24. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 25. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_0,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_f_0 = 0] (?,1) 26. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 0 && nondef_1 = 0] (?,1) 27. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 0 && nondef_1 >= 0 && -2*nondef_1 + v_c_0 >= 0 && 1 >= -2*nondef_1 + v_c_0] (?,1) 28. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_c_0 && 0 >= nondef_1 && 2*nondef_1 + -1*v_c_0 >= 0 && 1 >= 2*nondef_1 + -1*v_c_0] (?,1) 29. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_0 >= v_r] (?,1) 30. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_r >= v_0] (?,1) 31. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [0 >= v_d_0] (?,1) 32. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_d_0 >= 1] (?,1) 33. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 34. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 35. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 1 && v_f_0 = 0] (?,1) 36. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [v_c_1 = 0 && nondef_2 = 0] (?,1) 37. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_2 >= 0 && -2*nondef_2 + v_c_1 >= 0 && 1 >= -2*nondef_2 + v_c_1] (?,1) 38. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_2 && 2*nondef_2 + -1*v_c_1 >= 0 && 1 >= 2*nondef_2 + -1*v_c_1] (?,1) 39. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v__0 + v_c_2 >= 255] (1,1) 40. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + v_c_2,v_0,v_c_2,v_c_1,v_c_2,v_c_3,2,v_f_1,v_f_1,v_f_2,v_r,v_s) [255 >= v__0 + v_c_2] (?,1) 41. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_r >= v_0] (?,1) 42. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_0 >= v_r] (1,1) 43. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [1 >= v_d_0] (?,1) 44. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_d_0 >= 2] (?,1) 45. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 >= v_f_0] (?,1) 46. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 47. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 2 && v_f_0 = 0] (?,1) 48. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [v_c_1 = 0 && nondef_3 = 0] (?,1) 49. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_3 >= 0 && -2*nondef_3 + v_c_1 >= 0 && 1 >= -2*nondef_3 + v_c_1] (?,1) 50. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_3 && 2*nondef_3 + -1*v_c_1 >= 0 && 1 >= 2*nondef_3 + -1*v_c_1] (?,1) 51. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v__0 + -1*v_c_3] (1,1) 52. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + -1*v_c_3,v_0,v_c_3,v_c_1,v_c_2,v_c_3,1,v_f_2,v_f_1,v_f_2,v_r [v__0 + -1*v_c_3 >= 0] (?,1) ,v_s) 53. eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_stop(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) Signature: {(eval_bin_search_StepSize2_0,12) ;(eval_bin_search_StepSize2_1,12) ;(eval_bin_search_StepSize2_10,12) ;(eval_bin_search_StepSize2_11,12) ;(eval_bin_search_StepSize2_12,12) ;(eval_bin_search_StepSize2_13,12) ;(eval_bin_search_StepSize2_14,12) ;(eval_bin_search_StepSize2_15,12) ;(eval_bin_search_StepSize2_16,12) ;(eval_bin_search_StepSize2_17,12) ;(eval_bin_search_StepSize2_2,12) ;(eval_bin_search_StepSize2_3,12) ;(eval_bin_search_StepSize2_4,12) ;(eval_bin_search_StepSize2_5,12) ;(eval_bin_search_StepSize2_6,12) ;(eval_bin_search_StepSize2_7,12) ;(eval_bin_search_StepSize2_8,12) ;(eval_bin_search_StepSize2_9,12) ;(eval_bin_search_StepSize2_bb0_in,12) ;(eval_bin_search_StepSize2_bb10_in,12) ;(eval_bin_search_StepSize2_bb11_in,12) ;(eval_bin_search_StepSize2_bb12_in,12) ;(eval_bin_search_StepSize2_bb1_in,12) ;(eval_bin_search_StepSize2_bb2_in,12) ;(eval_bin_search_StepSize2_bb3_in,12) ;(eval_bin_search_StepSize2_bb4_in,12) ;(eval_bin_search_StepSize2_bb5_in,12) ;(eval_bin_search_StepSize2_bb6_in,12) ;(eval_bin_search_StepSize2_bb7_in,12) ;(eval_bin_search_StepSize2_bb8_in,12) ;(eval_bin_search_StepSize2_bb9_in,12) ;(eval_bin_search_StepSize2_start,12) ;(eval_bin_search_StepSize2_stop,12)} 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},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20,21,22},20->{53},21->{23,24,25},22->{23,24,25} ,23->{26,27,28},24->{26,27,28},25->{29,30},26->{29,30},27->{29,30},28->{29,30},29->{31,32,33,34,35},30->{41 ,42},31->{39,40},32->{39,40},33->{39,40},34->{39,40},35->{36,37,38},36->{39,40},37->{39,40},38->{39,40} ,39->{53},40->{18},41->{43,44,45,46,47},42->{53},43->{51,52},44->{51,52},45->{51,52},46->{51,52},47->{48,49 ,50},48->{51,52},49->{51,52},50->{51,52},51->{53},52->{18},53->{}] + Applied Processor: AddSinks + Details: () * Step 3: Failure MAYBE + Considered Problem: Rules: 0. eval_bin_search_StepSize2_start(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (1,1) 1. eval_bin_search_StepSize2_bb0_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 2. eval_bin_search_StepSize2_0(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 3. eval_bin_search_StepSize2_1(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 4. eval_bin_search_StepSize2_2(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 5. eval_bin_search_StepSize2_3(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 6. eval_bin_search_StepSize2_4(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 7. eval_bin_search_StepSize2_5(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 8. eval_bin_search_StepSize2_6(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 9. eval_bin_search_StepSize2_7(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 10. eval_bin_search_StepSize2_8(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 11. eval_bin_search_StepSize2_9(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 12. eval_bin_search_StepSize2_10(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 13. eval_bin_search_StepSize2_11(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 14. eval_bin_search_StepSize2_12(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 15. eval_bin_search_StepSize2_13(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 16. eval_bin_search_StepSize2_14(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 17. eval_bin_search_StepSize2_15(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v_s,v_0,4,v_c_1,v_c_2,v_c_3,0,0,v_f_1,v_f_2,v_r,v_s) True (?,1) 18. eval_bin_search_StepSize2_bb1_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 19. eval_bin_search_StepSize2_16(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_17(v__0,nondef_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 20. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 1] (?,1) 21. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [0 >= v_c_0] (?,1) 22. eval_bin_search_StepSize2_17(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 1] (?,1) 23. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 24. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 25. eval_bin_search_StepSize2_bb2_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_0,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_f_0 = 0] (?,1) 26. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_c_0 = 0 && nondef_1 = 0] (?,1) 27. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_c_0 >= 0 && nondef_1 >= 0 && -2*nondef_1 + v_c_0 >= 0 && 1 >= -2*nondef_1 + v_c_0] (?,1) 28. eval_bin_search_StepSize2_bb3_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,nondef_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v_c_0 && 0 >= nondef_1 && 2*nondef_1 + -1*v_c_0 >= 0 && 1 >= 2*nondef_1 + -1*v_c_0] (?,1) 29. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_0 >= v_r] (?,1) 30. eval_bin_search_StepSize2_bb4_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_r >= v_0] (?,1) 31. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [0 >= v_d_0] (?,1) 32. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_d_0 >= 1] (?,1) 33. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 >= v_f_0] (?,1) 34. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_1,v_c_3,v_d_0,v_f_0,v_f_0,v_f_2,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 35. eval_bin_search_StepSize2_bb5_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 1 && v_f_0 = 0] (?,1) 36. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [v_c_1 = 0 && nondef_2 = 0] (?,1) 37. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_2 >= 0 && -2*nondef_2 + v_c_1 >= 0 && 1 >= -2*nondef_2 + v_c_1] (?,1) 38. eval_bin_search_StepSize2_bb6_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,nondef_2,v_c_3,v_d_0,v_f_0,1,v_f_2,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_2 && 2*nondef_2 + -1*v_c_1 >= 0 && 1 >= 2*nondef_2 + -1*v_c_1] (?,1) 39. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v__0 + v_c_2 >= 255] (?,1) 40. eval_bin_search_StepSize2_bb7_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + v_c_2,v_0,v_c_2,v_c_1,v_c_2,v_c_3,2,v_f_1,v_f_1,v_f_2,v_r,v_s) [255 >= v__0 + v_c_2] (?,1) 41. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 + v_r >= v_0] (?,1) 42. eval_bin_search_StepSize2_bb8_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_0 >= v_r] (?,1) 43. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [1 >= v_d_0] (?,1) 44. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_d_0 >= 2] (?,1) 45. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 >= v_f_0] (?,1) 46. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_1,v_d_0,v_f_0,v_f_1,v_f_0,v_r,v_s) [-1 + v_f_0 >= 0] (?,1) 47. eval_bin_search_StepSize2_bb9_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [v_d_0 = 2 && v_f_0 = 0] (?,1) 48. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [v_c_1 = 0 && nondef_3 = 0] (?,1) 49. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 + v_c_1 >= 0 && nondef_3 >= 0 && -2*nondef_3 + v_c_1 >= 0 && 1 >= -2*nondef_3 + v_c_1] (?,1) 50. eval_bin_search_StepSize2_bb10_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,nondef_3,v_d_0,v_f_0,v_f_1,1,v_r,v_s) [-1 >= v_c_1 && 0 >= nondef_3 && 2*nondef_3 + -1*v_c_1 >= 0 && 1 >= 2*nondef_3 + -1*v_c_1] (?,1) 51. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) [-1 >= v__0 + -1*v_c_3] (?,1) 52. eval_bin_search_StepSize2_bb11_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_bb1_in(v__0 + -1*v_c_3,v_0,v_c_3,v_c_1,v_c_2,v_c_3,1,v_f_2,v_f_1,v_f_2,v_r [v__0 + -1*v_c_3 >= 0] (?,1) ,v_s) 53. eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> eval_bin_search_StepSize2_stop(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) 54. eval_bin_search_StepSize2_bb12_in(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) -> exitus616(v__0,v_0,v_c_0,v_c_1,v_c_2,v_c_3,v_d_0,v_f_0,v_f_1,v_f_2,v_r,v_s) True (?,1) Signature: {(eval_bin_search_StepSize2_0,12) ;(eval_bin_search_StepSize2_1,12) ;(eval_bin_search_StepSize2_10,12) ;(eval_bin_search_StepSize2_11,12) ;(eval_bin_search_StepSize2_12,12) ;(eval_bin_search_StepSize2_13,12) ;(eval_bin_search_StepSize2_14,12) ;(eval_bin_search_StepSize2_15,12) ;(eval_bin_search_StepSize2_16,12) ;(eval_bin_search_StepSize2_17,12) ;(eval_bin_search_StepSize2_2,12) ;(eval_bin_search_StepSize2_3,12) ;(eval_bin_search_StepSize2_4,12) ;(eval_bin_search_StepSize2_5,12) ;(eval_bin_search_StepSize2_6,12) ;(eval_bin_search_StepSize2_7,12) ;(eval_bin_search_StepSize2_8,12) ;(eval_bin_search_StepSize2_9,12) ;(eval_bin_search_StepSize2_bb0_in,12) ;(eval_bin_search_StepSize2_bb10_in,12) ;(eval_bin_search_StepSize2_bb11_in,12) ;(eval_bin_search_StepSize2_bb12_in,12) ;(eval_bin_search_StepSize2_bb1_in,12) ;(eval_bin_search_StepSize2_bb2_in,12) ;(eval_bin_search_StepSize2_bb3_in,12) ;(eval_bin_search_StepSize2_bb4_in,12) ;(eval_bin_search_StepSize2_bb5_in,12) ;(eval_bin_search_StepSize2_bb6_in,12) ;(eval_bin_search_StepSize2_bb7_in,12) ;(eval_bin_search_StepSize2_bb8_in,12) ;(eval_bin_search_StepSize2_bb9_in,12) ;(eval_bin_search_StepSize2_start,12) ;(eval_bin_search_StepSize2_stop,12) ;(exitus616,12)} 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},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{18},18->{19},19->{20,21,22},20->{53,54},21->{23,24,25},22->{23,24 ,25},23->{26,27,28},24->{26,27,28},25->{29,30},26->{29,30},27->{29,30},28->{29,30},29->{31,32,33,34,35} ,30->{41,42},31->{39,40},32->{39,40},33->{39,40},34->{39,40},35->{36,37,38},36->{39,40},37->{39,40},38->{39 ,40},39->{53,54},40->{18},41->{43,44,45,46,47},42->{53,54},43->{51,52},44->{51,52},45->{51,52},46->{51,52} ,47->{48,49,50},48->{51,52},49->{51,52},50->{51,52},51->{53,54},52->{18},53->{},54->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,37,38,52,43,41,30,44,45,46,48,47,49,50] c: [50] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,37,38,52,43,41,30,44,45,46,48,47,49] c: [49] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,37,38,52,43,41,30,44,45,46,48,47] c: [48] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,37,38,52,43,41,30,44,45,46] c: [38] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,37,52,43,41,30,44,45,46] c: [37] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,36,35,52,43,41,30,44,45,46] c: [36] | `- p:[18,40,31,29,25,21,19,22,26,23,24,27,28,32,33,34,52,43,41,30,44,45,46] c: [] MAYBE