How hard is it to reduce termination to partial correctness?
One way to answer this is to consider the computational complexity of the decision problems for the classes of partial correctness and termination queries that are known to be decidable.  Abstract interpretation using the polyhedral domain can infer the partial correctness annotations you mention in cases where the required annotations are conjunctions of linear inequalities.  Computing the abstract post-condition is exponential in the number of variables.  Then there is the overhead of finding the fixed point.  See Cousot's early papers for more on this and the Apron library if you want to play with it directly.

Finding variant functions is decidable when the variant functions are linear.  I couldn't find a complete characterization of the complexity of this, but "Termination of Linear Programs" by Tiwari has a section that discusses complexity.  See also "A Complete Method for the Synthesis of Linear Ranking Functions" by Podelski and Rybalchenko.  Also, Byron Cook has done work on leveraging abstract interpretation to help construct termination arguments.  See, for example, "Ranking Abstractions" and "Variance Analyses from Invariance Analyses".  These may give further insight into the relationship between partial correctness and termination.

Links:


http://www.csl.sri.com/users/tiwari/html/cav04.html
http://www7.in.tum.de/~rybal/papers/vmcai04-linear-ranking.pdf
http://www.dcs.qmul.ac.uk/~hyang/paper/esop08.pdf
http://research.microsoft.com/terminator/popl07a.pdf