YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval_rsd_start(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (1,1) 1. eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 2. eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 3. eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 4. eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] (?,1) 5. eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [-1 >= v_r] (?,1) 6. eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4(2*v_r,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] (?,1) 7. eval_rsd_4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] (?,1) 8. eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6(v_1,2*v_r,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] (?,1) 9. eval_rsd_6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 10. eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 11. eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 12. eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 13. eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 14. eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 15. eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,v_1,v_2,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 16. eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] 17. eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] 18. eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 19. eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14(v_1,v_2,nondef_0,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 20. eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] 21. eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_db_0,v_da_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] 22. eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) Signature: {(eval_rsd_0,6) ;(eval_rsd_1,6) ;(eval_rsd_10,6) ;(eval_rsd_11,6) ;(eval_rsd_12,6) ;(eval_rsd_13,6) ;(eval_rsd_14,6) ;(eval_rsd_2,6) ;(eval_rsd_4,6) ;(eval_rsd_5,6) ;(eval_rsd_6,6) ;(eval_rsd_7,6) ;(eval_rsd_8,6) ;(eval_rsd_9,6) ;(eval_rsd_bb0_in,6) ;(eval_rsd_bb1_in,6) ;(eval_rsd_bb2_in,6) ;(eval_rsd_bb3_in,6) ;(eval_rsd_bb4_in,6) ;(eval_rsd_start,6) ;(eval_rsd_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{22},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16,17},16->{18},17->{22},18->{19},19->{20,21},20->{16,17},21->{16,17},22->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(15,17)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval_rsd_start(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (1,1) 1. eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 2. eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 3. eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) 4. eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] (?,1) 5. eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [-1 >= v_r] (?,1) 6. eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4(2*v_r,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] (?,1) 7. eval_rsd_4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] (?,1) 8. eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6(v_1,2*v_r,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] (?,1) 9. eval_rsd_6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 10. eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 11. eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 12. eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 13. eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 14. eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 15. eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,v_1,v_2,v_r) [v_2 + -1*v_r >= 0 (?,1) && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 16. eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] 17. eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] 18. eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 19. eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14(v_1,v_2,nondef_0,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] 20. eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] 21. eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_db_0,v_da_0,v_r) [v_db_0 + -1*v_r >= 0 (?,1) && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] 22. eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True (?,1) Signature: {(eval_rsd_0,6) ;(eval_rsd_1,6) ;(eval_rsd_10,6) ;(eval_rsd_11,6) ;(eval_rsd_12,6) ;(eval_rsd_13,6) ;(eval_rsd_14,6) ;(eval_rsd_2,6) ;(eval_rsd_4,6) ;(eval_rsd_5,6) ;(eval_rsd_6,6) ;(eval_rsd_7,6) ;(eval_rsd_8,6) ;(eval_rsd_9,6) ;(eval_rsd_bb0_in,6) ;(eval_rsd_bb1_in,6) ;(eval_rsd_bb2_in,6) ;(eval_rsd_bb3_in,6) ;(eval_rsd_bb4_in,6) ;(eval_rsd_start,6) ;(eval_rsd_stop,6)} Flow Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{22},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{18},17->{22},18->{19},19->{20,21},20->{16,17},21->{16,17},22->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: eval_rsd_start(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True eval_rsd_bb0_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True eval_rsd_0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True eval_rsd_1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] eval_rsd_2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [-1 >= v_r] eval_rsd_bb1_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4(2*v_r,v_2,v_4,v_da_0,v_db_0,v_r) [v_r >= 0] eval_rsd_4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6(v_1,2*v_r,v_4,v_da_0,v_db_0,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,v_1,v_2,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] eval_rsd_bb2_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] eval_rsd_bb3_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14(v_1,v_2,nondef_0,v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_da_0,v_db_0,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in(v_1,v_2,v_4,-1 + v_db_0,v_da_0,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_bb4_in(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop(v_1,v_2,v_4,v_da_0,v_db_0,v_r) True Signature: {(eval_rsd_0,6) ;(eval_rsd_1,6) ;(eval_rsd_10,6) ;(eval_rsd_11,6) ;(eval_rsd_12,6) ;(eval_rsd_13,6) ;(eval_rsd_14,6) ;(eval_rsd_2,6) ;(eval_rsd_4,6) ;(eval_rsd_5,6) ;(eval_rsd_6,6) ;(eval_rsd_7,6) ;(eval_rsd_8,6) ;(eval_rsd_9,6) ;(eval_rsd_bb0_in,6) ;(eval_rsd_bb1_in,6) ;(eval_rsd_bb2_in,6) ;(eval_rsd_bb3_in,6) ;(eval_rsd_bb4_in,6) ;(eval_rsd_start,6) ;(eval_rsd_stop,6)} Rule Graph: [0->{1},1->{2},2->{3},3->{4,5},4->{6},5->{22},6->{7},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{18},17->{22},18->{19},19->{20,21},20->{16,17},21->{16,17},22->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: eval_rsd_start.0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [-1 >= v_r] eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4.7(2*v_r,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_4.7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6.9(v_1,2*v_r,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_6.9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,v_1,v_2 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_bb2_in.16(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] eval_rsd_bb2_in.17(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.20(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.21(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True Signature: {(eval_rsd_0.2,6) ;(eval_rsd_1.3,6) ;(eval_rsd_10.13,6) ;(eval_rsd_11.14,6) ;(eval_rsd_12.15,6) ;(eval_rsd_13.19,6) ;(eval_rsd_14.20,6) ;(eval_rsd_14.21,6) ;(eval_rsd_2.4,6) ;(eval_rsd_2.5,6) ;(eval_rsd_4.7,6) ;(eval_rsd_5.8,6) ;(eval_rsd_6.9,6) ;(eval_rsd_7.10,6) ;(eval_rsd_8.11,6) ;(eval_rsd_9.12,6) ;(eval_rsd_bb0_in.1,6) ;(eval_rsd_bb1_in.6,6) ;(eval_rsd_bb2_in.16,6) ;(eval_rsd_bb2_in.17,6) ;(eval_rsd_bb3_in.18,6) ;(eval_rsd_bb4_in.22,6) ;(eval_rsd_start.0,6) ;(eval_rsd_stop.23,6)} Rule Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{7},6->{26},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{19},18->{26},19->{20,21},20->{22,23},21->{24,25},22->{17},23->{18} ,24->{17},25->{18},26->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: eval_rsd_start.0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [-1 >= v_r] eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4.7(2*v_r,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_4.7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6.9(v_1,2*v_r,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_6.9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,v_1,v_2 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_bb2_in.16(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] eval_rsd_bb2_in.17(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.20(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.21(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True Signature: {(eval_rsd_0.2,6) ;(eval_rsd_1.3,6) ;(eval_rsd_10.13,6) ;(eval_rsd_11.14,6) ;(eval_rsd_12.15,6) ;(eval_rsd_13.19,6) ;(eval_rsd_14.20,6) ;(eval_rsd_14.21,6) ;(eval_rsd_2.4,6) ;(eval_rsd_2.5,6) ;(eval_rsd_4.7,6) ;(eval_rsd_5.8,6) ;(eval_rsd_6.9,6) ;(eval_rsd_7.10,6) ;(eval_rsd_8.11,6) ;(eval_rsd_9.12,6) ;(eval_rsd_bb0_in.1,6) ;(eval_rsd_bb1_in.6,6) ;(eval_rsd_bb2_in.16,6) ;(eval_rsd_bb2_in.17,6) ;(eval_rsd_bb3_in.18,6) ;(eval_rsd_bb4_in.22,6) ;(eval_rsd_start.0,6) ;(eval_rsd_stop.23,6) ;(exitus616,6)} Rule Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{7},6->{26},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{19},18->{26},19->{20,21},20->{22,23},21->{24,25},22->{17},23->{18} ,24->{17},25->{18},26->{27,28,29}] + Applied Processor: Decompose Greedy + 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] | `- p:[17,22,20,19,24,21] c: [17,19,20,21,22,24] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: eval_rsd_start.0(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_bb0_in.1(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_0.2(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_1.3(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_2.4(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_2.5(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [-1 >= v_r] eval_rsd_bb1_in.6(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_4.7(2*v_r,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_r >= 0] eval_rsd_4.7(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_5.8(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_6.9(v_1,2*v_r,v_4,v_da_0,v_db_0 ,v_r) [v_1 + -1*v_r >= 0 && v_r >= 0 && v_1 + v_r >= 0 && v_1 >= 0] eval_rsd_6.9(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_7.10(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_8.11(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_9.12(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_10.13(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_11.14(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_12.15(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,v_1,v_2 ,v_r) [v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_bb2_in.16(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && v_da_0 >= v_r] eval_rsd_bb2_in.17(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_r >= v_da_0] eval_rsd_bb3_in.18(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.20(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_13.19(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_14.21(v_1,v_2,nondef_0,v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.20(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_da_0,v_db_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && -1 + v_4 >= 0] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.16(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_14.21(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_bb2_in.17(v_1,v_2,v_4,-1 + v_db_0,v_da_0 ,v_r) [v_db_0 + -1*v_r >= 0 && v_da_0 + -1*v_r >= 0 && v_2 + -1*v_r >= 0 && v_1 + -1*v_r >= 0 && v_r >= 0 && v_db_0 + v_r >= 0 && v_da_0 + v_r >= 0 && v_2 + v_r >= 0 && v_1 + v_r >= 0 && v_db_0 >= 0 && v_da_0 + v_db_0 >= 0 && v_2 + v_db_0 >= 0 && v_1 + v_db_0 >= 0 && v_da_0 >= 0 && v_2 + v_da_0 >= 0 && v_1 + v_da_0 >= 0 && v_2 >= 0 && v_1 + v_2 >= 0 && v_1 >= 0 && 0 >= v_4] eval_rsd_bb4_in.22(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True eval_rsd_stop.23(v_1,v_2,v_4,v_da_0,v_db_0,v_r) -> exitus616(v_1,v_2,v_4,v_da_0,v_db_0 ,v_r) True Signature: {(eval_rsd_0.2,6) ;(eval_rsd_1.3,6) ;(eval_rsd_10.13,6) ;(eval_rsd_11.14,6) ;(eval_rsd_12.15,6) ;(eval_rsd_13.19,6) ;(eval_rsd_14.20,6) ;(eval_rsd_14.21,6) ;(eval_rsd_2.4,6) ;(eval_rsd_2.5,6) ;(eval_rsd_4.7,6) ;(eval_rsd_5.8,6) ;(eval_rsd_6.9,6) ;(eval_rsd_7.10,6) ;(eval_rsd_8.11,6) ;(eval_rsd_9.12,6) ;(eval_rsd_bb0_in.1,6) ;(eval_rsd_bb1_in.6,6) ;(eval_rsd_bb2_in.16,6) ;(eval_rsd_bb2_in.17,6) ;(eval_rsd_bb3_in.18,6) ;(eval_rsd_bb4_in.22,6) ;(eval_rsd_start.0,6) ;(eval_rsd_stop.23,6) ;(exitus616,6)} Rule Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{7},6->{26},7->{8},8->{9},9->{10},10->{11},11->{12},12->{13} ,13->{14},14->{15},15->{16},16->{17},17->{19},18->{26},19->{20,21},20->{22,23},21->{24,25},22->{17},23->{18} ,24->{17},25->{18},26->{27,28,29}] ,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] | `- p:[17,22,20,19,24,21] c: [17,19,20,21,22,24]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [v_1,v_2,v_4,v_da_0,v_db_0,v_r,0.0] eval_rsd_start.0 ~> eval_rsd_bb0_in.1 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_bb0_in.1 ~> eval_rsd_0.2 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_0.2 ~> eval_rsd_1.3 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_1.3 ~> eval_rsd_2.4 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_1.3 ~> eval_rsd_2.5 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_2.4 ~> eval_rsd_bb1_in.6 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_2.5 ~> eval_rsd_bb4_in.22 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_bb1_in.6 ~> eval_rsd_4.7 [v_1 <= 2*v_r, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_4.7 ~> eval_rsd_5.8 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_5.8 ~> eval_rsd_6.9 [v_1 <= v_1, v_2 <= v_1 + v_r, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_6.9 ~> eval_rsd_7.10 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_7.10 ~> eval_rsd_8.11 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_8.11 ~> eval_rsd_9.12 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_9.12 ~> eval_rsd_10.13 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_10.13 ~> eval_rsd_11.14 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_11.14 ~> eval_rsd_12.15 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_12.15 ~> eval_rsd_bb2_in.16 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_1, v_db_0 <= v_2, v_r <= v_r] eval_rsd_bb2_in.16 ~> eval_rsd_bb3_in.18 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_bb2_in.17 ~> eval_rsd_bb4_in.22 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_bb3_in.18 ~> eval_rsd_13.19 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_13.19 ~> eval_rsd_14.20 [v_1 <= v_1, v_2 <= v_2, v_4 <= unknown, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_13.19 ~> eval_rsd_14.21 [v_1 <= v_1, v_2 <= v_2, v_4 <= unknown, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_14.20 ~> eval_rsd_bb2_in.16 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_14.20 ~> eval_rsd_bb2_in.17 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_14.21 ~> eval_rsd_bb2_in.16 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_db_0, v_db_0 <= v_da_0, v_r <= v_r] eval_rsd_14.21 ~> eval_rsd_bb2_in.17 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_db_0, v_db_0 <= v_da_0, v_r <= v_r] eval_rsd_bb4_in.22 ~> eval_rsd_stop.23 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_stop.23 ~> exitus616 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_stop.23 ~> exitus616 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_stop.23 ~> exitus616 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] + Loop: [0.0 <= v_da_0 + v_db_0] eval_rsd_bb2_in.16 ~> eval_rsd_bb3_in.18 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_14.20 ~> eval_rsd_bb2_in.16 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_13.19 ~> eval_rsd_14.20 [v_1 <= v_1, v_2 <= v_2, v_4 <= unknown, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_bb3_in.18 ~> eval_rsd_13.19 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] eval_rsd_14.21 ~> eval_rsd_bb2_in.16 [v_1 <= v_1, v_2 <= v_2, v_4 <= v_4, v_da_0 <= K + v_db_0, v_db_0 <= v_da_0, v_r <= v_r] eval_rsd_13.19 ~> eval_rsd_14.21 [v_1 <= v_1, v_2 <= v_2, v_4 <= unknown, v_da_0 <= v_da_0, v_db_0 <= v_db_0, v_r <= v_r] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,v_1,v_2,v_4,v_da_0,v_db_0,v_r,0.0] eval_rsd_start.0 ~> eval_rsd_bb0_in.1 [] eval_rsd_bb0_in.1 ~> eval_rsd_0.2 [] eval_rsd_0.2 ~> eval_rsd_1.3 [] eval_rsd_1.3 ~> eval_rsd_2.4 [] eval_rsd_1.3 ~> eval_rsd_2.5 [] eval_rsd_2.4 ~> eval_rsd_bb1_in.6 [] eval_rsd_2.5 ~> eval_rsd_bb4_in.22 [] eval_rsd_bb1_in.6 ~> eval_rsd_4.7 [v_r ~*> v_1] eval_rsd_4.7 ~> eval_rsd_5.8 [] eval_rsd_5.8 ~> eval_rsd_6.9 [v_1 ~+> v_2,v_r ~+> v_2] eval_rsd_6.9 ~> eval_rsd_7.10 [] eval_rsd_7.10 ~> eval_rsd_8.11 [] eval_rsd_8.11 ~> eval_rsd_9.12 [] eval_rsd_9.12 ~> eval_rsd_10.13 [] eval_rsd_10.13 ~> eval_rsd_11.14 [] eval_rsd_11.14 ~> eval_rsd_12.15 [] eval_rsd_12.15 ~> eval_rsd_bb2_in.16 [v_1 ~=> v_da_0,v_2 ~=> v_db_0] eval_rsd_bb2_in.16 ~> eval_rsd_bb3_in.18 [] eval_rsd_bb2_in.17 ~> eval_rsd_bb4_in.22 [] eval_rsd_bb3_in.18 ~> eval_rsd_13.19 [] eval_rsd_13.19 ~> eval_rsd_14.20 [huge ~=> v_4] eval_rsd_13.19 ~> eval_rsd_14.21 [huge ~=> v_4] eval_rsd_14.20 ~> eval_rsd_bb2_in.16 [v_da_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_14.20 ~> eval_rsd_bb2_in.17 [v_da_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_14.21 ~> eval_rsd_bb2_in.16 [v_da_0 ~=> v_db_0,v_db_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_14.21 ~> eval_rsd_bb2_in.17 [v_da_0 ~=> v_db_0,v_db_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_bb4_in.22 ~> eval_rsd_stop.23 [] eval_rsd_stop.23 ~> exitus616 [] eval_rsd_stop.23 ~> exitus616 [] eval_rsd_stop.23 ~> exitus616 [] + Loop: [v_da_0 ~+> 0.0,v_db_0 ~+> 0.0] eval_rsd_bb2_in.16 ~> eval_rsd_bb3_in.18 [] eval_rsd_14.20 ~> eval_rsd_bb2_in.16 [v_da_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_13.19 ~> eval_rsd_14.20 [huge ~=> v_4] eval_rsd_bb3_in.18 ~> eval_rsd_13.19 [] eval_rsd_14.21 ~> eval_rsd_bb2_in.16 [v_da_0 ~=> v_db_0,v_db_0 ~+> v_da_0,K ~+> v_da_0] eval_rsd_13.19 ~> eval_rsd_14.21 [huge ~=> v_4] + Applied Processor: Lare + Details: eval_rsd_start.0 ~> exitus616 [huge ~=> v_4 ,v_r ~+> v_2 ,v_r ~+> v_da_0 ,v_r ~+> v_db_0 ,v_r ~+> 0.0 ,v_r ~+> tick ,tick ~+> tick ,K ~+> v_da_0 ,K ~+> v_db_0 ,v_r ~*> v_1 ,v_r ~*> v_2 ,v_r ~*> v_da_0 ,v_r ~*> v_db_0 ,v_r ~*> 0.0 ,v_r ~*> tick ,K ~*> v_da_0 ,K ~*> v_db_0] + eval_rsd_14.20> [v_da_0 ~=> v_db_0 ,huge ~=> v_4 ,v_da_0 ~+> v_da_0 ,v_da_0 ~+> v_db_0 ,v_da_0 ~+> 0.0 ,v_da_0 ~+> tick ,v_db_0 ~+> v_da_0 ,v_db_0 ~+> v_db_0 ,v_db_0 ~+> 0.0 ,v_db_0 ~+> tick ,tick ~+> tick ,K ~+> v_da_0 ,K ~+> v_db_0 ,v_da_0 ~*> v_da_0 ,v_da_0 ~*> v_db_0 ,v_db_0 ~*> v_da_0 ,v_db_0 ~*> v_db_0 ,K ~*> v_da_0 ,K ~*> v_db_0] eval_rsd_14.21> [v_da_0 ~=> v_db_0 ,huge ~=> v_4 ,v_da_0 ~+> v_da_0 ,v_da_0 ~+> v_db_0 ,v_da_0 ~+> 0.0 ,v_da_0 ~+> tick ,v_db_0 ~+> v_da_0 ,v_db_0 ~+> v_db_0 ,v_db_0 ~+> 0.0 ,v_db_0 ~+> tick ,tick ~+> tick ,K ~+> v_da_0 ,K ~+> v_db_0 ,v_da_0 ~*> v_da_0 ,v_da_0 ~*> v_db_0 ,v_db_0 ~*> v_da_0 ,v_db_0 ~*> v_db_0 ,K ~*> v_da_0 ,K ~*> v_db_0] YES(?,POLY)