Not necessarily. For instance, CBMC has been participating in the Termination category with an approach based on Bounded model checking, an underapproximation t

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).