I'll state this perhaps a bit too strongly (to make the point). Recursion, and program termination, are completely orthoginal issues. Check out our new paper:
CFL-Termination. This paper shows you how (if you have an oracle for partial correctness semantics) you can convert recursive programs into semantically equiv. non-recursive programs without tricky encodings using heap or non-linear updates to arithmetic variables. Enjoy ;-)