This is not true in theory. A model checker (NOT a bounded model checker) either produces a counter-example, a proof of correctness or times-out/gives up if the

This is not true in theory. A model checker (NOT a bounded model checker) either produces a counter-example, a proof of correctness or times-out/gives up if the theory is not decidable. A bounded model checker on the other hand, checks the property for a given depth 'k', and hence the result is not applicable to a complete run. In practice, it is all engineering, so anything can happen unless the model checker has been model checked.