Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback