They overapproximate. This means that may say something probably doesn't terminate even if it terminates. The idea is that if it says it terminates, then there is a proof it does.
Not necessarily. For instance, CBMC has been participating in the Termination category with an approach based on Bounded model checking, an underapproximation technique. Thus, they always produce correct result, but their analysis might not terminate (or may terminate with an "unknown" verdict).
Do they know beforehand a value of N so that the proofs have depth < N?